phi_rung_ladder_cert

Recognition Science places dimensionless observables on a discrete φ-ladder: a quantity at rung $r$ scales as a fixed yardstick times $\varphi^{r}$ (with an optional gap correction). In this module the baryon asymmetry $\eta_B$ is assigned rung 44, so $\eta_B\sim\varphi^{-44}$.

The certificate packages that assignment together with three elementary factorizations of 44 and 55. The factor 11 is the integer nearest the RS coherence scale $Z_{\mathrm{cf}}=\varphi^5\in(11,12)$; the factors 4 and 5, and the sum $44+11=55$, are the arithmetic links the module records to the eight-tick period and the passive-mode count.

Local setting (module doc): the file proves only these rung and arithmetic relations, with status 0 sorry and 0 axiom. Upstream, the certificate structure itself is the sole dependency: four fields that must be inhabited.

The theorem builds an instance of the baryon-rung certificate structure field by field. The rung identity $\eta_B$-rung $=-44$ is definitional, discharged by rfl. The three Nat equalities $44=4\cdot 11$, $44+11=55$, and $55=5\cdot 11$ are closed by norm_num. No external lemmas are required beyond the structure declaration and the already-defined rung value.

This is the module’s named Baryon-Rung Theorem: it locks $\eta_B$ onto the φ-ladder at $-44$ and records the integer skeleton that ties that rung to the passive-mode count (factors of 11) and to the eight-tick octave (the 4 in $44=4\times 11$). In the broader forcing chain the eight-tick period is T7; the nearby integer 11 sits next to $Z_{\mathrm{cf}}=\varphi^5$. Downstream use is not yet wired in this graph (used_by empty), so the certificate presently stands as the closed arithmetic anchor for any later cosmology lemma that needs the baryon rung or its factorizations.