import FrcCore.Series
import FrcCore.Theme.Logic
import FrcCore.Theme.SecondOrder
import FrcCore.Theme.Formation

/-!
# FrcCore.Keys.Logic — the keyed theorems of the logic theme (ledger migration, task LM19)

One declaration per key, `FRC.Ledger.p<key>`, generated by `make_keys.py` from the ledgers' Lean bindings: the theorem
that every row carrying the key asserts, proved from the themes alone. The paper's module keeps its declaration
`FRC.<Module>.p<key>` as an alias. Every declaration has no axioms (`check_core_axioms.py`).
-/

namespace FRC.Ledger

-- Keys of the logic theme (generated by make_keys.py from the ledgers' Lean bindings; edit the ledgers, not this file)
/-- p00186 — 00:Z1. G\"odel is vacuous over the finite $\Om$: its theory is complete and decidable, and neither incompleteness theorem has an instance, since $\Om$ interprets no Robinson $\mathsf{Q}$ (25:C1, 25:C2, 25:C3). Incompleteness migrates to the comprehension horizon, the \emph{horizon clause}, as a decomposition (25:G7). Its complexity face is imported (25:G3), its uniform certificate $\Om$-hard (Z3), and its diagonal confined below $t(\M)$ (Z9). -/
theorem p00186 : (∀ (n : Nat) (S : Nat → Nat), (∀ (x : Nat), x < n → S x < n) → (∀ (x y : Nat), x < n → y < n → S x = S y → x = y) → ∀ (z : Nat), z < n → ¬∀ (x : Nat), x < n → S x ≠ z) ∧ (∀ (n : Nat) (D Z : Nat → Bool) (Sg : Nat → Nat → Bool), (∀ (x : Nat), x < n → D x = true → ∃ y, y < n ∧ D y = true ∧ Sg x y = true) → (∀ (x x' y : Nat), x < n → x' < n → D x = true → D x' = true → Sg x y = true → Sg x' y = true → x = x') → (∃ z, z < n ∧ D z = true ∧ Z z = true) → (∀ (x y : Nat), x < n → y < n → D x = true → D y = true → Sg x y = true → Z y = false) → False) ∧ (∀ (M : FRC.Logic.FinStr) (env : Nat → Nat) (δ σ ζ : FRC.Logic.FForm), ¬((∀ (x : Nat), x < M.m → FRC.Logic.Sat M (FRC.Logic.cons x env) δ → ∃ y, y < M.m ∧ FRC.Logic.Sat M (FRC.Logic.cons y env) δ ∧ FRC.Logic.Sat M (FRC.Logic.cons y (FRC.Logic.cons x env)) σ) ∧ (∀ (x x' y : Nat), x < M.m → x' < M.m → FRC.Logic.Sat M (FRC.Logic.cons x env) δ → FRC.Logic.Sat M (FRC.Logic.cons x' env) δ → FRC.Logic.Sat M (FRC.Logic.cons y (FRC.Logic.cons x env)) σ → FRC.Logic.Sat M (FRC.Logic.cons y (FRC.Logic.cons x' env)) σ → x = x') ∧ (∃ z, z < M.m ∧ FRC.Logic.Sat M (FRC.Logic.cons z env) δ ∧ FRC.Logic.Sat M (FRC.Logic.cons z env) ζ) ∧ ∀ (x y : Nat), x < M.m → y < M.m → FRC.Logic.Sat M (FRC.Logic.cons x env) δ → FRC.Logic.Sat M (FRC.Logic.cons y env) δ → FRC.Logic.Sat M (FRC.Logic.cons y (FRC.Logic.cons x env)) σ → ¬FRC.Logic.Sat M (FRC.Logic.cons y env) ζ)) ∧ (∀ (M : FRC.Logic.FinStr) (φ : FRC.Logic.FForm) (env : Nat → Nat), FRC.Logic.fval M env φ = true ↔ FRC.Logic.Sat M env φ) ∧ (∀ (M : FRC.Logic.FinStr) (φ : FRC.Logic.FForm) (env : Nat → Nat), FRC.Logic.Sat M env φ ∨ FRC.Logic.Sat M env φ.neg) ∧ ∀ (M : FRC.Logic.FinStr) (φ : FRC.Logic.FForm) (env : Nat → Nat), ¬(FRC.Logic.Sat M env φ ∧ FRC.Logic.Sat M env φ.neg) :=
  And.intro @FRC.Logic.no_finite_successor (And.intro @FRC.Logic.no_finite_Q (And.intro @FRC.Logic.no_interpretation (And.intro @FRC.Logic.fin_theory_decidable (And.intro @FRC.Logic.fin_theory_complete (@FRC.Logic.fin_theory_consistent)))))
/-- p05013 — 5:C2, 29:C10. The pigeonhole (O3): an agent with fewer than $s^{K+1}$ records in a frame of $M>s^{K+1}$ formations holds no injective representation of it, so the frame's cardinality is not certifiable from within. Counterparts 25:D1, 00:A4. -/
theorem p05013 : (∀ (s : Nat), (2 : Nat) ≤ s → ∀ (K : Nat), FRC.Logic.records s K < s ^ (K + (1 : Nat))) ∧ ∀ {N R : Nat}, R < N → ∀ (f : Nat → Nat), (∀ (i : Nat), i < N → f i < R) → (∀ (i j : Nat), i < N → j < N → f i = f j → i = j) → False :=
  And.intro @FRC.Logic.records_lt (@FRC.Logic.no_mirror)
/-- p05016 — 5:C5. Horizon separation: halting for machines of bounded space $K$ is decided from above within $|Q|\,K\,s^{K}$ steps (a configuration repeats) and never from within (diagonalisation); Turing's theorem is an external non-existence theorem, classified with Cantor's, not an instance of the bundle. -/
theorem p05016 : (∀ (f : Nat → Nat) (n : Nat), (∀ (y : Nat), y < n → f y < n) → ∀ (x : Nat), x < n → ∃ i j, i < j ∧ j ≤ n ∧ FRC.Logic.iter f x i = FRC.Logic.iter f x j) ∧ ∀ (f : Nat → Nat) (n : Nat), (∀ (y : Nat), y < n → f y < n) → ∀ (h x : Nat), x < n → ((∃ k, FRC.Logic.iter f x k = h) ↔ ∃ k, k ≤ n ∧ FRC.Logic.iter f x k = h) :=
  And.intro @FRC.Logic.repeat_below (@FRC.Logic.halts_iff_halts_below)
/-- p05019 — 5:D3. Diagonal normal form: $\{$Eff, Cns, Cmp, IR$\}$ inconsistent (B2), Tarski a variant with the truth predicate for Cmp; the diagonal is a theorem when external --- Cantor's theorem, $n<2^{n}$ on every frame, uncountability, halting --- and a paradox engine only over an internalised registry with completeness demanded. -/
theorem p05019 : ∀ (n : Nat), n < (2 : Nat) ^ n :=
  @FRC.Logic.cantor_finite
/-- p05027 — 5:E1. Global choice on a finite universe: with a canonical order, $\operatorname{ch}(A)=\min A$ is a uniform pointwise choice rule; over a fixed finite base AC is a definable theorem; finite products are nonempty without it. -/
theorem p05027 : (∀ (P : Nat → Bool) (n x : Nat), FRC.Logic.leastBelow P n = some x → x < n ∧ P x = true ∧ ∀ (y : Nat), y < x → P y = false) ∧ ∀ (P : Nat → Bool) (n x : Nat), x < n → P x = true → ∃ y, FRC.Logic.leastBelow P n = some y :=
  And.intro @FRC.Logic.leastBelow_spec (@FRC.Logic.leastBelow_some)
/-- p05028 — 5:E2. Periodic choice: an equality-periodic family $A_{i+N}=A_i$ has the choice $f(i)=\operatorname{ch}(A_i)$ of the same period; group-periodic families as equivariant surjections $\pi:A\to I$ with equivariant sections. -/
theorem p05028 : ∀ {P Q : Nat → Bool} {n : Nat}, (∀ (x : Nat), x < n → P x = Q x) → FRC.Logic.leastBelow P n = FRC.Logic.leastBelow Q n :=
  @FRC.Logic.leastBelow_congr
/-- p05031 — 5:E5. Periodic K\H{o}nig: in a finite digraph with out-degree $\ge1$ the greedy walk repeats a vertex within $|D|+1$ steps and is eventually periodic with period $\le|D|$ --- the pigeonhole on an iteration over finitely many states. -/
theorem p05031 : (∀ (f : Nat → Nat) (n : Nat), (∀ (y : Nat), y < n → f y < n) → ∀ (x : Nat), x < n → ∃ i j, i < j ∧ j ≤ n ∧ FRC.Logic.iter f x i = FRC.Logic.iter f x j) ∧ ∀ (f : Nat → Nat) (n : Nat), (∀ (y : Nat), y < n → f y < n) → ∀ (x : Nat), x < n → ∃ i p, (0 : Nat) < p ∧ p ≤ n ∧ ∀ (k : Nat), FRC.Logic.iter f x (i + k + p) = FRC.Logic.iter f x (i + k) :=
  And.intro @FRC.Logic.repeat_below (@FRC.Logic.eventually_periodic)
/-- p25010 — 25:C1, 29:B5. Lemma innocence (i): no finite structure interprets $Q$ --- a model of $Q$ has an injective successor with $0$ outside its range, and on a finite set an injective map is onto. $Q$'s successor axioms alone, with no induction, exclude every finite model. -/
theorem p25010 : (∀ (n : Nat) (S : Nat → Nat), (∀ (x : Nat), x < n → S x < n) → (∀ (x y : Nat), x < n → y < n → S x = S y → x = y) → ∀ (z : Nat), z < n → ∃ x, x < n ∧ S x = z) ∧ ∀ (n : Nat) (S : Nat → Nat), (∀ (x : Nat), x < n → S x < n) → (∀ (x y : Nat), x < n → y < n → S x = S y → x = y) → ∀ (z : Nat), z < n → ¬∀ (x : Nat), x < n → S x ≠ z :=
  And.intro @FRC.Logic.inj_onto (@FRC.Logic.no_finite_successor)
/-- p25014 — 25:C5. Tarski scoped: the $m+1$ sentences $\varphi,\neg\varphi,\dots,\neg^{m}\varphi$ outnumber the $m$ elements of $\M$, so every numbering of the sentences by elements of $\M$ gives two of them the same number. Truth in $\M$ is defined externally by a finite table with the evaluation procedure of C2. What fails is the internalisation of truth. -/
theorem p25014 : ∀ (m : Nat) (g : Nat → Nat), (∀ (i : Nat), i < m + (1 : Nat) → g i < m) → ¬∀ (i j : Nat), i < m + (1 : Nat) → j < m + (1 : Nat) → g i = g j → i = j :=
  @FRC.Logic.sentences_outnumber
/-- p25015 — 25:D1. Relational diagonal: an agent of storage capacity $K$ with $a^{K}<m$ has no injective encoding of the elements of $\M$ into its storage states. Every internal representation identifies distinct elements. A fortiori the agent holds no faithful model of $\M$ that also represents the model's own encoding map. -/
theorem p25015 : ∀ {m R : Nat}, R < m → ∀ (ρ : Nat → Nat), (∀ (i : Nat), i < m → ρ i < R) → ¬∀ (i j : Nat), i < m → j < m → ρ i = ρ j → i = j :=
  @FRC.Logic.part_collides
/-- p25048 — 25:F4. Density: $m$ has $d$ base-$a$ digits. An injective coding of length-$n$ strings by $k$-tuples, $k\ge1$, needs $m^{k}\ge a^{n}$, so $n<dk$. In F2's $\delta(u)=\exists v\,(\mathrm{Diag}(u,v)\wedge\theta(v))$ let $v$ have $k$ coordinates and $u$ have $k_{1}$. Each coordinate of $v$ is named three times, each of $u$ once. So $\lvert\delta\rvert\ge2c(k)+c(k+k_{1})$, and $\lambda=\delta(\ulcorner\delta\urcorner)$ has $\lvert\lambda\rvert\ge3c(k)+k_{1}$, $c(j)$ the total length of the $j$ shortest names. -/
theorem p25048 : (∀ {a n m k : Nat} (c : Nat → Nat), (∀ (i : Nat), i < a ^ n → c i < m ^ k) → (∀ (i j : Nat), i < a ^ n → j < a ^ n → c i = c j → i = j) → a ^ n ≤ m ^ k) ∧ ∀ {a n m k d : Nat}, (0 : Nat) < a → m < a ^ d → a ^ n ≤ m ^ (k + (1 : Nat)) → n < d * (k + (1 : Nat)) :=
  And.intro @FRC.Logic.dense_coding (@FRC.Logic.digit_bound)
/-- p29006 — 29:B4. Declining the license is coherent: the finite initial segment with truncated successor, sum and product has a complete, decidable theory and no injective successor missing $0$; on the cycle of $n$ points the successor act is total, returns to its start after $n$ steps, and makes nothing new: every point is already an image. -/
theorem p29006 : (∀ (M : FRC.Logic.FinStr) (φ : FRC.Logic.FForm) (env : Nat → Nat), FRC.Logic.Sat M env φ ∨ FRC.Logic.Sat M env φ.neg) ∧ (∀ (M : FRC.Logic.FinStr) (φ : FRC.Logic.FForm) (env : Nat → Nat), FRC.Logic.fval M env φ = true ↔ FRC.Logic.Sat M env φ) ∧ (∀ (n : Nat) (S : Nat → Nat), (∀ (x : Nat), x < n → S x < n) → (∀ (x y : Nat), x < n → y < n → S x = S y → x = y) → ∀ (z : Nat), z < n → ¬∀ (x : Nat), x < n → S x ≠ z) ∧ (∀ (n : Nat), (0 : Nat) < n → ∀ (x : Nat), FRC.Formation.cyc n x < n) ∧ (∀ (n : Nat), (0 : Nat) < n → ∀ (x : Nat), x < n → FRC.Logic.iter (FRC.Formation.cyc n) x n = x) ∧ ∀ (n : Nat), (0 : Nat) < n → ∀ (z : Nat), z < n → ∃ x, x < n ∧ FRC.Formation.cyc n x = z :=
  And.intro @FRC.Logic.fin_theory_complete (And.intro @FRC.Logic.fin_theory_decidable (And.intro @FRC.Logic.no_finite_successor (And.intro @FRC.Formation.cyc_lt (And.intro @FRC.Formation.cyc_return (@FRC.Formation.cyc_onto)))))
/-- p29007 — 29:B6. Lemma innocence (ii): on $[0,n)$ every nonempty subset has a least element, and a property true at $0$ and closed under successor below $n$ holds below $n$: induction is a theorem of every finite frame, for all subsets. -/
theorem p29007 : (∀ (P : Nat → Bool) (n x : Nat), x < n → P x = true → ∃ y, FRC.Logic.leastBelow P n = some y) ∧ (∀ (P : Nat → Bool) (n x : Nat), FRC.Logic.leastBelow P n = some x → x < n ∧ P x = true ∧ ∀ (y : Nat), y < x → P y = false) ∧ ∀ (n : Nat) (P : Nat → Bool), P (0 : Nat) = true → (∀ (x : Nat), x + (1 : Nat) < n → P x = true → P (x + (1 : Nat)) = true) → ∀ (x : Nat), x < n → P x = true :=
  And.intro @FRC.Logic.leastBelow_some (And.intro @FRC.Logic.leastBelow_spec (@FRC.Formation.finite_induction))
/-- p29010 — 29:C2. Theorem idleness: a check that passes in any universe passes, read by the identity, in the closed finite universe of its own trace, $t(r)$ objects. A record entails nothing that fails there: no count above $t(r)$, no unbounded supply. The sentence ``the universe of formations is infinite'' is certified by no agent at any capacity. -/
theorem p29010 : (∀ (T : FRC.Formation.Trace) (U : FRC.Formation.Universe) (e : Nat → Nat), FRC.Formation.Passes T U e → FRC.Formation.Passes T (FRC.Formation.minimal T) fun i => i) ∧ (∀ (T : FRC.Formation.Trace), (FRC.Formation.minimal T).size = T.t) ∧ ∀ (T : FRC.Formation.Trace), (FRC.Formation.minimal T).Closed :=
  And.intro @FRC.Formation.realized (And.intro @FRC.Formation.minimal_size (@FRC.Formation.minimal_closed))
/-- p29011 — 29:C3. The asymmetry: the check of a trace is decided by exhaustive evaluation of its $t^{2}$ atoms and terminates, and the trace is itself a record of $t^{2}$ symbols, retained when $t^{2}\le K$; bounded structural facts are certifiable, the unbounded supply is not (C2). Cited definitions (not proofs): FRC.Formation.decPasses. -/
theorem p29011 : (∀ (T : FRC.Formation.Trace) (i : Nat), (FRC.Formation.record T i).length = i * T.t) ∧ ∀ (T : FRC.Formation.Trace), (FRC.Formation.record T T.t).length = T.t * T.t :=
  And.intro @FRC.Formation.record_length (@FRC.Formation.record_square)
/-- p29012 — 29:C4. Corollary symmetry, uncertifiability of the bound: a passed check passes after padding by any number $k$ of fresh formations, in a closed realizing universe of exactly $t+k$ objects, so the passing entails no upper bound; with C10, no record fixes the cardinality. -/
theorem p29012 : (∀ (T : FRC.Formation.Trace) (U : FRC.Formation.Universe) (e : Nat → Nat), FRC.Formation.Passes T U e → ∀ (k : Nat), FRC.Formation.Passes T (FRC.Formation.pad U k) e) ∧ ∀ (T : FRC.Formation.Trace) (U : FRC.Formation.Universe) (e : Nat → Nat), FRC.Formation.Passes T U e → ∀ (k : Nat), (FRC.Formation.Passes T (FRC.Formation.pad (FRC.Formation.minimal T) k) fun i => i) ∧ (FRC.Formation.pad (FRC.Formation.minimal T) k).size = T.t + k ∧ (FRC.Formation.pad (FRC.Formation.minimal T) k).Closed :=
  And.intro @FRC.Formation.passes_pad (@FRC.Formation.realization_at_size)
/-- p29014 — 29:C6. Lemma boundary, Case 1: the disjoint double of a closed universe carries the swap, an automorphism without fixed points, of order two; a condition invariant under the swap has an even number of satisfiers, never exactly one; the check passes in the double. -/
theorem p29014 : (∀ (U : FRC.Formation.Universe), U.Closed → ∀ (x : Nat), x < (FRC.Formation.double U).size → (FRC.Formation.double U).form (FRC.Formation.swap U x) = match (FRC.Formation.double U).form x with | some y => some (FRC.Formation.swap U y) | none => none) ∧ (∀ (U : FRC.Formation.Universe) (x : Nat), x < (FRC.Formation.double U).size → FRC.Formation.swap U x ≠ x) ∧ (∀ (U : FRC.Formation.Universe) (x : Nat), x < (FRC.Formation.double U).size → FRC.Formation.swap U (FRC.Formation.swap U x) = x) ∧ (∀ (T : FRC.Formation.Trace) (U : FRC.Formation.Universe) (e : Nat → Nat), FRC.Formation.Passes T U e → FRC.Formation.Passes T (FRC.Formation.double U) e) ∧ (∀ (U : FRC.Formation.Universe) (D : Nat → Bool), (∀ (x : Nat), x < (FRC.Formation.double U).size → D (FRC.Formation.swap U x) = D x) → FRC.Logic.count D (FRC.Formation.double U).size = (2 : Nat) * FRC.Logic.count D U.size) ∧ ∀ (U : FRC.Formation.Universe) (D : Nat → Bool), (∀ (x : Nat), x < (FRC.Formation.double U).size → D (FRC.Formation.swap U x) = D x) → FRC.Logic.count D (FRC.Formation.double U).size ≠ (1 : Nat) :=
  And.intro @FRC.Formation.swap_form (And.intro @FRC.Formation.swap_ne (And.intro @FRC.Formation.swap_swap (And.intro @FRC.Formation.passes_double (And.intro @FRC.Formation.invariant_count_even (@FRC.Formation.no_unique_invariant)))))
/-- p29015 — 29:C7. Lemma boundary, Case 2: the minimal realization holds the trace's objects and nothing else, and a datum the trace never forms has no preimage there: descriptive uniqueness is confined to trace-derived objects, so every presentable object is reachable. -/
theorem p29015 : (∀ (T : FRC.Formation.Trace), (FRC.Formation.minimal T).size = T.t) ∧ ∀ (T : FRC.Formation.Trace) (x : Nat), (∀ (i : Nat), i < T.t → T.atom i x = false) → ∀ (y : Nat), y < T.t → (FRC.Formation.minimal T).form y ≠ some x :=
  And.intro @FRC.Formation.minimal_size (@FRC.Formation.no_preimage_in_minimal)
/-- p29016 — 29:C8. Proposition illusion (i), (ii): the buffer frame of $\sigma$ seeds and $D$ rounds has $\sigma(D+1)$ formations; every object below level $D$ has a fresh image one level up; $k$ acts from a seed reach level $k$ for $k\le D$. Instance $\sigma=2$, $D=17$: $M=36>2\cdot2^{4}$, $D>2^{4}$. -/
theorem p29016 : (∀ (σ D x : Nat), x < σ * (D + (1 : Nat)) → x % (D + (1 : Nat)) < D → (FRC.Formation.buffer σ D).form x = some (x + (1 : Nat))) ∧ (∀ (σ D x : Nat), x < σ * (D + (1 : Nat)) → x % (D + (1 : Nat)) < D → x + (1 : Nat) < σ * (D + (1 : Nat)) ∧ (x + (1 : Nat)) % (D + (1 : Nat)) = x % (D + (1 : Nat)) + (1 : Nat)) ∧ (∀ (σ D s : Nat), s < σ → ∀ (k : Nat), k ≤ D → FRC.Formation.chain σ D s k = some (s * (D + (1 : Nat)) + k)) ∧ (∀ (σ D s k : Nat), s < σ → k < D → ∃ x y, FRC.Formation.chain σ D s k = some x ∧ (FRC.Formation.buffer σ D).form x = some y ∧ FRC.Formation.chain σ D s (k + (1 : Nat)) = some y ∧ x < y ∧ y < (FRC.Formation.buffer σ D).size) ∧ (2 : Nat) * (2 : Nat) ^ ((3 : Nat) + (1 : Nat)) < (FRC.Formation.buffer (2 : Nat) (17 : Nat)).size ∧ (2 : Nat) ^ ((3 : Nat) + (1 : Nat)) < (17 : Nat) :=
  And.intro @FRC.Formation.buffer_forms (And.intro @FRC.Formation.buffer_fresh (And.intro @FRC.Formation.chain_level (And.intro @FRC.Formation.illusion (@FRC.Formation.illusion_instance))))
/-- p29022 — 29:E2. Certificate conservativity: a $\Delta_0$ sentence takes its standard value in every frame beyond its bound (5:B6); every instance of a schema below the bound is decided by evaluation; induction transfers instance-wise (B6). Derivations through infinitary principles are kept as derivability facts: a reading. -/
theorem p29022 : (∀ (N : Nat) (φ : FRC.Logic.Form) (env : Nat → Nat), FRC.Logic.boundF env φ < N → FRC.Logic.evalF? N env φ = FRC.Logic.evalF env φ) ∧ (∀ (M : FRC.Logic.FinStr) (φ : FRC.Logic.FForm) (env : Nat → Nat), FRC.Logic.fval M env φ = true ↔ FRC.Logic.Sat M env φ) ∧ (∀ (n : Nat) (P : Nat → Bool), P (0 : Nat) = true → (∀ (x : Nat), x + (1 : Nat) < n → P x = true → P (x + (1 : Nat)) = true) → ∀ (x : Nat), x < n → P x = true) ∧ ∀ (P : Nat → Bool) (n x : Nat), FRC.Logic.leastBelow P n = some x → x < n ∧ P x = true ∧ ∀ (y : Nat), y < x → P y = false :=
  And.intro @FRC.Logic.stable (And.intro @FRC.Logic.fin_theory_decidable (And.intro @FRC.Formation.finite_induction (@FRC.Logic.leastBelow_spec)))
/-- p29024 — 29:E4. Effective determinacy on a finite frame: subsets and relations are finitely many, and the full second-order theory is decided by exhaustive evaluation over them. The finite direction of 5:D8. -/
theorem p29024 : (∀ (M : FRC.Logic.FinStr) (φ : FRC.Logic.SForm) (env senv renv : Nat → Nat), FRC.Logic.sval2 M env senv renv φ = true ↔ FRC.Logic.Sat2 M env senv renv φ) ∧ (∀ (M : FRC.Logic.FinStr) (φ : FRC.Logic.SForm) (env senv renv : Nat → Nat), FRC.Logic.Sat2 M env senv renv φ ∨ FRC.Logic.Sat2 M env senv renv φ.neg) ∧ ∀ (M : FRC.Logic.FinStr) (φ : FRC.Logic.SForm) (env senv renv : Nat → Nat), ¬(FRC.Logic.Sat2 M env senv renv φ ∧ FRC.Logic.Sat2 M env senv renv φ.neg) :=
  And.intro @FRC.Logic.so_theory_decidable (And.intro @FRC.Logic.so_theory_complete (@FRC.Logic.so_theory_consistent))
/-- p29026 — 29:X1. \textbf{``One can always continue''} is derived, not posited: in a buffered finite frame every act on a reachable object succeeds and no enumeration below the horizon is exhausted (C8), while no check witnesses an end (C6, C7). Rests on C2, C6--C8. -/
theorem p29026 : (∀ (σ D s k : Nat), s < σ → k < D → ∃ x y, FRC.Formation.chain σ D s k = some x ∧ (FRC.Formation.buffer σ D).form x = some y ∧ FRC.Formation.chain σ D s (k + (1 : Nat)) = some y ∧ x < y ∧ y < (FRC.Formation.buffer σ D).size) ∧ (∀ (U : FRC.Formation.Universe) (D : Nat → Bool), (∀ (x : Nat), x < (FRC.Formation.double U).size → D (FRC.Formation.swap U x) = D x) → FRC.Logic.count D (FRC.Formation.double U).size ≠ (1 : Nat)) ∧ ∀ (T : FRC.Formation.Trace) (x : Nat), (∀ (i : Nat), i < T.t → T.atom i x = false) → ∀ (y : Nat), y < T.t → (FRC.Formation.minimal T).form y ≠ some x :=
  And.intro @FRC.Formation.illusion (And.intro @FRC.Formation.no_unique_invariant (@FRC.Formation.no_preimage_in_minimal))
/-- p29027 — 29:X2. \textbf{The finite ontology loses no proof practice:} induction is a theorem of every finite frame (B6) and every executed verification is a bounded instance (E2). Rests on B6, E2. -/
theorem p29027 : (∀ (n : Nat) (P : Nat → Bool), P (0 : Nat) = true → (∀ (x : Nat), x + (1 : Nat) < n → P x = true → P (x + (1 : Nat)) = true) → ∀ (x : Nat), x < n → P x = true) ∧ ∀ (N : Nat) (φ : FRC.Logic.Form) (env : Nat → Nat), FRC.Logic.boundF env φ < N → FRC.Logic.evalF? N env φ = FRC.Logic.evalF env φ :=
  And.intro @FRC.Formation.finite_induction (@FRC.Logic.stable)
-- end keys

end FRC.Ledger