saturation_exponent
plain-language theorem explainer
Defines the complementary φ-ladder exponent as the integer 45. Cosmology proofs cite it as the partner to the η_B rung −44, so that −44 + 45 = 1 and η_B × φ⁴⁵ = φ at the rung level. The body is a bare integer assignment, not a derived computation.
Claim. The saturation exponent is the integer $45$, used as the complementary $\varphi$-power opposite the baryon-asymmetry rung $-44$.
background
In the exact baryon-asymmetry module, $\eta_B$ is placed on the $\varphi$-ladder at rung $-44$. The structural claim is that $44 = 4 \times 11$: generation-0 chirality flip count times the CW torsion gap $\Delta\tau_{01}$. The same product seeds the fine-structure formula $\alpha^{-1} = 44\pi \times \exp(-w_8 \ln\varphi / 44\pi)$.
The complementary scale is written $\Theta_{\mathrm{crit}} = \varphi^{45}$ in the extended framework. Adding the two defined exponents gives $-44 + 45 = 1$, so $\eta_B \times \varphi^{45} \approx \varphi$ at the rung level: matter content sits one golden-ratio rung above the complementary pair. $\varphi$ itself is the self-similar fixed point forced at T6.
Upstream, the same integer appears in BaryonAsymmetryDerivation as a bare definition; the exact module re-exports it so local rung arithmetic and certificates can name one constant.
proof idea
No proof. The declaration is a definitional abbreviation: the integer literal $45$ inhabiting $\mathbb{Z}$. Downstream theorems such as rung_sum and eta_B_times_saturation discharge the arithmetic $-44 + 45 = 1$ by norm_num or simp on this constant and eta_B_rung.
why it matters
Without a named complementary exponent, the $\varphi$-power balance $\eta_B \times \varphi^{45} = \varphi$ cannot be stated as a formal identity. Downstream, eta_B_times_saturation proves $\mathrm{eta_B_rung} + \mathrm{saturation_exponent} = 1$; rung_sum / rung_sum_named restate $-44 + 45 = 1$; and both BaryonAsymmetryCert and BaryonAsymmetryExactCert package the field phi_rung_connection (or the equivalent $\varphi^{-44}\cdot\varphi^{45} = \varphi$) around this constant.
In the Recognition chain this is bookkeeping on the $\varphi$-ladder forced by T5–T6 (J-uniqueness and the golden fixed point), not a new dynamical derivation of 45. The honest status in the parent derivation is that both $-44$ and $45$ are hypothesis-grade rung assignments; the theorems only certify integer arithmetic between them.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.