EncodedRules.lean

1import BFPP.EncodedRecurrence23/-! # Explicit formulas for the encoded successor and limit coordinates -/45namespace BFPP67set_option autoImplicit false8open Set Order910universe u11variable {ρ σ κ : Ordinal.{u}} [Fact (IsSuccLimit ρ)] [Fact (IsSuccLimit σ)]12    [hκ : Fact (IsSuccLimit κ)]1314theorem encodeProfiles_delay_even_succ (hρκ : ρ ≤ κ) (hσκ : σ ≤ κ)15    (z : TwoProfile (OrdinalIndex ρ) (OrdinalIndex σ)) (i : OrdinalIndex κ) :16    encodeProfiles hρκ hσκ z.delay (evenIndex κ (succ i)) =17      encodeProfiles hρκ hσκ z (evenIndex κ i) := by18  rw [encodeProfiles_delay_interleave, interleave_even, Profile.delay_apply,19    Profile.delayValue_succ, encodeProfiles_even]2021theorem encodeProfiles_delay_odd_succ (hρκ : ρ ≤ κ) (hσκ : σ ≤ κ)22    (z : TwoProfile (OrdinalIndex ρ) (OrdinalIndex σ)) (i : OrdinalIndex κ) :23    encodeProfiles hρκ hσκ z.delay (oddIndex κ (succ i)) =24      encodeProfiles hρκ hσκ z (oddIndex κ i) := by25  rw [encodeProfiles_delay_interleave, interleave_odd, Profile.delay_apply,26    Profile.delayValue_succ, encodeProfiles_odd]2728theorem encodeProfiles_delay_odd_zero (hρκ : ρ ≤ κ) (hσκ : σ ≤ κ)29    (z : TwoProfile (OrdinalIndex ρ) (OrdinalIndex σ)) :30    encodeProfiles hρκ hσκ z.delay (oddIndex κ ⊥) = 4 := by31  rw [encodeProfiles_odd, Profile.at_bot, add_zero]3233theorem encodeProfiles_delay_upper_limit (hρκ : ρ ≤ κ) (hσκ : σ ≤ κ)34    (z : TwoProfile (OrdinalIndex ρ) (OrdinalIndex σ)) (i : OrdinalIndex κ)35    (hi : IsSuccLimit i.val) :36    encodeProfiles hρκ hσκ z.delay (oddIndex κ i) =37      upperEnvelope (restrictFamily i.property.le (encodeProfiles hρκ hσκ z)) := by38  letI : Fact (IsSuccLimit i.val) := ⟨hi⟩39  rw [encodeProfiles_delay_interleave, interleave_odd, Profile.delay_apply]40  exact (interleave_upperEnvelope_prefix i.property41    (z.val.1.extend hρκ) (z.val.2.extend hσκ)).symm4243/-- At a limit ordinal the odd encoded coordinate is its immediate successor. -/44theorem oddIndex_limit_val (i : OrdinalIndex κ) (hi : IsSuccLimit i.val) :45    (oddIndex κ i).val = i.val + 1 := by46  change 2 * i.val + 1 = i.val + 147  rw [ordinal_two_mul_limit i.val hi]4849end BFPP

SHA-256