phi45_scale
plain-language theorem explainer
Defines the complementary scale φ⁴⁵ used throughout the exact baryon-asymmetry derivation. Cosmologists and RS auditors cite it when stating the φ⁴⁴/φ⁴⁵ balance η_B × φ⁴⁵ = φ. The body is a one-line power of the golden ratio in RS-native units.
Claim. Let $\varphi$ be the golden ratio. The complementary scale is the real number $\varphi^{45}$.
background
The module closes the baryon asymmetry derivation on the φ-ladder: η_B sits on rung −44, and the structural identity η_B × φ⁴⁵ = φ is proved as a formal theorem. The electroweak formula is η_B = (ε_CP / g★) × washout_factor, with all factors RS-derived (Jarlskog positivity, SM g★ = 106.75 from Q₃, sphaleron rate at T_EW).
The rung 44 equals 4 × 11 (generation-0 chirality flip count times the CW torsion gap Δτ₁₂). The same product seeds α⁻¹. The complementary exponent 45 is one rung above that pair, so φ⁻⁴⁴ × φ⁴⁵ = φ: matter content sits exactly one self-similar overshoot above the −44/45 pair.
Here φ is the unique self-similar fixed point forced by T6 from J-uniqueness (T5) and the Recognition Composition Law.
proof idea
Pure definition: unfold to the integer power φ^(45 : ℤ) with no further proof obligations. Downstream lemmas (e.g. phi45_scale_gt_one) unfold this name and apply one_lt_zpow₀ with one_lt_phi.
why it matters
Named scale for the φ⁴⁴/φ⁴⁵ balance that is the module's main physical claim. Feeds eta_B_phi45_balance (η_B × φ⁴⁵ = φ), the ratio form eta_B_eq_phi_over_phi45_scale, the positivity lemma phi45_scale_gt_one, full_derivation_chain, and the package certificate BaryonAsymmetryExactCert (which records the identity φ⁻⁴⁴ × φ⁴⁵ = φ among its fields).
Ties the baryon-to-photon ratio to the same 4 × 11 product that governs α⁻¹, and to the forcing chain T5–T6 (J-uniqueness → φ forced). The golden ratio appears as the self-similar overshoot of the complementary pair, not as an inserted constant.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.