Finitism.lean — FrcCore

1import FrcCore.Keys.Logic2import FrcCore.Keys.Foundation34/-!5# FrcCore.Finitism — 29-finitism predicates on the core67The predicates of *The Undeclared Posit of Potential Infinity* (29-finitism) that the core proves with no axioms,8named by their accession keys below and proved in the modules this one imports through the key files: the logic9theme's `Theme/Formation` (formation universes, traces and bounded certificates: the minimal realization of10Theorem idleness, 29:C2; the padding of Corollary symmetry, 29:C4; the disjoint double and its swap and the11minimal realization's confinement of Lemma boundary, 29:C6, 29:C7; the buffer frame of Proposition illusion,1229:C8; the record of Corollary asymmetry, 29:C3; induction from the least element, 29:B6), `Theme/SecondOrder`13(the full second-order theory of a finite structure decided by evaluation, 29:E4), `Theme/Logic` (the finite14frame's complete decidable theory, no finite model of Q, the record count, the stability schema: 29:B4, 29:B5,1529:C10, 29:E2) and the foundation theme's `Theme/Foundation` (the cycle, 29:B4). Two predicates carry the keys of16equivalent rows of earlier papers: 29:B5 is 25:C1 (`p25010`) and 29:C10 is 5:C2 (`p05013`). The paper's python17witness is the framework's ledger file `frc/ledgers/p29_finitism.py`. No Mathlib statements: no row needs them.18-/1920namespace FRC.Finitism21-- Ledger predicates of 29-finitism (generated by make_predicates.py from docs/29-finitism/29-finitism-ledger.json; edit the ledger, not this section)22/-- 29:B4 (p29006) — 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. -/23theorem 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 :=24  @FRC.Ledger.p2900625/-- 29:B5 (p25010) — 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. -/26theorem 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 :=27  @FRC.Ledger.p2501028/-- 29:B6 (p29007) — 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. -/29theorem 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 :=30  @FRC.Ledger.p2900731/-- 29:C2 (p29010) — 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. -/32theorem 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 :=33  @FRC.Ledger.p2901034/-- 29:C3 (p29011) — 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. -/35theorem 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 :=36  @FRC.Ledger.p2901137/-- 29:C4 (p29012) — 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. -/38theorem 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 :=39  @FRC.Ledger.p2901240/-- 29:C6 (p29014) — 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. -/41theorem 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) :=42  @FRC.Ledger.p2901443/-- 29:C7 (p29015) — 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. -/44theorem 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 :=45  @FRC.Ledger.p2901546/-- 29:C8 (p29016) — 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}$. -/47theorem 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) :=48  @FRC.Ledger.p2901649/-- 29:C10 (p05013) — 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. -/50theorem 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 :=51  @FRC.Ledger.p0501352/-- 29:E2 (p29022) — 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. -/53theorem 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 :=54  @FRC.Ledger.p2902255/-- 29:E4 (p29024) — 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. -/56theorem 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) :=57  @FRC.Ledger.p2902458/-- 29:X1 (p29026) — \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. -/59theorem 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 :=60  @FRC.Ledger.p2902661/-- 29:X2 (p29027) — \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. -/62theorem 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 φ :=63  @FRC.Ledger.p2902764-- end ledger predicates65end FRC.Finitism66