etaBExactRungCert
Baryon asymmetry η_B sits at φ-rung 44.
plain-language theorem explainer
Three combinatorial expressions for the baryon-to-photon ratio rung all evaluate to the integer -44 at three spatial dimensions. A cosmologist working in Recognition Science would cite this to anchor the exact φ-ladder position of η_B. The proof is a term-mode construction that supplies the dimension witness, the chirality-torsion witness, the fermionic-DOF witness, and the three pairwise agreement lemmas.
Claim. At spatial dimension three the expressions $1 - D^2(D+2)$, $-(bitFlipCount(0) times |torsionGap(0,1)|)$, and $1 - fermionicDOF/2$ each equal $-44$ and are pairwise equal, where these expressions are the three reparameterizations of the integration gap minus one.
background
Recognition Science fixes the baryon-to-photon ratio η_B on the φ-ladder via the integration gap at D=3. The gap equals D²(D+2)-1 and evaluates to 44 when D=3. The module re-expresses this single integer through three combinatorial routes: the direct dimension formula, the product of bit-flip count on the 3-cube Gray code with the torsion gap from the CW-filtration spectrum, and the fermionic degree-of-freedom count after matter-antimatter doubling. The module doc states these are not independent forcing routes but distinct reparameterizations of the same underlying integer.
proof idea
Term-mode construction of the EtaBExactRungCert structure. It directly references the dimension witness lemma at D=3, the chirality equation lemma, the fermionic equation lemma, the AB and AC agreement lemmas, the BC agreement lemma, the chirality-product bridge lemma, and the fermionic-half bridge lemma.
why it matters
The declaration unifies the three witnesses for the -44 rung of η_B and confirms they all reduce to integrationGap D -1 =44 at D=3. It thereby closes the combinatorial derivation of the exact φ-ladder position required by the eight-tick octave and the forcing of D=3. No downstream theorems are listed, but the result supplies the concrete integer that later mass and coupling formulas on the φ-ladder will use.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.
papers checked against this theorem (showing 1 of 1)
-
DBI scalar fields tie ΛCDM on late-time data, H₀ near 73
"we use rd as a free parameter, allowing it to be constrained directly by observational data"