| # | Description | Status | Sources |
|---|---|---|---|
| A. Inputs | |||
| A1p05001 | The classical theorems, accepted unchanged: Gödel I and Rosser, Tarski’s undefinability, Turing’s halting theorem, Cantor’s theorem and uncountability, Russell, Burali–Forti, Skolem, Vitali, Hausdorff, Banach–Tarski; the operational paradoxes (Hilbert’s hotel, Zeno). No classical derivation is disputed. | I | [G"odel 1931; Rosser 1936; Tarski 1956; Turing 1937; Cantor 1891; Russell 1903; Burali-Forti 1897; Skolem 1922; Vitali 1905; Hausdorff 1914; Banach & Tarski 1924] |
| A2p05002 | Metamathematics: Robinson’s $Q$, essentially undecidable, every model infinite; $\mathrm{Con}(Q)$ by cut elimination in $I\Delta_0+\mathrm{superexp}$, not in $I\Delta_0+\mathrm{exp}$; Tait’s finitism; Dedekind’s categoricity of the second-order naturals; true second-order arithmetic not arithmetical; Tarski’s decidable real field; Solovay’s model and Shelah’s inaccessible. | I | [Tarski et al. 1953; H'ajek & Pudl'ak 1993; Wilkie & Paris 1987; Tait 1981; Shapiro 1991; Tarski 1951; Solovay 1970; Shelah 1984] |
| A3p05003 | Combinatorics and set theory: Fraenkel–Mostowski permutation models (symmetry as an obstruction to choice); de Bruijn–Erdős compactness of colouring; aperiodic tile sets and the undecidability of the domino problem (Berger, Robinson); Zermelo’s choice. | I | [Jech 1973; de Bruijn & ErdH os 1951; Berger 1966; Robinson 1971; Zermelo 1904] |
| A4p05004 | The corpus: the totality finite and complete (00:A2), counting closes by return (00:A5), a bounded observer a proper part and every reading a projection (00:A4, A6), Gödel vacuous over the finite $\Omega$ (00:Z1), the $\Omega$-hard demarcation (00:Z3); finite mathematics as ontologically primary (Lev, Zeilberger). | I | |
| B. Gödel’s bundle and the frames | |||
| B1p05005 | The standing hypotheses: (Eff) effective axiomatisation, (Arith) interpretability of $Q$, (Cns) consistency. Two doors for infinity: the meta-level syntax, potential and retained; and (IR), the object theory interprets $Q$ — an injective non-cyclic successor with sequence coding, the completed registry inside the theory. | D | Section 3; § 3.1 |
| B2p05006 | The bundle $\{$Eff, Cns, Cmp, IR$\}$ is inconsistent, with no soundness assumption: under Eff and IR the Rosser sentence is available, and Cmp decides it against plain consistency. | T | Prop. 1; Thm. 3.3 |
| B3p05007 | Witnessed independence: every three-element subset is satisfiable — $Q$ itself ($\neg$Cmp, consistent by finitary means, the superexponential cost exact); $\mathrm{Th}(W_N)$ ($\neg$IR: consistent, complete, decidable, singly axiomatised, interpreting no $Q$ since every model of $Q$ is infinite); the inconsistent extension ($\neg$Cns); true arithmetic ($\neg$Eff). Four legs, all load-bearing. | T |   Thm. 3.4 master: 00:Z1 |
| B4p05008 | The arithmetic frame $W_N$: domain $[0,N)$, constant $0$, order $<$, the graphs $S$, $A$, $M$ of successor, sum and product restricted to the domain (overflow fails the atom); frame truth is truth in $W_N$; a $\Delta_0$ sentence is transcribed through the graphs with guarded bounded quantifiers. | D | Def. 1; § 3.2 |
| B5p05009 | Per-frame completeness: $\mathrm{Th}(W_N)$ is consistent, complete and decidable, axiomatised by the categorical sentence $\sigma_N$; truth in any finite structure is decided by evaluation, and the theory of any structure is complete. | T | Prop. 2 master: 00:Z1 |
| B6p05010 | Bounded stability, schema form: a $\Delta_0$ sentence $\varphi$ with bound $t(\varphi)$ has $W_N\models\varphi^{*}\iff\N\models\varphi$ for every $N>t(\varphi)$, each instance $\mathrm{St}(\varphi,M)$ a finite conjunction of finite checks; proved for an explicit $\Delta_0$ language with $t(\varphi)$ computed; Goldbach below $20$ has $t=400$ and value true (below $10$, $t=100$, decided by the kernel). | T |  Thm. 3.6; Ex. 3.7 |
| B7p05011 | The unbounded quantifier is the internalised registry: a $\Pi^{0}_{1}$ sentence receives a verdict from each frame about its own domain and none about all frames at once; frame-relative completeness covers every executed verification (a bounded $\Delta_0$ trace) and no $\Pi^{0}_{1}$ closure. | Ω | master: 00:Z3 |
| C. Where incompleteness goes | |||
| C1p05012 | The bounded agent of capacity $K$: records of at most $K$ symbols over $s\ge2$ letters, fewer than $s^{K+1}$ of them; certification is a retained record encoding a completed proof-check, one sentence per record, no schema compression. | D | Def. 2 |
| C2p05013 | No internal mirror: fewer than $s^{K+1}$ records exist, so an agent with $s^{K+1}<N$ holds no injective representation of the domain of $W_N$ — a proper part cannot mirror the whole (pigeonhole). | T | Prop. 3 master: 00:A4 |
| C3p05014 | Vanishing certified fraction: at least $c^{L}$ normal-form sentences of length $\le L$, half of each cohort frame truths by completeness, fewer than $s^{K+1}$ certified, so the certified fraction is at most $s^{K+1}/\lfloor c^{L}/2\rfloor\to0$. | T | Prop. 4 |
| C4p05015 | The migration: without IR every sentence about the totality is decided and incompleteness reappears as a resource bound on agents — the Gödel sentence’s role passes to truths whose shortest certificate exceeds the capacity; truth for $W_N$ is definable one level up (Tarski relativised to a resource hierarchy). | D | § 3.3; 00:Z1 master: 00:Z1 |
| C5p05016 | 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. | T | § 3.3 |
| D. The reductio principle and the forced selection | |||
| D1p05017 | The premises and baselines: AT (an absolute totality), IR (the internalised registry), AC$\infty$ (unrestricted choice over uncountable families); Cns, Cmp, Meas (the exact measure axioms of each geometry), and Det — a totality decides every well-posed question about itself, elements, subsets and relations, with its full second-order theory effectively presented; declared as an axiom. | D | § 4.1 |
| D2p05018 | Antinomy normal form: Cns $+$ AT $+$ comprehension is inconsistent (Russell, Burali–Forti); the witness of Cns $+\neg$AT is bounded comprehension — every set $u$ has a subset not among its members and no universal set exists, decided on $V_4$. | T | Prop. 5 |
| D3p05019 | 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. | T | Prop. 6; Rem. 4.1 |
| D4p05020 | Choice normal forms: Vitali (countably additive translation-invariant measure on all subsets $+$ AC$\infty$ on $\R/\Q$, a countable amenable group) and Banach–Tarski (finitely additive isometry-invariant measure $+$ AC$\infty$ $+$ a free non-amenable rotation subgroup) are inconsistent bundles with distinct mechanisms; the finite witness is counting measure with definable choice. | T | Prop. 7 |
| D5p05021 | The reductio principle: for each normal form a baseline $B$ and one infinitary premise $I$ with $B+I$ contradictory and $B+\neg I$ satisfiable by an explicit witness — bounded ranks, $\mathrm{Th}(W_N)$, counting measure (Solovay’s model as classical corroboration); the rejection of $I$ is coherent and witnessed. | T | |
| D6p05022 | The selection thesis: every normal form conjoins completed infinity with a totalising operation (comprehension, completeness, total selection, a total measure); each is harmless alone, contradiction tracks the conjunction; classical mathematics rejected the totalising conjunct at each crisis, this paper the shared one, the selection settled by Det rather than convention. | D | § 4.4; § 2.5 |
| D7p05023 | Forced exit: Det supplies Eff and Cmp, so $\{$Cns, Det, IR$\}$ is inconsistent and, Cns and Det being constitutive, the reductio is forced against IR — no determinate totality internalises an unbounded registry; the four-clause bundle condenses to this triad. Conditional on Det. | T | Prop. 8; B2 |
| D8p05024 | Finiteness of determinate totalities: in ZF with every infinite set Dedekind-infinite, a structure satisfies Det iff it is finite — finite: the full higher-order theory decided by exhaustive evaluation; infinite: a copy of $\N$ inside gives an effective reduction of true second-order arithmetic, which is not arithmetical. The real field’s first-order tameness is silence about its subsets. | T | Prop. 9 |
| D9p05025 | Corollaries: no absolute totality is determinate (a universal set is infinite by the iterated singletons); Meas is decided content — a Det totality decides every measure question, trivially on a finite one (counting measure). The totalising conjuncts of two normal forms follow from D8. | T | Cor. 1; Cor. 2 |
| D10p05026 | The three gates: syntactic infinity (meta-level, potential, retained), semantic infinity (a completed object of the theory, the target in all three forms), diagonalisation (a method, dangerous only downstream of the second gate); the paper argues with an unbounded supply of finite objects only. | D | § 4.5; Table 2 |
| E. Choice recovered | |||
| E1p05027 | 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. | T | Prop. 10 |
| E2p05028 | 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. | T | Lemma 5.2; Def. 5 |
| E3p05029 | Equivariant periodic choice: a $G$-equivariant section exists iff each stabiliser action $G_i\curvearrowright A_i$ has a fixed point (one orbit at a time); the Fraenkel–Mostowski mechanism in positive form. | T | Thm. 5.3 |
| E4p05030 | The definable basis: every subspace of a finite vector space has the greedy $\min$-basis, one definable function on all subspaces; the equivariant obstruction — $\Z/2$ acting by $v\mapsto-v$ on the line over $\F_5$ fixes no basis ($-v\neq v$), over $\F_2$ it does: arithmetic, not formal. | T | Thm. 5.4; Ex. 5.5 |
| E5p05031 | Periodic Kő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. | T | Lemma 5.6 |
| E6p05032 | Periodic de Bruijn–Erdős, dimension one: a $\sigma$-periodic graph of bounded range whose finite subgraphs are $c$-colourable admits a definable $\sigma^{m}$-periodic $c$-colouring (the transfer digraph $D_c$, its sub-digraph of vertices beginning walks of every length, E5). | T | Thm. 5.7 |
| E7p05033 | The dimension boundary: in $\Z^{2}$ aperiodic tile sets exist — every finite patch admissible, no periodic configuration — and the domino problem is undecidable; the passage from finite admissibility to infinite realisability has no finite certificate, its demarcation none either. The finite reading asserts patch admissibility only. | Ω | § 5.4; A3 |
| E8p05034 | The choice paradoxes vanish: on a finite set counting measure is complete and invariant, no decomposition doubles the set ($X\sqcup X$ does not inject into $X$), and every ultrafilter is principal; periodic variants inherit this on one period. | T | § 5.5 |
| F. The reading | |||
| F1p05035 | Ontology and conservativeness: actual infinity is an idealisation of the finite; the bounded fragment is kept exactly, the unbounded fragment in schema form; analysis as approximation over finite grids; choice in the small. Positioning: finitism, intuitionism, ultrafinitism, structuralism; the potential-infinity rule retained at the meta-level as a commitment, not a neutrality. | D | master: 00:A2 |
| F2p05036 | The Reductio Rule and its two tribunals: the economic ledger (the classical exit keeps $\Pi_1$, $\Pi_2$ number theory at a superexponential consistency grant; the finite exit keeps the bounded fragment and declines one classically provable existence claim, E7) and the constitutive Det, on which the verdict rests; objections O1–O5 answered. | D | § 6.2; § 6.3 |
| F3p05037 | The catalogue: the pathologies of the completed infinite in four classes — antinomies, consistent-but-unregistrable, underdetermination, physical divergences — each removed by finiteness; the one exclusion retained, the schema over finite instances and the successor act. | D | Appendix A |
| T. Tasks | |||
| T1p05041 | The standing of the iteration rule — whether the potential-infinity rule of the meta-level can be rejected, and at what cost — is the subject of companion work; the present results are stated to survive either outcome. | O | § 6.1 |
Nothing matches that filter.
Status
- I
- Import. A standard result, or a corpus result, used without reproof.
- D
- Definition. A naming or declared convention, carrying no empirical content.
- T
- Theorem. Derived, and machine-verified in exact arithmetic by the named witness.
- Ω
- $\Omega$-hard. Decided by the totality; not closeable by a bounded observer. A demarcation, not an open item.
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 (
p05007) — 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).