EtaBCert
plain-language theorem explainer
Certificate structure packing five claims for the RS baryon-to-photon prediction: φ^{-44} lies in (5.5×10^{-10}, 7.5×10^{-10}), the Planck 2018 central value 6.1×10^{-10} sits inside, the integer 44 factors as chirality flip-count times torsion gap, and the structural asymmetry is positive. Cosmologists citing the RS η_B interval use this bundle. As a structure it has no proof body; the companion instance supplies the witnesses.
Claim. A certificate asserting $\varphi^{-44} > 5.5\times 10^{-10}$, $\varphi^{-44} < 7.5\times 10^{-10}$, that the observed central value $6.1\times 10^{-10}$ lies strictly between those bounds, that the structural integer $44$ equals (bit-0 flip count on the eight-tick cycle) times the absolute torsion gap between generations $0$ and $1$, and that the structural baryon-to-photon ratio is positive.
background
This module certifies the Recognition Science interval prediction for the baryon-to-photon ratio: $\varphi^{-44}\in(5.5,7.5)\times 10^{-10}$. The Planck 2018 central value $\eta_B=(6.10\pm 0.04)\times 10^{-10}$ falls inside. The same integer 44 that appears in the fine-structure formula $\alpha^{-1}=44\pi,\exp(-w_8\ln\varphi/44\pi)$ is recovered here as a product of two geometric counts.
Bit-flip count on axis 0 of the eight-tick Gray-code cycle equals 4. The torsion gap $\Delta\tau_{01}$ between the first two CKM generations has absolute value 11. Their product is 44. The structural asymmetry $\eta_B^{\mathrm{struct}}=J_{CP}/g_\star$ is used only for sign and smallness; its raw magnitude is scaffold-level (order $10^{-7}$) because the washout constant is not yet derived.
Bounds on $\varphi^{\pm 44}$ are obtained from the Fibonacci closed form $\varphi^{44}=F_{44}\varphi+F_{43}$ with $F_{44}=701408733$, $F_{43}=433494437$ and a crude enclosure $\varphi\in(1.61,1.62)$, which already places $\varphi^{-44}$ near $6.4\times 10^{-10}$.
proof idea
Pure structure definition: five named fields of type Prop, no proof body. Downstream, the instance etaBCert fills each field by an already-proved lemma: phi_pow_neg44_lower and phi_pow_neg44_upper for the interval endpoints, observed_eta_in_interval for the Planck central value, rung_44_equals_flip_times_torsion for the factorization $44=\mathrm{bitFlipCount}(0)\cdot|\mathrm{torsionGap},0,1|$, and eta_B_positive for positivity of the structural ratio. No new algebra occurs at this declaration.
why it matters
Master certificate for the cosmology-side $\eta_B$ claim. Its sole consumer is the verified instance etaBCert, which discharges every field. The structural field ties baryon asymmetry to the same 44 that governs $\alpha^{-1}$, linking electromagnetism and cosmology through chirality (eight-tick Gray code, T7) and CKM torsion. Positivity of $\eta_B^{\mathrm{struct}}$ is the genuine derived content (matter over antimatter); the magnitude interval is an RS-native $\varphi$-ladder prediction, not a fit. Open scaffolding remains on the washout constant that would convert the structural ratio into the observed magnitude.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.