PhiRungLadderCert
plain-language theorem explainer
Certificate structure packaging the baryon-asymmetry rung (−44) with its arithmetic factorizations through 11 (the passive-mode count). Cosmologists placing η_B on the φ-ladder cite this bundle. Fields are pure equalities; the inhabited instance is discharged by reflexivity and numeric normalization.
Claim. A certificate of four equalities: the baryon-asymmetry rung equals $-44$; $44 = 4 \times 11$; $44 + 11 = 55$; and $55 = 5 \times 11$.
background
The module records the baryon-asymmetry rung on the Recognition Science φ-ladder. Masses and dimensionless ratios sit at integer rungs $r$ with scale $\varphi^r$ (or $\varphi^{-r}$); here $\eta_B$ is assigned rung $-44$, so $\varphi^{44} = 1/\eta_B$ in RS-native units.
The integer 11 is the passive-mode count appearing in the eight-tick / octave arithmetic of the forcing chain. The certificate factors 44 and 55 through 11: $44 = 4 \cdot 11$ and $55 = 5 \cdot 11$, with the intermediate sum $44 + 11 = 55$ linking the baryon rung to an $N_e$-style count.
Upstream, eta_B_rung_val is the constant definition $-44$. The surrounding module proves the related factorizations (baryon rung factorization, $N_e$ arithmetic) that this structure packages as a single Prop bundle.
proof idea
No proof body: this is a structure whose four fields are equality propositions. Inhabitation is separate. The downstream theorem builds an instance by rfl on the rung definition and norm_num on the three natural-number arithmetic identities.
why it matters
This is the certificate type for the module's baryon-rung theorem. The parent theorem phi_rung_ladder_cert inhabits it and is labeled THE BARYON-RUNG THEOREM: the baryon asymmetry rung (−44) sits on the φ-ladder with arithmetic encoding the passive-mode count.
In the RS framework the φ-ladder (forced by T5–T6 J-uniqueness and the golden fixed point) organizes dimensionless cosmology numbers. Packaging $\eta_B$ at $-44$ with the $4\cdot 11$ and $5\cdot 11$ factorizations ties the observed baryon asymmetry scale to the same 11-mode / eight-tick arithmetic used elsewhere in the octave structure (T7). Status reported for the module: 0 sorry, 0 axiom.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.