IndisputableMonolith.Gravity.Analysis.Q3PatchSeating

   1import Mathlib
   2import IndisputableMonolith.Patterns
   3
   4/-!
   5# Canonical three-cube × record-time seating into the Fin 16 patch
   6
   7Frozen world G1 of
   8`holography/plans/OrderSensitive_Gravity_Proposition_20260802.html`.
   9
  10Packs Pattern 3 axes into patch bits 0,1,2 and record-time into bit 3.
  11Does not import the heavy gravity analysis chain.
  12
  13## Honesty
  14
  15* THEOREM: bijectivity and the time-bit involution.
  16* MODEL: treating the fourth bit as record time.
  17-/
  18
  19namespace IndisputableMonolith
  20namespace Gravity
  21namespace Analysis
  22namespace Q3PatchSeating
  23
  24open IndisputableMonolith.Patterns
  25
  26@[simp] def bitNat : Bool → ℕ
  27  | true => 1
  28  | false => 0
  29
  30theorem bitNat_le_one (b : Bool) : bitNat b ≤ 1 := by
  31  cases b <;> simp [bitNat]
  32
  33def seatNat (p : Pattern 3) (t : Bool) : ℕ :=
  34  bitNat (p 0) + 2 * bitNat (p 1) + 4 * bitNat (p 2) + 8 * bitNat t
  35
  36theorem seatNat_lt (p : Pattern 3) (t : Bool) : seatNat p t < 16 := by
  37  have h0 := bitNat_le_one (p 0)
  38  have h1 := bitNat_le_one (p 1)
  39  have h2 := bitNat_le_one (p 2)
  40  have ht := bitNat_le_one t
  41  unfold seatNat
  42  omega
  43
  44def seat (p : Pattern 3) (t : Bool) : Fin 16 :=
  45  ⟨seatNat p t, seatNat_lt p t⟩
  46
  47def unseat (v : Fin 16) : Pattern 3 × Bool :=
  48  (fun
  49    | 0 => v.val.testBit 0
  50    | 1 => v.val.testBit 1
  51    | 2 => v.val.testBit 2,
  52   v.val.testBit 3)
  53
  54def flipTime (v : Fin 16) : Fin 16 :=
  55  ⟨v.val ^^^ 8, by
  56    have := v.isLt
  57    interval_cases v.val <;> decide⟩
  58
  59theorem seat_unseat (v : Fin 16) :
  60    seat (unseat v).1 (unseat v).2 = v := by
  61  apply Fin.ext
  62  fin_cases v <;> rfl
  63
  64/-- Packing four bits into a Nat recovers them by `testBit`. -/
  65private theorem pack4_testBit (b0 b1 b2 b3 : Bool) :
  66    let n := bitNat b0 + 2 * bitNat b1 + 4 * bitNat b2 + 8 * bitNat b3
  67    n.testBit 0 = b0 ∧ n.testBit 1 = b1 ∧ n.testBit 2 = b2 ∧ n.testBit 3 = b3 := by
  68  revert b0 b1 b2 b3
  69  decide
  70
  71theorem unseat_seat (p : Pattern 3) (t : Bool) :
  72    unseat (seat p t) = (p, t) := by
  73  have h := pack4_testBit (p 0) (p 1) (p 2) t
  74  refine Prod.ext ?_ ?_
  75  · funext i
  76    fin_cases i
  77    · simpa [unseat, seat, seatNat] using h.1
  78    · simpa [unseat, seat, seatNat] using h.2.1
  79    · simpa [unseat, seat, seatNat] using h.2.2.1
  80  · simpa [unseat, seat, seatNat] using h.2.2.2
  81
  82theorem seat_injective (p₁ p₂ : Pattern 3) (t₁ t₂ : Bool)
  83    (h : seat p₁ t₁ = seat p₂ t₂) : p₁ = p₂ ∧ t₁ = t₂ := by
  84  have := congrArg unseat h
  85  simpa [unseat_seat] using this
  86
  87theorem seat_surjective (v : Fin 16) :
  88    ∃ (p : Pattern 3) (t : Bool), seat p t = v :=
  89  ⟨(unseat v).1, (unseat v).2, seat_unseat v⟩
  90
  91theorem seat_bijective :
  92    Function.Bijective (fun pt : Pattern 3 × Bool => seat pt.1 pt.2) := by
  93  refine ⟨?_, ?_⟩
  94  · intro ⟨p₁, t₁⟩ ⟨p₂, t₂⟩ h
  95    have := seat_injective p₁ p₂ t₁ t₂ h
  96    exact Prod.ext this.1 this.2
  97  · intro v
  98    exact ⟨⟨(unseat v).1, (unseat v).2⟩, seat_unseat v⟩
  99
 100private theorem xor8_lt_eight {n : ℕ} (hn : n < 8) : n ^^^ 8 = n + 8 := by
 101  interval_cases n <;> decide
 102
 103private theorem xor8_add_eight {n : ℕ} (hn : n < 8) : (n + 8) ^^^ 8 = n := by
 104  interval_cases n <;> decide
 105
 106theorem seat_flipTime (p : Pattern 3) (t : Bool) :
 107    seat p (!t) = flipTime (seat p t) := by
 108  apply Fin.ext
 109  have ha : bitNat (p 0) + 2 * bitNat (p 1) + 4 * bitNat (p 2) < 8 := by
 110    have h0 := bitNat_le_one (p 0)
 111    have h1 := bitNat_le_one (p 1)
 112    have h2 := bitNat_le_one (p 2)
 113    omega
 114  cases t
 115  · -- t = false, !t = true
 116    simp only [seat, flipTime, seatNat, bitNat, Bool.not_false]
 117    exact (xor8_lt_eight ha).symm
 118  · simp only [seat, flipTime, seatNat, bitNat, Bool.not_true]
 119    -- LHS: a + 0, RHS: (a + 8) ^^^ 8
 120    simpa [Nat.add_assoc] using (xor8_add_eight ha).symm
 121
 122theorem flipTime_involutive (v : Fin 16) : flipTime (flipTime v) = v := by
 123  apply Fin.ext
 124  change (v.val ^^^ 8) ^^^ 8 = v.val
 125  rw [Nat.xor_assoc, Nat.xor_self, Nat.xor_zero]
 126
 127theorem timeSlice_is_patch_symmetry :
 128    (∀ v, flipTime (flipTime v) = v) ∧
 129      (∀ p t, seat p (!t) = flipTime (seat p t)) :=
 130  ⟨flipTime_involutive, seat_flipTime⟩
 131
 132end Q3PatchSeating
 133end Analysis
 134end Gravity
 135end IndisputableMonolith
 136