Finite Ring Cosmology

Theoretical framework for reinterpretation of Mathematics, Physics and Cosmology over a finite holographic substrate whose cardinality is fixed by the de Sitter entropy. One succession of arguments from first principles to finite arithmetic, open problems of mathematics, and the physics of the Standard Model. Every claim tagged, sourced, formalised and, where it admits a finite check, machine-verified.

The predicate ledger of the corpus: the master ledger 00 and the ledger of every public paper, one predicate per row. A row is cited by its ledger and label, as 00:A1 or 35:P11, and each label opens the row in its own ledger. The accession key pNNNNN stays fixed while labels may move, and register.html#pNNNNN opens its row. The Filters choose a paper, a block and a status, and the search runs within the choice. Across all papers, a prediction or an explanation stated in more than one paper is listed once, at its first appearance, with its restatements linked.

Filters
#PredicateStatus Sources
A. Foundation: from existence to the finite carrierpython8Lean7Lean, Mathlib1
A1p00001The Universe exists: the sole indubitable given (“I think, therefore the Universe is”). Neither axiom nor assumption.G
A2p00004Finitude: the Universe is the totality of its registered manifestations (A8). For any totality and any reading of capacity $R$, the registered Universe embeds in the shell of $R$ members, and among any $R+1$ members two share a residue (5:C2, 29:C1, 29:C2): the Universe is finite, its structural cardinality $\Om$ (A7).T
python sourceLean, the core
A3p00003Completeness of the totality: whatever exists is registered within — the registration of any totality is onto its registered Universe (A8) — so no outside (A8), no host (A1). Unique: two totalities each registered whole within the other have one count (5:C2 both ways), one count one Carrier (A6). No proper closed substructure (A10). Observers are parts within (A4).T
python sourceLean, the core
A4p00197Incompleteness of observation: every observation is a registration by an embedded part (C4, A13) of cardinality $\p<\sqrt\Om$ (A6, B8): every reading identifies two members (25:D1, 5:C2) — an incomplete projection, complete only at the whole count. No frame sees more: one translation carries each member to each, one affine map each frame to each (A6, 1:C2). Horizon: Z1, Z9.T
python sourceLean, the core
A5p00188Counting closes by return: the successor $C_q:x\mapsto x{+}1\ (\mathrm{mod}\ q)$ on $q\ge2$ points is one $q$-cycle with no fixed point, so iteration is bounded and cyclic; its interpretation is A2’s.T
python sourceLean, the core
A6p00008The Carrier C: A timeless torsor of $\Om$ elements, its cardinality is its only absolute characteristic; reframings $x\mapsto ax+b$ are automorphisms, so $0,1,-1$ are frame data; a Subject’s frame charts it as the prime field $\F_\Om$ — the frame’s chart, never the Carrier (C1). Arena and numbers: B1.D
A7p00009Scale, the sole quantitative import: the de Sitter entropy of the observable universe fixes the cardinality exactly, $\Om=4\dS+1$. Its chart numeral is $\dS=\pi(r_H/\ell_P)^2=3.3\times10^{122}$ [chart] at $r_H=c/H_\Lambda$ (14-entr), so $\Om=1.3\times10^{123}$ [chart]. The Carrier congruences are certified by the realisations (B5, C8), not imported. Metrology: L2.I
python sourceLean, Mathlib
A8p00010Realisation, not correspondence: a sufficiently expressive, predictive, registration-complete structure is its subject, not an abstraction of it. By the incompleteness of observation (A4) no registration reaches an unregistered reality, so a distinction with no registered residue is no distinction. Identification rows (R) are therefore constitutive: defended by the totality of registered consequences, killed by explicit falsifiers.D
A9p00161The trusted base: the kernel’s type theory, with the prelude’s natural numbers read as the index of shells; no core statement asserts unboundedness, and no step of a certificate computes a count above $\Om$ at any admissible instance.D
A10p00162Completeness is primality: the residues of a count $q\ge2$ have no proper nonzero ideal iff $q$ is prime, so the arithmetic of a counting cycle is complete exactly on prime cycles — the formal shadow of A3, since a proper closed substructure of the totality would be a second totality within it.T
python sourceLean, the core
A11p00163The quarter-turn exists iff $\p\equiv1\pmod4$: for an odd prime $\p$, $-1$ is a square in $\F_\p$ iff $\p\equiv1\pmod4$ (the formal shadow of B3).T
python sourceLean, the core
A12p00164Every prime carries a frame: every prime field $\F_\p$ of the totality has a primitive root, so a drive $\gen$ with $\langle\gen\rangle=\F_\p^{\times}$ exists (the formal shadow of C1).T
python sourceLean, the core
A13p00196Labels and support: a reading’s labels $\mathcal L_i$ count distinctions only through their support $\rho_i{:}\mathcal L_i\to\Om$; labels with one support are one distinction, so the distinctions realised are the quotient $\mathcal L_i/{\sim_i}$, and labels may outnumber them without adding one (A4).D
B. The Carrier: the substrate structurepython5Lean5
B1p00011All numbers are unframed Carrier residues, framed rationals ($\fQ$) in a Subject frame, in which every structure the sciences use is built exactly. The continuum is a labelled idealisation read against $\mathbb R$ [chart], never an object. The accessible smalls are the counts below the observer’s horizon, the wrap-free window of primality, parity and order (B8, B9).D
B2p00012Phase cycle $\Phi=\F_\Om^{\times}\cong C_{\Om-1}$, the split torus of order $\Om-1=4\dS$; the cycle’s order and divisor lattice are frame-invariant (the arithmetic of $\dS$ is the spectrum of admissible dynamics), its marked elements frame data.D
B3p00013Quarter-turn torsion: $4\mid\Om-1$ by construction ($\Om=4\dS+1$, A7), so the split torus carries a unique order-four subgroup — the Carrier’s $Q_4$ core $\{1,\hbar,-1,h\}$ ($\hbar^2\equiv-1$, $h:=-\hbar$ the root-pair partner of $\hbar$, B7), the symmetry-complete condition. The Subject’s labels $\{1,\im,-1,-\im\}$ are frame data (C1), the two quarter-turns distinct objects (D7).D
B4p00014Triality centre: $3\mid\Om+1$, so $x^2+x+1$ has no root in $\F_\Om$, and its roots $\omega,\omega^2$ with $1$ form the unique order-three group of norm-one residue pairs, the triality centre; its labels $\{1,\omega,\omega^2\}$ are Subject frame data (C1); jointly with B3 it forces the substrate residue (B5).D
B5p00015The substrate residue: the quarter-turn ($4\mid\Om-1$, B3) and the triality centre ($3\mid\Om+1$, B4) jointly hold iff $\Om\equiv5\pmod{12}$. Both are relations certified by realisations, never properties of an integer: $Q_4$ by the quantum realisation (D4), the triality centre by the strong realisation (D6). The inference runs structure $\to$ congruence (A3); a laboratory pattern instantiates the residue or does not (10:E9).T
python sourceLean, the core
B6p00016Four generative levels (succession $\to$ addition $\to$ multiplication $\to$ fixed-base exponentiation) generate the carrier’s two cyclic structures ($C_\Om$, $C_{\Om-1}$) and the exponential bridge lemma; the fifth level (tetration) folds back since exponents are $(\Om{-}1)$-cardinality residues, so the hierarchy, unbounded under the classical reading, closes at four over $\F_\Om$ (structural, not a cost claim).D
B7p00165Physical constants are definite Carrier residues: the register $\{\dS,\Om,c,\hbar,G,k_B\}$ is generator-free in $\dS$ alone — $G=2\dS=-c^2$, $c^2=2^{-1}$ (C8, D7), $\hbar^2=-1$, $k_B^2=-2$, $|k_B|=\hbar/c$; the defining congruences are the observer’s complete certificates, $G$ exact, the rest up to sign (B10); $h:=-\hbar$ is the root-pair partner of $\hbar$ (B3, D7). No Subject counterpart of $G$ or $\hbar$; no fifth constant (C1).T
python sourceLean, the core
B8p00166The window ladder: a nested Subject, $\p^2<\Om$, has its own horizon below the Carrier’s quarter-root, $\sqrt\p<\Om^{1/4}$, and its shell below the coherence horizon, $\p<\Om^{1/2}$; the saturating Subject ($\p^2\to\Om$) locks the ladder $\mathrm{small}<\Om^{1/4}<\p\text{-hard}<\Om^{1/2}<\Om\text{-hard}<\Om$, one square-root horizon per embedding (the bands: B12). Lab-verified ($\Om=2{,}408{,}561$).T
python sourceLean, the core
B9p00019Certification is the orthogonal axis to the B8 bands: a certified entity carries a bounded-height defining relation holding across shells; a framed transcendental is a hard role with none. Registers: at the Carrier the four constants (B7); at the Subject the half-period and quarter-turn, $2\pi\equiv-1$, $\im^2\equiv-1$ (C1) — the same congruence shapes (self-similarity). Physical constants $\Om$-hard, mathematical constants $\p $-hard.D
B10p00168One gauge bit closes the sign sector: no C14-type marker exists — $-1$ is a square on admissible $\Om$, so square class is pair-blind, and integer parity is frame data (A6). Registered faces are pair-invariant: $c^2$, the one-way member synchronisation gauge (C8); $|k_B|$ (C12); $\{\hbar,h\}$ the two named unit faces (B7).T
python sourceLean, the core
B12p00167The two-level horizon law: hardness is one mechanism at every scale — a role is $\Om$-hard when it lives at the Carrier’s scale, $\p$-hard when it lies beyond the Subject’s own horizon $\sqrt\p$ inside its own shell; hardness attaches to roles, never to bare residues. The ladder: B8; certification: B9.D
B13p00169The sign of the Boltzmann residue: $k_B:=-\hbar/c$, the sign fixed by the Hawking scaling $k_Bc=h$ read in the chart [chart]; the registered face is $|k_B|$ (B10).D
B14p00170The octant sector: $C_8\subset C_{4\dS}$ exists exactly when $\dS$ is even (14:C6).T
python sourceLean, the core
C. The Subject: the frame and its registrationpython13Lean13
C1p00021The frame, Subject-only: $(\chron;0,1,\gen)$, origin, unit and the drive $x\mapsto gx$ (A6). Shell data, capacity-first: $\kap $ primitive, $\p =4\kap +1$, $\im=-\gen^\kap $ (C7), $\pi=2\kap $, $e=\gen^{\,\im}$; $\gen$ the one nonsquare frame datum (C3, C8). Exponents of $\gen$ are taken in $\Zp$, a residue in an exponent standing for its lift $\iota:\F_\p\to\{0,\dots,\p-1\}$. The web closes on every shell: $2\pi\equiv-1$, $\gen^{\,\pi}\equiv-1$, $-\pi=2^{-1}$ (N2).T
python sourceLean, the core
C2p00022Scale-shift duality: dilation $x\mapsto gx$ is phase evolution of the frame, advancing $t$; over the cycle it is the fractional Fourier transform, whose quarter-turn $Q_4$ is the discrete Fourier transform.T
python sourceLean, the core
C3p00150Euclidean--Lorentzian dichotomyThe drive fixes a Lorentzian time axis, causal order is algebraic, the split and non-split tori the two signatures. The signature is the square class of the temporal coefficient $\nu=\gen$ (C1); in $\F_\p$, $\nu=2^{-1}\cdot(2\gen)$, both classes fixed by the parity of $\kap$ (8:B3). In the Carrier $c^2=2^{-1}$ is a square (C8, D7), and $\eta_{00}=-c^2$ is a chart artifact.T
python sourceLean, the core
C4p00024Observer $=$ embedded shell (frame); observation $=$ shared-core comparison of two phase cycles.D
C5p00025Oriented frame $=$ unimodular basis; two oriented frames differ by exactly one matrix of determinant one.D
C6p00171One frame group, three sectorsGravity’s $(3{+}1)$ tensor, the Riemann observer geometry and the quantum spinor structure are three readings of a shell’s frame group $\mathrm{SL}_2$ (C22), element by element, its three tori the scale-time, translation and boost freedoms; continuum shadow the declared $S^3$ (C23), spinor double cover the Clifford layer (D4). Falsifier: a registered space-time, observer or spinor freedom outside the three tori.R
C7p00189Orientation is derived, not conventional: the $c$-square congruence ($\dS$ even, C8) annihilates orientation transport on every Carrier carrying it ($\im^{\dS}\in\{\pm1\}$); the oriented quarter-turn $\im=-\gen^\kap $ is a selection, read by pullback covariance and count positivity; the joint flip $(\gen,\im,s)\mapsto(\gen^{-1},-\im,-s)$ permutes the registration channels. The constants’ derivation consumes no selection (B7). Parity marker: C14. The selection by matter content: D16.T
python sourceLean, the core
C8p00028The square class is chronon parityFor a primitive drive the squares are $\langle \gen^2\rangle$: a residue’s quadratic class is its drive-step parity. Registered transport is even, the one-way multiplier $\gen$ odd, so the one-way speed is gauge and the two-way constant invariant. $[c^2]$ is even iff $\dS$ is even, a relation certified by the unit realisation (D7). The Tsirelson $\sqrt2=\zeta_8+\zeta_8^{-1}$ is its two-way symmetrisation.T
python sourceLean, the core
C9p00029The Object frame is $(\dt;\,q,k,v)$: every entry a Subject residue — offset $\dt$ (synchronisation datum), position $q$, winding $k$ (D2), rate $v$; one relative datum per frame datum. The momentum reading is one quarter-turn from the winding, $p=\im\,k$; the canonical commutator $[\hat q,\hat p]=\im\hbar$ composes the Subject’s chart quarter-turn with the Carrier’s action quantum (D7, B7).D
C10p00030Two strata of probabilityA registered probability is a framed rational; a structural weight is an element of the parity-even cyclotomic subring. The strata coincide exactly on the stationary core-valued $Q_4$ sector, joined by two proved reductions and the stratum-sampling clause (D10). On a single Object the weights are uniform over the fibres (22-qm Rem. borndomain); non-uniform statistics arrive through the engineered-core readout.T
python sourceLean, the core
C11p22028Pair-tally uniqueness (22-qm Prop. gleason, the uniqueness of the pair tally on the stationary $Q_4$ sector): on the stationary core-valued $Q_4$ sector, tally-valued, fibre-additive, drive-invariant, parity-even registration functionals form the character cone fixed by the pure windings; adding channel-selectivity (assumed, not derived; the sampling clause D10) picks the Born ray. The minimal degree is forced; proof shape: 22-qm.T
python sourceLean, the core
C12p00032Temperature and the classical arity, derived: the temperature domain is acceleration, $[\Theta]=[E][k_B]^{-1}=[L][T]^{-2}$, flag-free, $\Theta_P=E_P/|k_B|$, Unruh closing as a domain identity; neither mass nor temperature is primitive — $M$-$L$-$T$-plus-thermal is the torsion-free shadow of the two-generators-plus-flag system (the mass primitive standing in for the flag, the thermal for $k_B$), classical dimensional analysis recovered in exponents and arity.T
python sourceLean, the core
C14p00034The quarter-turn is the odd member of the $\pm\sqrt{-1}$ pair: the two representatives have opposite integer parity (distinct from chronon parity, C8), and $e^{\,\im\pi}:=\gen^{\,2\kap\,\iota(\im)^{2}}\equiv(-1)^{\iota(\im)}$ (the lift $\iota$ of C1), so $e^{\,\im\pi}\equiv-1$ holds exactly on the odd member. The conjugate chart toggles it: the parity names the matter–antimatter gauge (C7), and the selection is generator-independent within the chirality.T
python sourceLean, the core
C16p00151The spinor dichotomy: $\kap$ odd $\Leftrightarrow$ $C_{\p-1}\cong C_4\times C_\kap$ $\Leftrightarrow$ $v_2(\p-1)=2$ $\Leftrightarrow$ $3\kap r+4s\equiv1\ (\mathrm{mod}\ 4\kap)$ is solvable: the spinor class. Shell and Carrier share the $2$-part $C_{2^m}$, $m=\min(v_2(\p-1),v_2(\Om-1))$, and the shell closes on a cover of degree $2^{v_2(\Om-1)-m}$; the shared order times the cover degree is the Carrier’s $2$-part, $8$ exactly when $\dS\equiv2\ (\mathrm{mod}\ 4)$. The midpoint event of a $\kap$-odd shell: 38:C14.T
python sourceLean, the core
C19p00190The Hopf section: on the frames by elements (no group counted, Q20) the boost torus $C_{\p +1}$ is fixed-point-free on $\mathbb{P}^1$ and meets the Borel trivially, so every frame factors uniquely as (cone-chart event)$\times$(boost): the cone chart is a global section of the non-split fibration (C22), $\p (\p -1)$ fibres of $\p +1$; $\mathrm{SL}_2$ obstructs at $-1$.T
python sourceLean, the core
C20p00040The mass–energy channel: the winding sector $C_{\p -1}$ meets the boost base $C_{\p +1}$ in the sign alone and the spinor cover $C_{2(\p +1)}$ in exactly $Q_4$, every $\p =4\kap +1$; the quarter is spinorial, $N(\im)=\im^{2}=-1$: the mass transport crosses the sheet; mass phase $=$ winding rate, one $Q_4$ datum (D2); Carrier instance $78^{58}=89=h$ on $\Om =233$ (38:A4).T
python sourceLean, the core
C21p00041The dilation rigidity theorem: static clock comparison is a register character $\gen^{-\Delta n}$; characters are rigid, so the strong-field dilation law is the unique exponential reading, zero coefficient freedom; the PPN temporal form admits no register character (transitivity defect exactly $4ab$); the cover halves the angle at every tick (C20).T
C22p00152The frame variety and its two fibrations$\mathrm{PGL}_2(\F_\p)\cong\mathrm{SO}_3(\F_\p)$; the norm-one sphere is $\mathrm{SL}_2$, the spin cover of $\mathrm{PSL}_2$, whose elements are frame moves, not registrations. For every $\p=4\kap+1$ of the totality each element is one direction in $\mathbb{P}^1$, one shell cell and one drive phase. Two fibrations partition the variety: non-split $C_{\p +1}$ over $\p (\p -1)$, with the cone-chart section (C19), split $C_{\p -1}$ over $\p (\p +1)$ without.T
C23p00182The spatial chart is the 3-sphere (declared)$SU(2)=S^3$ is declared the continuum chart of the frame group (C27) [chart]. The group has the three element types of $\mathrm{SL}_2(\mathbb{R})$, $SU(2)$ only one; no finite datum marks the compact real form, and cycle closure selects none. Then the spinor sign gives $S^3$, not $SO(3)$ (C22), uniqueness is Poincaré–Perelman [import], and de Sitter slicing has $S^3$ sections [import] (A7).D
C24p13064The third-order wall of $\pi$: for every prime $\p\ge5$ of the totality, $\sigma_\p=\sum_{k<(\p-1)/2}\binom{2k}{k}/((2k+1)16^{k})$ satisfies $\sigma_\p\equiv0\ (\mathrm{mod}\ \p^{2})$ (Sun, JNT 131 (2011), (1.4)) and $\sigma_\p/\p^{2}\equiv(-1)^{(\p+1)/2}B_{\p-3}/36\ (\mathrm{mod}\ \p)$: Sun’s Conjecture 5.1, $\sigma_\p\equiv(-1)^{(\p-1)/2}(H_{\p-1}/12+3\p^{4}B_{\p-5}/160)\ (\mathrm{mod}\ \p^{5})$ for $\p>5$, proved by Hessami Pilehrood, Hessami Pilehrood and Tauraso (Int. J. Number Theory 8 (2012), Thm. 5 (44)), reduced mod $\p^{3}$ with Glaisher’s $H_{\p-1}\equiv-\p^{2}B_{\p-3}/3\ (\mathrm{mod}\ \p^{3})$; $\p=5$ direct. Re-verified for all primes below $10^{4}$.I
C25p00139The horizon is the origin's antipode on the boost torusFor $w^2=\nu$ a nonsquare, the torsor map $\mathbb{P}^1(\F_\p)\to C_{\p +1}$, $P\mapsto u_P/\bar u_P$ with $u_P$ the unique boost carrying $0$ to $P$, is equivariant and sends the origin to $1$ and the horizon $[1{:}0]$ to $-1=\zeta^{(\p +1)/2}$. Origin and horizon are the sign pair $C_{\p -1}\cap C_{\p +1}$ (C20), exchanged by the torus’s unique involution $q\mapsto\nu/q$. On the additive cycle the antipode is the seam $\p/2$ (1:Z1, 1:Z2).T
python sourceLean, the core
C26p00174The four chains of 13-epi are E- and G-partial sumsThe derangement chain $D_n/n!=\sum_{k\le n}(-1)^{k}/k!$ is the partial-sum chain of the E-function $e^{-z}$ at $1$; the arcsin and Machin chains are those of the G-functions $\arcsin z$ at $1/2$ and $\arctan z$ at $1/5$, $1/239$; $e^{\pm1}\in\mathcal E$ and $\pi,1/\pi\in\mathcal G$, both rings (Fischler–Rivoal) [import]. The factorial rate $\Theta(k/\log k)$ against the geometric rate $\Theta(k)$ of 13-epi E5 is that of E- against G-partial sums.I
C27p00183The frame group has one form: on every shell $\mathrm{SU}_2(\F_{\p^2}/\F_\p)=\mathrm{SL}_2(\F_\p)$ for the Hermitian form $wJ$, $w^{\p}=-w$, every element of finite order; the sphere $x^2+y^2+z^2+w^2=1$ and $ad-bc=1$ correspond point by point through the quarter-turn.T
D. The realisations (mathematics as physics)
D1p00042Time is scale-dilationEach Subject’s clock is its own drive $x\mapsto gx$. A composite is read through the reader’s one drive, so its diagonal action and conserved offset are observer-derived, the offset group fixed by the arena’s divisor structure; the Carrier has no clock. Falsifier: a registered duration that is not a drive count of the reader’s frame, or a frame-independent Carrier tick.R
D2p00043Mass is winding rate ($E=hf$ an identity); masslessness $\Leftrightarrow$ drive-invariance; a mass is the non-split component the drive rotates, the part of a residue pair that Frobenius conjugation reverses, masslessness the split-torus eigen-alignment. Falsifier: a rest mass with no cycle winding, a massless drive-variant state, or a stationary state whose registered frequency is not its winding index ($E=hf$ failing).R
D3p00044Distance is decoherence: the separation of two systems is their decoherence count in the observer’s chart, the metric the graph metric of shared-core comparison — the spatial reading of the one relational channel, the twin of D1 (time) and D2 (mass). Falsifier: a metric separation not monotone in the decoherence count of the relational channel.R
D4p00045Quantum: matter is the phase character of a finite cycle; observation is shared-core comparison; the complex amplitude is forced by $Q_4$ ($\im^2{=}{-}1$). Falsifier: a confirmed third-order interference $I_3\neq0$, $S\neq2\sqrt2$, or real-amplitude network behaviour (22-qm P2, P3).R
D5p00046Gravity: a cell-local change of frame is a gauge symmetry, and the connection compensating it is the field (the geometric/diffeomorphism frame). Falsifier: a source gravitating by other than its full mass, entanglement induced off the Newtonian rate, or $\eta\neq0$ (22-qm P1, C22).R
D6p00047Forces: the same recipe applied to the substrate’s three other frame data, namely phase (EM), spinor (weak), and colour (strong); “finish gauging the frame.” Falsifier: a fifth force, a gauge group or charge outside the rank-five frame, or a fourth generation.R
D7p00048A unit of measure is a reciprocal cross-frame relationA unit is observer counts per substrate count, its atomic form the action quantum $\hbar^2=-1$ (B7), its domain the unit-free order-four flag: unitful measures carry it, observables are flag-free, the absolute unit value $\Om$-hard. The fundamental units are the four domain horizons (10-dim). Falsifier: an embedded observer registering an absolute unit value, or a unitful measure with no cross-frame reciprocal.R
D8p00049Elementary is $\Om$-hard: an elementary particle is a large beyond-horizon residue, never observed at rest; the observable exception is the gauge sector’s drive-invariant residue, the photon (G1, Z6); instantiated at $517\times\sqrt\Om$ on a concrete shell (37-sim). Falsifier: an elementary particle with a resolved internal residue (substructure), or a massive drive-invariant gauge residue.R
D9p00050The observable is a small residue: a bounded observer reads only small residues, so an observable stable object carries a small exact residue (particle $+$ binding wrap) — the confined hadron, the light nucleus, the stable atom; decay is frame-normalisation toward it. Falsifier: a stable observable object carrying no small exact residue — a stable coloured state, or strong/electromagnetic proton decay.R
D10p00051The unified sampling clauseA registration protocol samples one stratum of a drive-presented ensemble. Over complete joint recurrences the counts are forced exact tallies (22-qm Rem. strata), on incomplete batches the largest-remainder gauge, shared by the quantum readout and the gravity crossover. Falsifier: outcome tallies over a complete joint recurrence that are not exact ratios, or a fixed-setting protocol sampling more than one stratum.R
D13p00140Observation is the Hopf sectionThe Subject registers its past cone, one chronon per decoherence step (D1, D3), through the cone chart (C19, C22); the horizon is the origin’s antipode (C25). Falsifier: a registration on the direct branch whose value is not the Object’s drive state at $\chron -k$ for its decoherence count $k$, read modulo $\p -1$, or a registration off the past cone.R
D14p00184Mass is dilation (the harness face of D2): the boost factor of a frame’s per-chronon step (C19) is its mass phase, one $Q_4$ datum with the winding rate (C20). Rest energy is the norm reading, $\ker N=C_{\p +1}$, boost-invariant. The lab charts it between the exact $C_4$ stations, the pair class $4\gcd(\dS,2\kap +1)$ host-decided. Falsifier: D2’s.R
D15p00153Thermodynamic entropy is the channel countThe entropy of the first law (E7) is the shell’s record $\kap(\p+1)=(\p^2-1)/4=|\F_\p^\times|\,|C_{\p+1}|/4$, one $k_B$ per channel, $S_{\mathrm{th}}=k_B\,\kap(\p+1)$ [chart]: the count itself, not its logarithm. The record is the capacity of $\F_{\p^2}$, $\p^2=4\kap(\p+1)+1$, as $\dS$ is the Carrier’s. Falsifier: a horizon whose Clausius entropy $\int dM/T$ at the thermometer temperature differs from $k_B$ times its channel count beyond order $1/\p$.R
D16p00175Matter selects the orientation: the joint flip of C7 is the matter–antimatter gauge, and the instance’s matter content selects one orientation; the sector faces are G2 and G15–G17. Falsifier: a registered asymmetry between the two orientations not carried by the matter content.R
D17p00185Gravitational time dilation is literalThe static clock ratio between two stations is the register character $\gen^{-\Delta n}$ of their offset (C21), $\beta=\gamma=1$ (E4, D1). Its registration dictionary is 38:C12 on a hosted pair and 38:C13 on the Carrier, its per-chronon rate the floor (38:C10–C11), the temporal face its half. Falsifier: a static clock ratio not fixed by $\Delta n$ (the PPN temporal form, defect $4ab$).R
E. Gravitypython9Lean8Lean, Mathlib1
E1p00052Uniqueness of the dynamics: in every gauge sector the relevant gauge-invariant adjacency-local action is the unique curvature-square Casimir (Maxwell $F^2$, gravity Fierz–Pauli, Yang–Mills $\mathrm{Tr}\,F^2$) — one adjacency-local uniqueness lemma, proven on the shell.T
python sourceLean, the core
E3p00154Gravity (linear): the Coulomb law is gravity’s own lattice Green’s function; the field equation is the discrete Fierz–Pauli functional, the unique adjacency-local stiffness (E1). Universal attraction is the drive’s single time arrow.T
python sourceLean, the core
E4p00055Gravity (nonlinear completion): the relational shift-symmetry Ward identity forbids self-sourcing (what gravitates is winding rate, D2), so the static potential is harmonic and the completion is the unique scale-covariant exponential metric (Deser’s bootstrap inapplicable); $\beta=\gamma=1$ and the classical tests exact, the first departures strong-field. Falsifier: a weak-field departure from $\beta=\gamma=1$, or a self-sourcing static potential.R
python sourceLean, the core
E5p00056Gravity (the floor’s faces): collapse yields no event horizon and no singularity but an operationally black body at $r_f=r_s/\ln\Om$, clock rate $1/\sqrt\Om$, its interior a microscopic slip core. The global drive enters local physics only through the floor: preferred-frame parameters are $O(1/\sqrt\Om)\sim3\times10^{-62}$, Lense–Thirring at the GR value. Falsifier: a registered event horizon or singularity, or a preferred-frame parameter above $O(1/\sqrt\Om)$.R
python sourceLean, the core
E6p00176Gravity (horizon count): the registration sphere of a shell has area $A=\p(\p+1)$ and record $\kap(\p+1)$, so $\kap(\p+1)/A=\kap/\p$ exactly, the $Q_4$ gauge quotient, and closes the calibration: at the coherence horizon $\p^2\to\Om$ the record law returns $(\Om-1)/4=\dS$, the imported entropy (A7). The chart reading $S=\tfrac14A/\ell_P^2$ is L5’s. Corollary: the merger area law $\Delta A=2M_1M_2$, saturated (37-sim). Triple: E7.T
python sourceLean, the core
E7p00058Gravity (horizon triple): the record is the registered state count $\kap(\p+1)=(A/4)(1-1/\p )=M(M-1)$ (37:B5, 37:C7) on the rate face $M=(\p +1)/2$ (D2, D14; $\p =2M-1$ the count face), $d[\kap(\p+1)]/dM=\p$ exactly. The temperature has two exact faces, the registration rate $T=(\p +1)/\p ^2$ (E5) and the response $T_{\mathrm{resp}}=(d[\kap(\p+1)]/dM)^{-1}=1/\p$, split by $1+1/\p$. First law $dM=T_{\mathrm{resp}}\,d[\kap(\p+1)]=T\,d[\kap(\p+1)]/(1+1/\p )$; Smarr $2T_{\mathrm{resp}}\kap(\p+1)=M(1-1/\p )$, $2T\kap(\p+1)=M(1-1/\p ^2)$; the chart’s $dM=T\,dS_{\mathrm{th}}$, $M=2TS_{\mathrm{th}}$ [import] to order $1/\p$ (D15).T
python sourceLean, the core
E10p00147The fold is a chart projection: the substrate coordinate $r$ is the decoherence count, the exponential reading the character $\gen^{-\Delta n(r)}$, and the exact datum at a shell of the radial partition is the pair $(r,\gen^{-\Delta n(r)})$, injective in $r$; the areal reading $R=re^{M/r}$ [chart] multiplies the count by the lifted character and forgets $r$ — its two branches are two Carrier data (the residue product $r\gen^{\Delta}$ collides at $\p =13,17,29$, the pair never), and the cut current $p_r=Q_r/A_r$ recovers $r$ from any exterior reading ($A_r=6(2r^2+2r+1)$ on $\mathbb Z^3$, monotone). The fold-return average is fold-independent: $P_EFU^nF^{-1}P_E=P_EU^nP_E$ for every interior chart $F$, the period average $N^{-1}J_E$ (not $N_I^{-1}$), $P_EU^NP_E=P_E$ — no echo criterion. The $r_f$-anchored statements are made in the substrate coordinate, $r_*<r_f<M$ for $M>(\ln\Om /2)^2$ Planck masses [chart].T
python sourceLean, the core
E11p00198The registered adjacency chart (declared): a translation-homogeneous bounded-degree chart on the Subject’s cells, locally flat and three-dimensional [chart], C23’s discrete twin. The drive induces the scale-time direction alone, and the Carrier’s residues carry no chart flat to the horizon radius beyond dimension one (E12); the three dimensions are the frame freedoms (C6). Given the chart, induced relaxation holds (21:C22).D
E12p00199The chart count: a homogeneous chart on the $\Om$ registrations, flat to the horizon radius in $d$ dimensions, holds the $\mathbb Z^{d}$ ball of that radius; for $d\ge2$ the ball exceeds $\Om$, for $d=1$ it fits. The one chart flat to the horizon radius is the drive’s scale-time direction (E11); a three-chart of curvature radius $\sqrt\Om$ needs $\Om^{3/2}$ cells (A2).T
python sourceLean, the core
E13p00200The strong-field wave operator (declared): on the exponential reading (E4) the one wave operator is the chart’s $\Box_g$, 21-gravity’s wave equation with the all-orders index $e^{2u}$ ($\sqrt{-g}\,g^{tt}=-e^{4u}$), acting on the cell’s one phase. The chart is horizonless, continued to the floor $r_f=2M/\ln\Om$ where $e^{2u}=\Om$ (E5) [chart]. The quoted ringdown is the eikonal limit (E14); the $(2,2,0)$ reading is open.D
E14p00201The eikonal pair: on the exponential reading (E4) the photon sphere sits at $r_c=2M$, $b_c=2eM$, and the orbital rate equals the Lyapunov rate, $\Omega_c=\lambda=1/(2eM)$, both $3\sqrt3/(2e)$ of Schwarzschild’s. The wave operator’s $\ell=2$ mode (E13) is $(0.4641-0.0923\,i)/M$ [approx], $0.8\%$ above the eikonal $(\ell+\tfrac12)/(2eM)$. Falsifier: that mode read as the remnant’s $(2,2,0)$ oscillation, $+24\%$ against Kerr, excluded by GW250114 [import].R
python sourceLean, Mathlib
F. Quantumpython2Lean2
F1p00059Quantum mechanics: the Born weighting on the Subject’s ledger is one declared identification, that registration data are sample pairs, plus counting theorems (C8, C10, C11, 22:C13). Falsifier: outcome tallies on the stationary core-valued $Q_4$ sector that are not the pair-form ratios, or a real-amplitude network behaviour (22:C13).R
F2p00191Multi-body registration: an unequal-cycle composite returning below $\Om$ (Q20) recurs jointly at the lcm of its parts’ registration periods; each pair’s conserved offset lives on the $\gcd$ cycle (the quotient $A/\langle v\rangle$), and dephasing over every joint recurrence below $\Om$ is exact, extending the Born-rule count (F1) verbatim to unequal cycles (37-sim: joint recurrence verified, 1400/1400 characters cancel).T
python sourceLean, the core
F4p00062The wavefunction folds on x=i,rg,sThe Object cycle decomposes by the $Q_4$ quotient, $x=\im^{\,r}\gen^{\,s}$: the class $r$ the registrable phase (C14), the coset rung $s$ the outcome index (10:G2); the fold is division-unique, a product iff $\kap$ odd (C16). Fibres are the cosets $q_\alpha\cdot\mathrm{core}$, pointer channels the core characters, the amplitude the coherent fibre sum (22-qm Def. measvectors): observation resolves cosets, never points within one.T
F5p00194The graded registration law: an Object component $\ell^{a}$ registers at depth $d=\mathrm{ord}_{\ell^{a}}(\p)$ — $1$ absorbed (register, unique image), $2$ observable (odd $\ell$: boost torus, unique home; $2^{a}>4$: off both tori), else beyond-quadratic; the sign always $\{\pm1\}$. Visible iff $\p^{d}<\Om$; the cap is $2$ at saturating and minimal towers; opacity relational — hydrogen’s interior opaque/observable/absorbed at $173/181/197$. Controls: proton whole, $(5,13)$ refused.T
python sourceLean, the core
F6p00064The binding lift: a pair fuses iff cycles coprime, windings unit; else the F2 offsets stay drive-confined (22-qm B5, C15) — the deuteron, $(4,4)$, spectrumless. Fusion carries the half-driven offsets onto the F4 rungs; pointer channels forced, Born lands with exact dephasing ($1+\omega+\omega^{2}=0$, $T'=516$). Energies $E_{s}=s\,h/3$, stations $\{0,58,116\}$; cores odd$(\q-1)$: hydrogen $(4,3)\to C_{12}$, $\kap_{O}=3$, ground first.T
G. Interactions: electromagnetism, the weak and strong forces, matter, flavour and superconductivitypython3Lean3
G1p00178Electromagnetism (exact), on the force realisation D6: charge $=$ quantised winding index; the photon is massless, the observable residue $2$ of the split torus $C_{\Om-1}$ (two helicities $=$ two $\F_\Om$-fixed lines $=N(1{-}\im)$; D2, D8); Maxwell is the unique relevant action (E1). The bare coupling: Z8.T
G2p00067Weak (amplitudes): the chiral $V\!-\!A$ current and four-fermion $G_F=1/(\sqrt2\,v^2)$ derived; $W,Z$ scattering unitarised (equivalence theorem).T
G3p00068Weak (scale): the lone scale is the non-split saturation scale, $v=m_P e^{-\mathcal B}$, the exponent $\mathcal B$ the cross-scale $\beta$-function of the non-split channel, not the $\mathrm{SU}(2)$ gauge coefficient ($b_2=19/6$ gives $10^{8}$ GeV). Value tagged: $v$, $\Om$-hard as $\Lambda_{\mathrm{QCD}}$ (G6); the failing computation sums the $\beta$-function over the $\Om$-hard masses (Z6). Relation, $\Om$-blind: the transmutation form.Ω
G4p00069Strong (structure): $\SU(3)$ $=$ the special unitary transformations of a Hermitian three-form, its rank forced as the minimal triality frame (the cubic of $\Om\equiv5\pmod{12}$, B5); the confining area law derived from the positivity of $S_\rho$, the gluon the residue $0$ of the norm-one residue pairs (no $\F_\Om$-fixed line).T
G5p00070Strong (tension): the string tension in finite units, $\sigma=-\ln c_1(\beta)>0$, computed — the finite-group area law gives $c_1$ as an exact character sum (no Haar, no $\Om\to\infty$); closed form on $\SU(2,\F_3){=}2T$ (matching continuum $\SU(2)$ through $O(\beta^3)$), colour $c_1^{\SU(3)}{=}\tfrac\beta{18}{+}\tfrac{\beta^2}{216}{+}\cdots$.T
G6p00071Strong (scale): the cross-scale $\beta$-function and the absolute $\Lambda_{\mathrm{QCD}}$ (dimensional transmutation, $\sigma\sim\ln(1/\beta)$). Value tagged: the absolute $\Lambda_{\mathrm{QCD}}$, in no embedded reader’s window — the failing computation is the $\beta$-function integrated to the substrate scale over the $\Om$-hard spectrum. Relation, $\Om$-blind: $\sigma\sim\ln(1/\beta)$ and the ratios of G8–G10.Ω
G7p27043Strong (CP): the vacuum angle vanishes, $\bar\theta=\theta+\arg\det M_q=0$, with no axion — the colour action carries no substrate-native topological term and colour is drive-invariant ($\theta=0$), and the Hermitian quark mass matrices have real determinant ($\arg\det M_q=0$); the CP phase $\delta_{\mathrm{CP}}$ sits in the up–down misalignment.T
G8p00073Strong (hadron spectrum): a baryon is the centre-neutral triality invariant $\varepsilon_{abc}$ of $\SU(3,\F_2)$; the $\SU(3)_F$ mass relations are exact scale-cancelling identities — Gell-Mann–Okubo, decuplet equal spacing, Coleman–Glashow, the orderings $M_n{>}M_p$ and $M_\Sigma{>}M_\Lambda$, heavy-quark symmetry, the vector-nonet spacing; the decuplet–octet hyperfine is the colour-magnetic curvature invariant, $A_{\mathrm{light}}{=}\sqrt\sigma\,c_{\mathrm{mag}}(\beta)$ the spin-$2$ partner of the tension $c_1$ (G5). Formulas: 35-hadr.T
G9p00074Strong (the residue series): the observable baryon is the Carrier residue $1$, the determinant $\Lambda^3(\mathbf3){=}\varepsilon_{abc}$, forced by the gluon residue $0$ ($N{=}3$ from $\Lambda^N{=}\det$); the meson is residue $1$ (the $q\bar q$ trace); series closed: photon $2$, gluon $0$, baryon $1$, meson $1$ (G1). Selector, stability: the minimal-wrap state is the stable proton, decay frame-normalisation toward it (D9).T
G10p00075Strong (the baryon scale): the absolute ground-state spectrum is the $\Om$-hard scale $\sqrt\sigma{=}\Lambda_{\mathrm{QCD}}$ (G6) times sub-horizon eigenvalues; the baryon mass-over-scale is the computed confinement eigenvalue $M_N/\sqrt\sigma{=}E_0{=}2.232$ (the finite operator $H{=}|p|{+}\sqrt\sigma\,r$, converged finite matrix; $4.6\%$); the constituent ratios $\{\lambda_l,\lambda_{\mathrm{hf}}\}$ are evaluated forward from $\{N{=}3,\beta\}$ with no measured baryon mass, so the light-hadron spectrum is parameter-free over $\sqrt\sigma$; no new $\Om$-hard residue.T
G11p27020One generation (content): $=$ the spinor $\mathbf{16}$ of the rank-five frame — all gauge reps, hypercharges, charges, anomaly-free, $\nu_R$ — recovered in the compact theory, where the frame is $\C^3\oplus\C^2$, via the correspondence: the imported $\mathrm{SO}(10)$ template evaluated on the realisation (27-fld B5).T
python sourceLean, the core
G12p00155One generation (origin)Read with the quarter-turn ($4\mid\Om-1$), the Carrier’s four representation charts are four directions; their reflection algebra has basis $e_S$, $S\subseteq\{1,2,3,4\}$, $16$ elements, $e_Se_T=\pm e_{S\cup T}$ for disjoint $S,T$, else $0$. The quarter-turn as fifth direction maps $e_S\mapsto e_S$ ($|S|$ even), $e_Se_5$ ($|S|$ odd) onto the even basis of five directions: the chiral spinor $\mathbf{16}$. On the realisation 27:B5 matter is this spinor.T
python sourceLean, the core
G13p00078One generation (masses): its elementary particles’ absolute masses are framed-transcendentals, $\Om$-hard (D8, Z6). Value tagged: the sixteen absolute masses, in no embedded reader’s window — the failing computation is the winding of a beyond-horizon residue read at rest. Relations, $\Om$-blind and certified: the mass ratios G16–G17.Ω
G14p00079Count/generate split: one bosonic carrier $+$ three fermion generations (the cubic $C_3$), chirality fixed by the drive, on the role-to-matter realisation (27:B6); $\SO(10)$ unification forced by the relational ontology, the automorphism lemma reduced to the horizon (Z5).D
G15p00080Flavour (structure): the seesaw scale, $b$–$\tau$ unification and the role-ladder mass ordering are derived; the observed spectrum is the projection of the one $\mathbf{16}$. The mixing angles and phases reduce to the role-depth texture, the lopsided $\sigma$, the trimaximal $C_3$ column and quark–lepton complementarity (28-flav C9), leaving the $\Om$-hard phases $\{\delta_0,\delta_\nu,\delta_{\mathrm{CP}}\}$ (Z6); the seesaw fixes $Q_\nu{=}2/3$.T
G16p00081Flavour (Koide): the charged-lepton ratio $Q=2/3$ is the cube-root generation orbit at the self-dual quarter-turn, $Q=\tfrac13+\tfrac23\rho^2$ exact, the value $\rho^2=2^{-1}$ the quarter-turn realisation (28-flav B5; falsifier: $Q_\ell$ off $\tfrac23$ beyond the $\tau$-mass tolerance $\pm7\times10^{-6}$); the winding-phase selection onto that orientation is bedrock, $\Om$-hard in magnitude, its $\Z_2$ sign the derived drive orientation (C7); the sub-horizon reading is $\delta_0=Q/3=2/9$ (radians).T
python sourceLean, the core
G17p00179Flavour (exact ratios): Koide $2/3$ (G16), the factor $3$ of Georgi–Jarlskog, the squared amplitudes the split/non-split norms $N(1{-}\im){=}2$, $N(1{-}\omega){=}3$ on the realisation 28:B5 (G1, G4), trimaximal $|F_{jk}|^2{=}\tfrac13$, maximal Jarlskog $J^2{=}\tfrac1{108}$, the $\lambda$-texture from role depths, and the charged sectors locked by $\delta_\ell{:}\delta_d{:}\delta_u=1{:}\tfrac12{:}\tfrac13$ to $\delta_0$.T
G18p00083Flavour (projection): the $\mathbf{16}\to$observed-spectrum projection map (through $C_3\times Q_4\times$ scale-wrap) is constructed, anchored at its unique drive-invariant total singlet $\nu^c=\Lambda^0$ (the $\mathbf1$ of $\mathbf{16}$), the matter twin of the photon (G1); the residual scale-wrap magnitude is the $\Om$-hard mass set (Z6).T
G19p00088Superconductivity (structure): superconductivity is split-torus confinement, the electric/phase dual of colour (G4), the charge-$2$ condensate a phase-singlet reducing $\mathrm{U}(1)$ to a residual $\Z_2$ (flux $h/2e$) and the Abrikosov vortex the dual colour string whose line tension vanishes at the Kramers–Wannier self-dual point $\beta_*=\tfrac12\ln(1+\sqrt2)$ that is $T_c$.T
G20p00089Superconductivity (duality): the electric–magnetic duality is the $Q_4$ quarter-turn on the charge-flux lattice (charge$\leftrightarrow$flux, Josephson$\leftrightarrow$phase-slip), predicting an Airy vortex-core spectrum and a quantum current standard whose metrology triangle closes on $q_c^2=4$.T
G21p00090Superconductivity (scale): the absolute transition scale ($T_c\propto\omega_D$, the gap and vortex tension in physical units) is $\Om$-hard, the family of $\Lambda_{\mathrm{QCD}}$ (G6) and $v$ (G3). Value tagged: the absolute $T_c$ (with $\omega_D$), in no embedded reader’s window — the failing computation is the physical unit of the shell-exact ratios. Relations, $\Om$-blind: the ratios and the Airy law of G20.Ω
L. Cosmology and the dark sectorpython3Lean, Mathlib3
L1p00192Cosmology (the dark sector)The synchronisation floor $a_0=cH_0/2\pi$ fixes the acceleration scale parameter-free: the $2\pi$ by the angle–count dictionary (14:B2), the threshold one cycle per drive period (32:B3), $1.04\times10^{-10}$ [chart] at the channel-1 $H_0=67.4$ (L3), tied to $H(z)$, not $\Lambda$ (P1; 21:X1). Below the floor the amplitude reading, given the barrier identification (32:B8, 21:B9), gives the radial acceleration relation unfitted. Falsifiers: 32:B3, 21:P4.R
python sourceLean, Mathlib
L2p00085Metrology of the importThe datum $\dS$ is read on two faces by four instrument classes, concordantly (14-entr). Evidence is weighed on two registers: metrology under the circularity criterion (channel-disjoint from the fitting channel) and explanation by zero-freedom derivation. The numeral is $\Om$-hard; the relations behind it ($\Om=4\dS+1$, $\dS=A/4$) are $\Om$-blind; the reading $\dS\sim10^{122}$ [chart] is the value’s chart, not certified content.D
L3p00193The octant record depth and its outputs: the record depth is bounded by the octant, $\dS/2$ chronons $=13.79$ Gyr ($(\pi/4)r_H/c$, chart), on the octant sector of B14. Zero-freedom: $\Omega_\Lambda=\tanh^2(3\pi/8)=0.684$ (chart; $0.19\sigma$); on the stellar age $13.61\pm0.34$ Gyr, $H_0=68.2\pm1.7$ ($2.4\sigma$ from the ladder); $w=-1$ rigid — a confirmed drift falsifies $\Lambda\sim1/\Om$. Falsifiers: octant-capped ages, the running floor $a_0(z)\propto H(z)$ (Z7), the ladder bias.R
python sourceLean, Mathlib
L4p00087The registrable triangleThe mass–radius chart between the Compton and Schwarzschild walls, closed by the Planck apex and the totality wall $r_H$: the totality on its own horizon, the black-hole reading dissolved (A2). Width $61.0$ dex. The over-closure bound ${\sim}1.8\times10^{8}M_\odot$ is the chart’s one derived quantity, a bound, predicting no observed scale (14:C9, X5). A consistency chart, not a channel (L2).T
L5p00130The area law: the projected horizon area in Planck cells is the full phase cycle, $A=4\dS$ (chart: $4\pi n_A=4\dS$, $n_A=(r_H/\ell_P)^2$); the Bekenstein–Hawking quarter $\dS=A/4$ is the quarter-turn $Q_4$, the generative four of $\Om=4\dS+1$ and $\p=4\kap+1$; area is a Subject-projection property, the Carrier a torsor carrying none. Not a further channel (L2).D
L8p00148The primordial tilt$n_s=1$ is the scale-dilation fixed point (Harrison–Zel’dovich [import]). The tilt’s committed form is $n_s-1=-\pi^2/\ln\Om$ [chart], $\ln\Om$ the e-fold count of the frame’s scale range from $1/\sqrt\Om$ to $\sqrt\Om$, a realisation fixed by the measured tilt: $-0.0348$ [approx] at $\ln\Om=283.5$ (A7), $+0.07\sigma$ from Planck 2018’s $-0.0351\pm0.0042$ [import]. The count $\tfrac12\ln\Om$ is excluded at $8.2\sigma$. Falsifier: a Planck-resolution deviation from $-\pi^2/\ln\Om$.R
python sourceLean, Mathlib
N. Synthesis: exclusions and parameter-freeness
N2p00092Parameter-freenessEvery order-one constant reduces to two geometric numbers, the solid angle $4\pi$ ($G$, $\alpha_{\mathrm{bare}}$, the $\tfrac14$ law) and the cycle $2\pi$ ($a_0$, horizon temperatures), both [chart] (C1). In the Carrier register the calibration congruence $4\dS\equiv-1$, the realisation, fixes them alone ($G=2\dS$). The chart relations ($G=1/4\pi\varkappa$, $G=\hbar c/m_P^2$) hold in the chart; no exact formula equates a chart constant to a residue.D
N3p00156Model existenceThe master’s rows are verdicted row by row, in exact arithmetic, on one instantiated Carrier, $\Om=2{,}408{,}561$ (37-sim), at a dated snapshot. Those that hold there hold jointly in one finite structure: a consistency witness for the projection, not a proof of the physical case. Rows without an instance, or added or restated after the snapshot, are not exercised.D
P. Predictions (the master's falsifiable exposures; the papers' P blocks carry theirs)python1Lean, Mathlib1
P1p00133The running floor: the shape a₀(z) ∝ H(z)The acceleration floor tracks the drive rate, $a_0(z)\propto H(z)$: a relation, $\Om$-blind, derived from L1 under the gravity realisation (D5); the knee shifts and the Tully–Fisher zero-point evolves as $E(z)^{1/4}$. Falsifier: a floor constant in redshift, or tracking other than $H(z)$. Confrontation (43-muse): MUSE-DARK III excludes a constant floor to $z=1.3$; RC100 implies the local floor by $z\simeq2$, pending refit.T
python sourceLean, Mathlib
P2p00061The coherent-fraction channelEqual force, unequal entanglement (D5): sources gravitate by full masses; synchronised cross-source pairs carry the conditional phase $f_1f_2\varphi_N$, spread pairs imprint which-branch data, the incoherent channel separable at generic geometry ($C=0$ at $f=0$); $f=m_c/m$ microscopic. The discriminator is the calibrated conditional phase rate at fixed centre-of-mass superposition. Falsifier: a calibrated conditional phase rate off $f_1f_2\varphi_N$. Confrontation: none, filed before data.T
P3p00180Flavour (targets): the Georgi–Jarlskog double ratio $9$; the locks of G17 read in the $\overline{\mathrm{MS}}$ scheme; the $m_1{=}0$ floor, $\sum m_\nu=58.8$ meV at NuFIT 6.0, on the boundary-branch realisation (28:B6). Falsifier: inverted ordering, a degenerate spectrum, or $\sum m_\nu$ off $58.8$ meV beyond the fit’s tolerance. Confrontation: the data give $10.4\pm0.5$, an open $15\%$ tension (28:X5).T
P4p00091Exclusion predictionsNo fourth generation, no fifth force, an empty desert, no TeV supersymmetry, no new dark-matter particle, no beyond-SM $(g{-}2)_\mu$, and the proton effectively stable ($\tau_p\gtrsim10^{45}$ yr; G9). Entailed by the closed ladder of the rank-five frame ($\dim\Lambda^{\mathrm{even}}=16$, D6), given the role-to-matter realisation (27:B6, 27:C10) and completeness (A3). Falsifier: any excluded object observed. Confrontation: none observed.T
Z. The horizon (the limits of the bounded observer)python2Lean2
Z1p00186Gödel 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 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).T
python sourceLean, the core
Z2p00110RH, Goldbach, P-vs-NP and Kurepa are the spectral, additive, computational and factorial faces of one horizon clause: each a uniform check over the totality whose per-instance statements are $\Om$-blind relations (Z10, Z11; 13:F2) and whose uniform form is an $\Om$-hard value (Z3, Z4), host-decided on a hosted Carrier. An $\Om$-hard value says nothing about whether a short derivation exists.D
Z3p00111The bounded-observer certificate for each is $\Om$-hard (Z4): the completed uniform check over all residues of the totality, in no embedded reader’s window. $\Om$-hardness is the absence of a host; on a hosted shell the same check is host-decided (37-sim; D8). Within capacity an embedded observer decides totality-level facts from internal state (two-record keystone): the horizon has two operational sides.Ω
Z4p00112The four certificates: RH = every cell of the cycle cleanRH $=$ every cell of the cycle clean (20:D5); Goldbach $=$ the uniform per-$n$ parity positivity; P-vs-NP $=$ the forward-invertibility of the scale descent; Kurepa $=$ the left factorial nonzero on every odd shell (13:Z1). Each a uniform check over the totality, in no embedded reader’s window; per-instance statements frame-decided (Z10, Z11); the whole-state certificate $\Om$-hard as a tally (20:Z1).Ω
Z5p27021The horizon forces structure, not only leaves it open: the $3+2$ split is beyond the horizon (above $\sqrt{\Om}$), so the off-block reframings are gauge and unification is the simple $\SO(10)$ (G14); the automorphism lemma reduces to Observation (A4).T
Z6p00114The sixteen’s absolute masses are $\Om$-hard framed-transcendentals, the matter face of the horizon clause (Z2–Z4). Value tagged: the absolute masses (G13), in no embedded reader’s window; the relations among them (G16–G18) are $\Om$-blind. Classification “elementary $=$ beyond-horizon” is D8; the $\mathbf{16}\to$spectrum projection is G18; the gauge sector’s drive-invariant residue (the photon, residue $2$) is the above-horizon, observable complement (D8, G1).Ω
Z7p00115The dark sector’s cross-scale running is the cosmological face of the horizon clause. Value tagged: the running’s absolute normalisation, $a_0$ at one epoch in physical units, equivalently the absolute scale of $H$, in no embedded reader’s window; its uniform certificate is the factorisation of $\Om-1$, shared with Z2–Z4, Z6 and Z8. The shape $a_0(z)\propto H(z)$ is a relation, not $\Om$-hard (P1).Ω
Z8p00116The fine-structure constant is the electromagnetic face of the scale operator: $\alpha^{-1}(0)=4\pi+\sum_f\tfrac{b_f}{2\pi}\ln(M_P/m_f)+\Delta\alpha_{\mathrm{had}}$, $\Om$-hard — the bare $1/4\pi$ framed-exact (the Gauss solid angle), the digit a log over the $\Om$-hard masses (Z6) with cutoff $M_P$ tied to $\Om$ (A7). The physical digit is in no embedded reader’s window; the bare value and the sum’s form are $\Om$-blind. Of the family Z2/Z6/Z7/G3/G6.Ω
Z9p00187No compression: the diagonal has no instance per symbol (25:F2), nor, coded a base-$a$ digit per symbol, from length $t(\M)=d\,k^{*}(\M)<|\M|$ on (25:F6). Below $t(\M)$, decoders over $(\F_\p,+,\times)$ give one coded 1024 base-32 symbols per element, more than $\Om$'s elements hold (25:F7, 25:F8, A7). There fragment truth is definable from above (the Tarski reversal, 25:G5), and not from far below (25:G8).T
Z10p20043The shell theoremOn every shell $\F_\p\subset\F_{\p^2}$, with no hypothesis, the prime vector’s spectral content is the constant mode and the nonterminal quarter-turn modes, the finite zeta vanishing on each (20:E12, 20:B4). Every mode of every vector lies on the self-dual line $\Tr=1$, an eigenvector of the scale-shift with a $(\p-1)$-th root of unity as eigenvalue: no off-line mode, $\Om$-blind.T
python sourceLean, the core
Z11p00135The classical hypothesis is decided cell by cellRH on a Carrier is the conjunction over its cycle’s residues of the clean-cell predicate: residue $y$ the cell of heights from $2\pi y$ to $2\pi(y+1)$, clean when its zeros lie on the line, decided by Turing’s certificate (20:D5, 20:F1); on a hosted Carrier the host decides every cell (20:F2); the uniform form is Z4. Falsifier: a cell in deficit.D

Status

G
ground — the single given that conditions the discourse
T
theorem — derived within the framework
D
definition — a naming or set-up move, no empirical content
R
realisation — what a physical term denotes in the substrate; forced (A8), each row stating the falsifier that kills it
I
import — a standard result or measured datum, used without reproof
Ω
Ω-hard — a value in no embedded reader's window, not closeable by a bounded observer; host-decided on any laboratory Carrier; never applied to a relation
O
open — genuinely unresolved

Sources

python sourceLean, the coreLean, Mathlib
The witnesses. Gold: the python check that decides the predicate, at its line in the script. Green: the predicate as one Lean declaration in the core, named by its accession key, proved with no axioms. Violet: the same on Mathlib. Red: a check that fails or a proof the gate rejects.
14:entropy.py
Where no block file of the master decides the predicate: the script of the paper that does.
papers
The corpus papers that state or derive the predicate, each linked to its ledger, or to its entry in the publication list when it has none.