Theme/Formation.lean — FrcCore

1import FrcCore.Theme.Logic23/-!4# Formation universes, traces and bounded certificates (prototype for 29-finitism, 9 October 2026)56The objects of `29-finitism` (The Undeclared Posit of Potential Infinity) in the core's grammar: a universe of7formations is a finite set of objects `0, …, size − 1` with a formation image `form x`, `none` where formation fails;8a trace is what a completed check reads — `t` mentioned objects and the formation atoms it asserts among them; a check9passes in a universe under a reading of its objects. No imports beyond the logic theme; no axioms.10-/1112namespace FRC.Formation1314/-- A universe of formations: `size` objects and the formation image `form x` of each (`none`: the act fails at `x`). -/15structure Universe where16  size : Nat17  form : Nat → Option Nat1819/-- Closed: every formation image is an object of the universe. -/20def Universe.Closed (U : Universe) : Prop := ∀ x y, x < U.size → U.form x = some y → y < U.size2122/-- The trace of a completed check: `t` mentioned objects `0, …, t − 1` and the formation atoms it asserts,23`atom i j = true` reading "the formation image of `i` is `j`". -/24structure Trace where25  t : Nat26  atom : Nat → Nat → Bool2728/-- The check passes in `U` under the reading `e`: the mentioned objects are distinct objects of `U` and every asserted29formation holds there. The check reads nothing else (the locality clause of Definition agent). -/30def Passes (T : Trace) (U : Universe) (e : Nat → Nat) : Prop :=31  (∀ i, i < T.t → e i < U.size) ∧32  (∀ i j, i < T.t → j < T.t → e i = e j → i = j) ∧33  (∀ i j, i < T.t → j < T.t → T.atom i j = true → U.form (e i) = some (e j))3435/-! ### Theorem idleness — every passed check passes in a finite universe of its trace's size -/3637/-- The minimal realization: exactly the trace's objects, each formed to the least object the trace asserts for it. -/38def minimal (T : Trace) : Universe :=39  ⟨T.t, fun i => Logic.leastBelow (fun j => T.atom i j) T.t⟩4041/-- 29:C2, 29:C7 — the minimal realization has exactly the trace's `t` objects. -/42theorem minimal_size (T : Trace) : (minimal T).size = T.t := rfl4344/-- A passed check asserts at most one image per object: the atoms are functional on the trace. -/45theorem atoms_functional (T : Trace) (U : Universe) (e : Nat → Nat) (h : Passes T U e) :46    ∀ i j j', i < T.t → j < T.t → j' < T.t → T.atom i j = true → T.atom i j' = true → j = j' :=47  fun i j j' hi hj hj' ha ha' =>48    have e1 := h.2.2 i j hi hj ha49    have e2 := h.2.2 i j' hi hj' ha'50    h.2.1 j j' hj hj' (Option.some.inj (e1.symm.trans e2))5152/-- 29:C2 — Theorem idleness (the core form): a check that passes anywhere passes in the finite universe of its own53trace, read by the identity: `t(r)` objects suffice. -/54theorem realized (T : Trace) (U : Universe) (e : Nat → Nat) (h : Passes T U e) :55    Passes T (minimal T) (fun i => i) := by56  refine ⟨fun i hi => hi, fun i j _ _ hij => hij, fun i j hi hj ha => ?_⟩57  show Logic.leastBelow (fun k => T.atom i k) T.t = some j58  obtain ⟨y, hy⟩ := Logic.leastBelow_some (fun k => T.atom i k) T.t j hj ha59  have sp := Logic.leastBelow_spec (fun k => T.atom i k) T.t y hy60  rw [hy, atoms_functional T U e h i y j hi sp.1 hj sp.2.1 ha]6162/-- 29:C2 — the minimal realization is closed: every image it assigns is one of its objects. -/63theorem minimal_closed (T : Trace) : (minimal T).Closed := fun x y _ hxy =>64  (Logic.leastBelow_spec (fun k => T.atom x k) T.t y hxy).16566/-! ### Corollary symmetry (the bound clause) — padding: the check passes in universes of every larger size -/6768/-- `U` with `k` fresh objects appended, formation failing at each. -/69def pad (U : Universe) (k : Nat) : Universe :=70  ⟨U.size + k, fun x => if x < U.size then U.form x else none⟩7172theorem pad_size (U : Universe) (k : Nat) : (pad U k).size = U.size + k := rfl7374theorem pad_form (U : Universe) (k x : Nat) (hx : x < U.size) : (pad U k).form x = U.form x := by75  show (if x < U.size then U.form x else none) = U.form x76  rw [ite_eq_left hx]7778/-- 29:C4 — Corollary symmetry, the bound: a passed check passes unchanged after padding by any number of formations,79so for every `B` there is a realizing universe of more than `B` objects and the passing entails no bound. -/80theorem passes_pad (T : Trace) (U : Universe) (e : Nat → Nat) (h : Passes T U e) (k : Nat) :81    Passes T (pad U k) e := by82  refine ⟨fun i hi => Nat.lt_of_lt_of_le (h.1 i hi) (Nat.le_add_right _ _), h.2.1, fun i j hi hj ha => ?_⟩83  rw [pad_form U k (e i) (h.1 i hi)]; exact h.2.2 i j hi hj ha8485/-- 29:C4 — the realization at every size: for every `k` the minimal realization padded by `k` fresh formations has86exactly `t + k` objects, is closed, and the check passes in it read by the identity. No size is entailed. -/87theorem realization_at_size (T : Trace) (U : Universe) (e : Nat → Nat) (h : Passes T U e) (k : Nat) :88    Passes T (pad (minimal T) k) (fun i => i) ∧ (pad (minimal T) k).size = T.t + k ∧ (pad (minimal T) k).Closed :=89  ⟨passes_pad T (minimal T) _ (realized T U e h) k, rfl, fun x y hx hxy => by90    have hxy' : (if x < T.t then (minimal T).form x else none) = some y := hxy91    match Nat.lt_or_ge x T.t with92    | .inl hlt =>93      rw [ite_eq_left hlt] at hxy'94      exact Nat.lt_of_lt_of_le (minimal_closed T x y hlt hxy') (Nat.le_add_right _ _)95    | .inr hge =>96      rw [ite_eq_right (Nat.not_lt.2 hge)] at hxy'97      cases hxy'⟩9899/-! ### The cyclic exhibit of Proposition posits — the successor act on the cycle of `n` points -/100101/-- The successor on the cycle of `n` points: `x ↦ x + 1 (mod n)`. -/102def cyc (n x : Nat) : Nat := (x + 1) % n103104/-- 29:B4 — the act is total: it stays on the cycle. -/105theorem cyc_lt (n : Nat) (hn : 0 < n) (x : Nat) : cyc n x < n := FRC.Nat.mod_lt' _ hn106107theorem cyc_iter (n : Nat) (hn : 0 < n) (x : Nat) (hx : x < n) : ∀ k, Logic.iter (cyc n) x k = (x + k) % n108  | 0 => (FRC.Nat.mod_eq_of_lt hx).symm109  | k + 1 => by110    show cyc n (Logic.iter (cyc n) x k) = (x + (k + 1)) % n111    rw [cyc_iter n hn x hx k]112    show ((x + k) % n + 1) % n = (x + (k + 1)) % n113    rw [FRC.Nat.mod_add_mod _ _ _ hn, Nat.add_assoc]114115/-- 29:B4 — the act returns to its start after `n` steps: the orbit is a cycle, so iteration makes nothing new. -/116theorem cyc_return (n : Nat) (hn : 0 < n) (x : Nat) (hx : x < n) : Logic.iter (cyc n) x n = x := by117  rw [cyc_iter n hn x hx n, Nat.add_comm]118  have : (n + x) % n = (n * 1 + x) % n := by rw [Nat.mul_one]119  rw [this, FRC.Nat.add_mul_mod_self_left x 1 n hn, FRC.Nat.mod_eq_of_lt hx]120121/-- The act is injective on the cycle. -/122theorem cyc_inj (n : Nat) (hn : 0 < n) : ∀ x y, x < n → y < n → cyc n x = cyc n y → x = y := fun x y hx hy e => by123  have key : ∀ z, z < n → cyc n z = if z + 1 < n then z + 1 else 0 := fun z hz => by124    show (z + 1) % n = _125    by_cases h : z + 1 < n126    · rw [ite_eq_left h]; exact FRC.Nat.mod_eq_of_lt h127    · rw [ite_eq_right h]128      have : z + 1 = n := Nat.le_antisymm (Nat.succ_le_of_lt hz) (Nat.le_of_not_lt h)129      rw [this]; exact FRC.Nat.mod_self n hn130  rw [key x hx, key y hy] at e131  by_cases h1 : x + 1 < n <;> by_cases h2 : y + 1 < n132  · rw [ite_eq_left h1, ite_eq_left h2] at e; exact Nat.succ.inj e133  · rw [ite_eq_left h1, ite_eq_right h2] at e; exact absurd e (Nat.succ_ne_zero x)134  · rw [ite_eq_right h1, ite_eq_left h2] at e; exact absurd e.symm (Nat.succ_ne_zero y)135  · have ex : x + 1 = n := Nat.le_antisymm (Nat.succ_le_of_lt hx) (Nat.le_of_not_lt h1)136    have ey : y + 1 = n := Nat.le_antisymm (Nat.succ_le_of_lt hy) (Nat.le_of_not_lt h2)137    exact Nat.succ.inj (ex.trans ey.symm)138139/-- 29:B4 — every point of the cycle is already an image: the act produces no new formation (the pigeonhole, `inj_onto`). -/140theorem cyc_onto (n : Nat) (hn : 0 < n) (z : Nat) (hz : z < n) : ∃ x, x < n ∧ cyc n x = z :=141  Logic.inj_onto n (cyc n) (fun x _ => cyc_lt n hn x) (cyc_inj n hn) z hz142143/-! ### Lemma boundary, Case 1 — the disjoint double, its swap, and the parity of invariant conditions -/144145/-- The disjoint double `U ⊔ U`: the objects `x < n` the first copy, `n + x` the second, each formed inside its copy. -/146def double (U : Universe) : Universe :=147  ⟨U.size + U.size, fun x => if x < U.size then U.form x148    else match U.form (x - U.size) with | some y => some (U.size + y) | none => none⟩149150/-- The swap of the two copies. -/151def swap (U : Universe) (x : Nat) : Nat := if x < U.size then U.size + x else x - U.size152153theorem swap_lt (U : Universe) (x : Nat) (hx : x < (double U).size) : swap U x < (double U).size := by154  show (if x < U.size then U.size + x else x - U.size) < U.size + U.size155  by_cases h : x < U.size156  · rw [ite_eq_left h]; exact Nat.add_lt_add_left h _157  · rw [ite_eq_right h]158    exact Nat.lt_of_lt_of_le (FRC.Nat.sub_lt_of_lt_add hx (Nat.le_of_not_lt h)) (Nat.le_add_left _ _)159160/-- 29:C6 — the swap is an involution. -/161theorem swap_swap (U : Universe) (x : Nat) (hx : x < (double U).size) : swap U (swap U x) = x := by162  show (if (if x < U.size then U.size + x else x - U.size) < U.size then U.size + (if x < U.size then U.size + x else x - U.size)163        else (if x < U.size then U.size + x else x - U.size) - U.size) = x164  by_cases h : x < U.size165  · rw [ite_eq_left h]166    have : ¬ U.size + x < U.size := Nat.not_lt.2 (Nat.le_add_right _ _)167    rw [ite_eq_right this, FRC.Nat.add_sub_cancel_left]168  · rw [ite_eq_right h]169    have hlt : x - U.size < U.size := FRC.Nat.sub_lt_of_lt_add hx (Nat.le_of_not_lt h)170    rw [ite_eq_left hlt, FRC.Nat.add_sub_of_le (Nat.le_of_not_lt h)]171172/-- 29:C6 — the swap moves every object: no fixed point. -/173theorem swap_ne (U : Universe) (x : Nat) (hx : x < (double U).size) : swap U x ≠ x := by174  show (if x < U.size then U.size + x else x - U.size) ≠ x175  by_cases h : x < U.size176  · rw [ite_eq_left h]; intro e177    have : U.size + x = 0 + x := by rw [Nat.zero_add]; exact e178    exact Nat.lt_irrefl 0 (Nat.lt_of_lt_of_le (Nat.lt_of_le_of_lt (Nat.zero_le _) h) (Nat.le_of_eq (FRC.Nat.add_right_cancel this)))179  · rw [ite_eq_right h]; intro e180    have hx2 : x < U.size + U.size := hx181    have hpos : 0 < U.size := match hU0 : U.size, hx2 with182      | 0, hx0 => absurd hx0 (Nat.not_lt_zero x)183      | m + 1, _ => Nat.succ_pos m184    have : x - U.size < x := Nat.sub_lt (Nat.lt_of_lt_of_le hpos (Nat.le_of_not_lt h)) hpos185    rw [e] at this; exact Nat.lt_irrefl x this186187theorem double_form_left (U : Universe) (x : Nat) (hx : x < U.size) : (double U).form x = U.form x := by188  show (if x < U.size then U.form x else _) = U.form x189  rw [ite_eq_left hx]190191theorem double_form_right (U : Universe) (x : Nat) (_hx : x < U.size) :192    (double U).form (U.size + x) = match U.form x with | some y => some (U.size + y) | none => none := by193  show (if U.size + x < U.size then _ else match U.form (U.size + x - U.size) with | some y => some (U.size + y) | none => none) = _194  have : ¬ U.size + x < U.size := Nat.not_lt.2 (Nat.le_add_right _ _)195  rw [ite_eq_right this, FRC.Nat.add_sub_cancel_left]196197theorem double_form_right' (U : Universe) (x : Nat) (h : ¬ x < U.size) :198    (double U).form x = match U.form (x - U.size) with | some y => some (U.size + y) | none => none := by199  show (if x < U.size then _ else match U.form (x - U.size) with | some y => some (U.size + y) | none => none) = _200  rw [ite_eq_right h]201202/-- 29:C6 — the swap is an automorphism of the double: it commutes with formation. -/203theorem swap_form (U : Universe) (hU : U.Closed) (x : Nat) (hx : x < (double U).size) :204    (double U).form (swap U x) = match (double U).form x with | some y => some (swap U y) | none => none := by205  by_cases h : x < U.size206  · have hs : swap U x = U.size + x := by show (if x < U.size then _ else _) = _; rw [ite_eq_left h]207    rw [hs, double_form_right U x h, double_form_left U x h]208    match hf : U.form x with209    | none => rfl210    | some y =>211      have hy : y < U.size := hU x y h hf212      show some (U.size + y) = some (if y < U.size then U.size + y else y - U.size)213      rw [ite_eq_left hy]214  · have hxs : x - U.size < U.size := FRC.Nat.sub_lt_of_lt_add hx (Nat.le_of_not_lt h)215    have hs : swap U x = x - U.size := by show (if x < U.size then _ else _) = _; rw [ite_eq_right h]216    rw [hs, double_form_left U _ hxs, double_form_right' U x h]217    match hf : U.form (x - U.size) with218    | none => rfl219    | some y =>220      show some y = some (if U.size + y < U.size then _ else U.size + y - U.size)221      have : ¬ U.size + y < U.size := Nat.not_lt.2 (Nat.le_add_right _ _)222      rw [ite_eq_right this, FRC.Nat.add_sub_cancel_left]223224/-- 29:C6 — a passed check passes in the double, read in the first copy. -/225theorem passes_double (T : Trace) (U : Universe) (e : Nat → Nat) (h : Passes T U e) : Passes T (double U) e := by226  refine ⟨fun i hi => Nat.lt_of_lt_of_le (h.1 i hi) (Nat.le_add_right _ _), h.2.1, fun i j hi hj ha => ?_⟩227  rw [double_form_left U (e i) (h.1 i hi)]; exact h.2.2 i j hi hj ha228229/-- Counting over two blocks. -/230theorem count_add (f : Nat → Bool) (a : Nat) : ∀ b, Logic.count f (a + b) = Logic.count f a + Logic.count (fun i => f (a + i)) b231  | 0 => rfl232  | b + 1 => by233    show Logic.count f (a + b) + cond (f (a + b)) 1 0 = Logic.count f a + (Logic.count (fun i => f (a + i)) b + cond (f (a + b)) 1 0)234    rw [count_add f a b, Nat.add_assoc]235236theorem count_congr {f g : Nat → Bool} : ∀ {n : Nat}, (∀ i, i < n → f i = g i) → Logic.count f n = Logic.count g n237  | 0, _ => rfl238  | n + 1, h => by239    show Logic.count f n + cond (f n) 1 0 = Logic.count g n + cond (g n) 1 0240    rw [count_congr (fun i hi => h i (Nat.lt_succ_of_lt hi)), h n (Nat.lt_succ_self n)]241242/-- 29:C6 — Lemma boundary, Case 1: a condition invariant under the swap has an even number of satisfiers in the double,243its satisfiers come in pairs. -/244theorem invariant_count_even (U : Universe) (D : Nat → Bool)245    (hD : ∀ x, x < (double U).size → D (swap U x) = D x) :246    Logic.count D (double U).size = 2 * Logic.count D U.size := by247  show Logic.count D (U.size + U.size) = 2 * Logic.count D U.size248  rw [count_add D U.size U.size, Nat.two_mul]249  have : ∀ i, i < U.size → D (U.size + i) = D i := fun i hi => by250    have hs : swap U i = U.size + i := by show (if i < U.size then _ else _) = _; rw [ite_eq_left hi]251    rw [← hs]; exact hD i (Nat.lt_of_lt_of_le hi (Nat.le_add_right _ _))252  rw [count_congr this]253254/-- 29:C6, 29:X1 — a swap-invariant condition has zero or at least two satisfiers, never exactly one. -/255theorem no_unique_invariant (U : Universe) (D : Nat → Bool)256    (hD : ∀ x, x < (double U).size → D (swap U x) = D x) : Logic.count D (double U).size ≠ 1 := by257  rw [invariant_count_even U D hD]258  intro h259  cases hc : Logic.count D U.size with260  | zero => rw [hc] at h; exact Nat.noConfusion h261  | succ c => rw [hc, Nat.mul_succ] at h; exact Nat.noConfusion (Nat.succ.inj h)262263/-! ### Lemma boundary, Case 2 — the minimal realization confines satisfiers to the trace -/264265/-- 29:C7, 29:X1 — Lemma boundary, Case 2: in the minimal realization a datum the trace never forms has no preimage,266so the backward condition "the object whose formation image is `x`" has zero satisfiers. -/267theorem no_preimage_in_minimal (T : Trace) (x : Nat) (hx : ∀ i, i < T.t → T.atom i x = false) :268    ∀ y, y < T.t → (minimal T).form y ≠ some x := fun y hy e =>269  have sp := Logic.leastBelow_spec (fun k => T.atom y k) T.t x e270  Bool.noConfusion ((hx y hy).symm.trans sp.2.1)271272/-! ### Lemma innocence (ii) — induction is a theorem of every finite frame -/273274/-- 29:B6, 29:E2, 29:X2 — Lemma innocence (ii): on the finite frame `[0, n)` the induction schema holds for every275property, from the least-number principle (`leastBelow`): a property true at `0` and closed under successor below `n`276holds below `n`. -/277theorem finite_induction (n : Nat) (P : Nat → Bool) (h0 : P 0 = true)278    (hs : ∀ x, x + 1 < n → P x = true → P (x + 1) = true) : ∀ x, x < n → P x = true := fun x hx => by279  match hP : P x with280  | true => rfl281  | false =>282    exfalso283    obtain ⟨m, hm⟩ := Logic.leastBelow_some (fun y => !P y) n x hx (by rw [hP]; rfl)284    have sp := Logic.leastBelow_spec (fun y => !P y) n m hm285    cases m with286    | zero => have := sp.2.1; rw [h0] at this; exact Bool.noConfusion this287    | succ k =>288      have hk : P k = true := by289        have := sp.2.2 k (Nat.lt_succ_self k)290        match hPk : P k with291        | true => rfl292        | false => rw [hPk] at this; exact Bool.noConfusion this293      have := sp.2.1; rw [hs k sp.1 hk] at this; exact Bool.noConfusion this294295/-! ### Proposition illusion — the buffer frame -/296297/-- The buffer frame: `σ` seeds, each the root of a chain of `D` formations; object `s (D + 1) + k` is seed `s` at298level `k ≤ D`; formation steps up the chain and fails at the top. -/299def buffer (σ D : Nat) : Universe :=300  ⟨σ * (D + 1), fun x => if x % (D + 1) < D ∧ x < σ * (D + 1) then some (x + 1) else none⟩301302theorem buffer_size (σ D : Nat) : (buffer σ D).size = σ * (D + 1) := rfl303304/-- 29:C8 — every object below the top level has a formation image: the act succeeds at every level `k < D`. -/305theorem buffer_forms (σ D x : Nat) (hx : x < σ * (D + 1)) (hk : x % (D + 1) < D) :306    (buffer σ D).form x = some (x + 1) := by307  show (if x % (D + 1) < D ∧ x < σ * (D + 1) then some (x + 1) else none) = some (x + 1)308  rw [ite_eq_left ⟨hk, hx⟩]309310/-- 29:C8 — the image is fresh: one level up, inside the frame. -/311theorem buffer_fresh (σ D x : Nat) (hx : x < σ * (D + 1)) (hk : x % (D + 1) < D) :312    x + 1 < σ * (D + 1) ∧ (x + 1) % (D + 1) = x % (D + 1) + 1 := by313  have hD : 0 < D + 1 := Nat.succ_pos D314  obtain ⟨q, hq⟩ := FRC.Nat.mod_spec (D + 1) hD x315  have hr : x % (D + 1) + 1 < D + 1 := Nat.add_lt_add_right hk 1316  have e : x + 1 = (D + 1) * q + (x % (D + 1) + 1) := by rw [← Nat.add_assoc, ← hq]317  refine ⟨?_, FRC.Nat.mod_unique hr e⟩318  -- x + 1 < σ(D+1): x lies in block q, x + 1 stays in block q since its residue is below D + 1319  have hq' : q < σ := match Nat.lt_or_ge q σ with320    | .inl hlt => hlt321    | .inr hσ =>322      have h1 : σ * (D + 1) ≤ (D + 1) * q := by rw [Nat.mul_comm]; exact Nat.mul_le_mul_left _ hσ323      have h2 : (D + 1) * q ≤ x := by rw [hq]; exact Nat.le_add_right _ _324      absurd (Nat.lt_of_lt_of_le hx (Nat.le_trans h1 h2)) (Nat.lt_irrefl x)325  rw [e]326  calc (D + 1) * q + (x % (D + 1) + 1) < (D + 1) * q + (D + 1) := Nat.add_lt_add_left hr _327    _ = (D + 1) * (q + 1) := by rw [Nat.mul_succ]328    _ ≤ (D + 1) * σ := Nat.mul_le_mul_left _ hq'329    _ = σ * (D + 1) := Nat.mul_comm _ _330331/-- The levels reached by iterating formation from a seed: `k` acts from seed `s` reach level `k`, for `k ≤ D`. -/332def chain (σ D s : Nat) : Nat → Option Nat333  | 0 => some (s * (D + 1))334  | k + 1 => match chain σ D s k with | some x => (buffer σ D).form x | none => none335336/-- 29:C8 — `k` acts from seed `s` reach level `k`, for `k ≤ D`. -/337theorem chain_level (σ D s : Nat) (hs : s < σ) : ∀ k, k ≤ D → chain σ D s k = some (s * (D + 1) + k)338  | 0, _ => rfl339  | k + 1, hk => by340    show (match chain σ D s k with | some x => (buffer σ D).form x | none => none) = some (s * (D + 1) + (k + 1))341    rw [chain_level σ D s hs k (Nat.le_of_succ_le hk)]342    have hD : 0 < D + 1 := Nat.succ_pos D343    have hmod : (s * (D + 1) + k) % (D + 1) = k :=344      FRC.Nat.mod_unique (Nat.lt_of_lt_of_le (Nat.lt_succ_of_le (Nat.le_of_succ_le hk)) (Nat.le_refl _)) (by rw [Nat.mul_comm])345    have hlt : s * (D + 1) + k < σ * (D + 1) :=346      calc s * (D + 1) + k < s * (D + 1) + (D + 1) := Nat.add_lt_add_left (Nat.lt_succ_of_le (Nat.le_of_succ_le hk)) _347        _ = (s + 1) * (D + 1) := by rw [Nat.succ_mul]348        _ ≤ σ * (D + 1) := Nat.mul_le_mul_right _ hs349    show (buffer σ D).form (s * (D + 1) + k) = some (s * (D + 1) + (k + 1))350    rw [buffer_forms σ D _ hlt (by rw [hmod]; exact Nat.lt_of_succ_le hk)]351    rfl352353/-- 29:C8, 29:X1 — Proposition illusion (i), (ii) in the core: in the buffer frame of `σ` seeds and `D` rounds, every354object reached by fewer than `D` acts from a seed has a formation image, and the image is one level further: no act on355a reachable object fails and no enumeration below the horizon `D` is exhausted. -/356theorem illusion (σ D s k : Nat) (hs : s < σ) (hk : k < D) :357    ∃ x y, chain σ D s k = some x ∧ (buffer σ D).form x = some y ∧ chain σ D s (k + 1) = some y ∧ x < y ∧358      y < (buffer σ D).size := by359  have hx := chain_level σ D s hs k (Nat.le_of_lt hk)360  have hy := chain_level σ D s hs (k + 1) hk361  refine ⟨s * (D + 1) + k, s * (D + 1) + (k + 1), hx, ?_, hy, Nat.lt_succ_self _, ?_⟩362  · have hmod : (s * (D + 1) + k) % (D + 1) = k :=363      FRC.Nat.mod_unique (Nat.lt_succ_of_lt hk) (by rw [Nat.mul_comm])364    have hlt : s * (D + 1) + k < σ * (D + 1) :=365      calc s * (D + 1) + k < s * (D + 1) + (D + 1) := Nat.add_lt_add_left (Nat.lt_succ_of_lt hk) _366        _ = (s + 1) * (D + 1) := by rw [Nat.succ_mul]367        _ ≤ σ * (D + 1) := Nat.mul_le_mul_right _ hs368    rw [buffer_forms σ D _ hlt (by rw [hmod]; exact hk)]; rfl369  · calc s * (D + 1) + (k + 1) < s * (D + 1) + (D + 1) := Nat.add_lt_add_left (Nat.succ_lt_succ hk) _370      _ = (s + 1) * (D + 1) := by rw [Nat.succ_mul]371      _ ≤ σ * (D + 1) := Nat.mul_le_mul_right _ hs372373/-- 29:C8 — the frame's cardinality clause of Proposition illusion at an instance: two seeds, `D = 17 > 2^4`, so374`M = 36 > 2 · 2^{3+1}` for an agent of capacity `3` over two letters — decided by the kernel. -/375theorem illusion_instance : 2 * 2 ^ (3 + 1) < (buffer 2 17).size ∧ 2 ^ (3 + 1) < 17 := by decide376377/-! ### Corollary asymmetry — a check terminates, and a trace is itself a bounded record -/378379/-- 29:C3 — the check of a trace in a universe under a reading is decided by exhaustive evaluation over the `t` objects380and the `t²` atoms: a completed check is a terminating computation. -/381def decPasses (T : Trace) (U : Universe) (e : Nat → Nat) : Decidable (Passes T U e) :=382  have d1 : Decidable (∀ i, i < T.t → e i < U.size) := FRC.Shell.decForallLT (fun i => e i < U.size) T.t383  have d2' : Decidable (∀ i, i < T.t → ∀ j, j < T.t → e i = e j → i = j) :=384    @FRC.Shell.decForallLT (fun i => ∀ j, j < T.t → e i = e j → i = j)385      (fun i => @FRC.Shell.decForallLT (fun j => e i = e j → i = j) (fun _ => inferInstance) T.t) T.t386  have d2 : Decidable (∀ i j, i < T.t → j < T.t → e i = e j → i = j) :=387    @decidable_of_iff _ _ ⟨fun h i j hi hj => h i hi j hj, fun h i hi j hj => h i j hi hj⟩ d2'388  have d3' : Decidable (∀ i, i < T.t → ∀ j, j < T.t → T.atom i j = true → U.form (e i) = some (e j)) :=389    @FRC.Shell.decForallLT (fun i => ∀ j, j < T.t → T.atom i j = true → U.form (e i) = some (e j))390      (fun i => @FRC.Shell.decForallLT (fun j => T.atom i j = true → U.form (e i) = some (e j)) (fun _ => inferInstance) T.t) T.t391  have d3 : Decidable (∀ i j, i < T.t → j < T.t → T.atom i j = true → U.form (e i) = some (e j)) :=392    @decidable_of_iff _ _ ⟨fun h i j hi hj => h i hi j hj, fun h i hi j hj => h i j hi hj⟩ d3'393  @instDecidableAnd _ _ d1 (@instDecidableAnd _ _ d2 d3)394395/-- The entries `f 0, …, f (n − 1)` as a list. -/396def rowList (f : Nat → Bool) : Nat → List Bool397  | 0 => []398  | n + 1 => rowList f n ++ [f n]399400theorem length_append (l m : List Bool) : (l ++ m).length = l.length + m.length := by401  induction l with402  | nil => show m.length = 0 + m.length; rw [Nat.zero_add]403  | cons a l ih => show (l ++ m).length + 1 = (l.length + 1) + m.length; rw [ih, Nat.succ_add]404405theorem rowList_length (f : Nat → Bool) : ∀ n, (rowList f n).length = n406  | 0 => rfl407  | n + 1 => by show (rowList f n ++ [f n]).length = n + 1; rw [length_append, rowList_length f n]; rfl408409/-- The atom table of a trace, row by row: the record that encodes the check. -/410def record (T : Trace) : Nat → List Bool411  | 0 => []412  | i + 1 => record T i ++ rowList (T.atom i) T.t413414/-- 29:C3 — Corollary asymmetry: a trace of `t` objects is a record of `t²` symbols, a bounded structural fact has a415certifying record, retained by every agent whose capacity covers it. -/416theorem record_length (T : Trace) : ∀ i, (record T i).length = i * T.t417  | 0 => by rw [Nat.zero_mul]; rfl418  | i + 1 => by419    show (record T i ++ rowList (T.atom i) T.t).length = (i + 1) * T.t420    rw [length_append, record_length T i, rowList_length, Nat.succ_mul]421422/-- 29:C3 — the record of the whole trace has `t²` symbols. -/423theorem record_square (T : Trace) : (record T T.t).length = T.t * T.t := record_length T T.t424425end FRC.Formation426