| # | Description | Status | Sources |
|---|---|---|---|
| A. Inputs | |||
| A1p29001 | The literature as stated: Robinson’s $Q$ and its models; the rule form of the license; Dedekind’s categoricity and the non-arithmetical second-order truth, cited as the classical position’s own theorems; the potentialist semantics; truthmakers. | I | [Tarski et al. 1953; Hilbert 1926; Tait 1981; Shapiro 1991; Linnebo 2013; Linnebo & Shapiro 2019; Armstrong 2004; Fine 1994; Vetter 2015] |
| A2p29002 | The corpus: the bounded agent and its record count (5:C1, 5:C2); bounded stability (5:B6); the finite frame’s complete decidable theory (5:B5, 00:Z1); the finite direction of determinacy (5:D8); no finite model of $Q$ (25:C1); the reading of a part (25:D1, 00:A4); counting closes by return (00:A5). | I | |
| B. The audit and the license | |||
| B1p29003 | A formation act of bounded arity yields a new object distinct from its inputs; the paradigms $x\mapsto\{x\}$ and the extension of a finite frame by one element. A configuration is finite and acyclic. In the core a universe is $\mathit{size}$ objects with a formation image, none where the act fails; a trace is $t$ objects with asserted atoms. | D | Def. 1 |
| B2p29004 | A license is a rule, adopted or declined, asserting nothing. A supply is a proposition: the totality of objects obtainable by iteration exists. Iteration names repeated application under the license; induction names the closure over its results. | D | Def. 2 |
| B3p29005 | The classical construction uses a medium, productivity and an unbounded license. The medium is a presupposition no position declines; productivity and the license are posits; the formalist reading declines productivity coherently. Ontological weight and formal innocence cannot both be claimed. | D | Prop. 1; § 2.4 |
| B4p29006 | 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. | T |   Prop. 1 master: 00:A5 |
| B5p25010 | 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. | T | Lemma 2.1 master: 00:Z1 |
| B6p29007 | 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. | T | Lemma 2.1 |
| B7p29008 | The modal ascent: asserted as true, the license quantifies over stages and possibilities; its truthmaker outruns every finite configuration, since every configuration is realized in a universe extending it by nothing (C2) and in universes of every larger size (C4). Rests on C2, C4. | D | Prop. 2 |
| C. Empirical idleness | |||
| C1p29009 | An agent of capacity $K$ over $s\ge2$ letters holds records of at most $K$ symbols, fewer than $s^{K+1}$; certification is a retained record encoding a completed check with a bounded local trace; the locality and interface clauses. Extends 5:C1. | D | Def. 3; § 4 |
| C2p29010 | 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. | T | Thm. 4.1 master: 00:A2 |
| C3p29011 | 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). | T | Cor. 1 |
| C4p29012 | 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. | T | Cor. 2 |
| C5p29013 | No symmetry of standing: every realization of C2 and C4 is a model of the finite position, which asserts nothing beyond what such models exhibit. Uncertifiability of the bound is a statement about records; the selection between the positions is made at the level of models and costs (§ 5.3). | D | Rem. 4.2 |
| C6p29014 | 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. | T | Lemma 4.3 |
| C7p29015 | 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. | T | Lemma 4.3 |
| C8p29016 | 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}$. | T | Prop. 3 |
| C9p29017 | Proposition illusion (iii): every completed check of the agent passes in buffered frames of every size above its trace (C4, C8) and in their doubles (C6), and no act on a presentable object fails (C7): no check separates the agent’s frame from any larger one. The classical “infinite universe” is the chart reading. Potentiality is the inside view of finitude. | D | Prop. 3 |
| C10p05013 | 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. | T | § 6, (O3) |
| D. The verdict | |||
| D1p29018 | The truthmaker demand, restricted: a foundational commitment that does ontological work owes an account of its carrier; truthmaker maximalism is not assumed; the deflationist reply is answered by idleness (C2). | D | § 5.1 |
| D2p29019 | Under the demand the assertion faces three outcomes: a completed range (actualism, the reductio of 5-reductio, C2 verbatim); a modal realm — articulated, borrowing the actualist semantics one level up; essence, horn (ii) renamed; primitive, met by declaration, operational content and cost (the fallback stated once); the finite stock, the survivor. | D | § 5.2–5.4 |
| D3p29020 | The objections O1–O7 and their replies: declaration (O1); induction untouched (B5, B6, E2; O2); the pigeonhole (C10; O3); not ultrafinitism (O4); the bound undecided by observation, the posit idle (C2, C4, C5; O5); the semantics engaged where the mirroring theorems live (O6); the free parameter (C2; O7). | D | § 6 |
| E. Bounded actualism | |||
| E1p29021 | One finite frame; its cardinality determinate and not certifiable by its parts (C10); the license a rule exercised within it; the universal assertion false, its phenomenology derived (C8, C9); induction a theorem (B6); closures as schemas (E2). In the programme the frame is the Carrier, $\Omega=4S+1$, $S\sim10^{122}$ [chart] (00:A2, 00:A7). | D | § 7 |
| E2p29022 | 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. | T | Prop. 4 |
| E3p29023 | Effective determinacy: a totality decides every well-posed question about itself, its subsets and relations included, each decision effectively producible; a property of the structure presented as a finite object, not of an agent inside it. | D | Cor. 3 |
| E4p29024 | 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. | T | Cor. 3 |
| E5p29025 | The costs: universal generalizations in schema form (E2); the frame bound unknowable from within (C10); the verdict conditional on declining unanalyzable modal primitives (D2’s fallback). | D | § 7 |
| X. What the construction explains | |||
| X1p29026 | “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. | T | Prop. 3 |
| X2p29027 | 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. | T | Lemma 2.1; Prop. 4 |
Nothing matches that filter.
Status
- I
- Import. A standard result, or a corpus result, used without reproof.
- D
- Definition. A naming, a declared convention or a reading, carrying no claim of its own.
- T
- Theorem. Derived in the paper, and machine-verified in exact arithmetic by the named witness.
Sources
- Gold: the python check that decides the predicate, at its line in the script (the source, rendered on this site); on hover the deciding family and the families that corroborate it, and the verdict of the last run (red when it fails). The script page's bar runs the predicate's cell of the package's notebook on Google Colab (one cell per predicate; the whole notebook from the header badge).
- The predicate as one Lean declaration, named by its accession key (
p29006) — the conjunction of the theorems that prove it — at its line in the rendered module, one mark per library that proves it, the core's first. Green: the core (lean/FrcCore) — the statement on the shell ring, by computation and induction, no Mathlib, no axioms: the finitist witness. Violet: Mathlib (lean/FrcLedger) — the classical statement for every shell on Mathlib's hierarchy (its axioms,propext,Classical.choice,Quot.sound, on hover). Red: a proof the gate rejects (an unfinished proof,native_decide) — not a witness. A predicate proved in both libraries shows both marks; one mark, one proof. The module page's bar opens the module as one executable file in Lean Live (the core on plain Lean, no Mathlib; the file elaborates in the browser and prints every predicate's axioms at its end); the header's two Lean badges count the marks of each colour and open the two executables. - section
- The statement in the paper's body that carries the predicate: a proposition, a remark or a section.
- rests on
- The predicates it rests on, by label: realisations, definitions and imports of this ledger, predicates of other ledgers (
32:B3) and of the master (00:D15).