phi45_scale_gt_one
plain-language theorem explainer
The complementary scale φ⁴⁵ is strictly larger than 1. Cosmology proofs that rewrite η_B as φ/φ⁴⁵ or assemble the baryon-asymmetry certificate cite this positivity fact. The argument is a one-line application of strict growth of integer powers for bases greater than one, using 1 < φ and the exponent 45 > 0.
Claim. With $\varphi$ the golden ratio and the complementary scale defined by $\varphi^{45}$, one has $1 < \varphi^{45}$.
background
The module closes the RS baryon-asymmetry story by placing η_B on φ-rung −44 and proving the pure φ-power identity η_B × φ⁴⁵ = φ. The complementary scale is the definition phi45_scale := φ^(45 : ℤ), the large partner of the −44 rung that appears in the balance theorem.
Upstream, Constants.one_lt_phi records 1 < φ (from the closed form (1+√5)/2). Integer powers of a real base greater than one are strictly increasing in the exponent when the exponent is positive, which is the Mathlib fact one_lt_zpow₀ used here. The same φ is forced as the self-similar fixed point (T6) and governs J, the mass ladder, and the eight-tick period.
Locally this lemma is only the size statement φ⁴⁵ ≫ 1; the structural content (44 = 4×11 from flip count and torsion gap) lives in sibling results.
proof idea
Unfold phi45_scale to φ^(45 : ℤ). Apply Mathlib's one_lt_zpow₀ to the base inequality one_lt_phi : 1 < φ, supplying the exponent witness (0 : ℤ) < 45 by norm_num. The result is exactly 1 < φ⁴⁵.
why it matters
The certificate baryon_asymmetry_exact_cert packages this fact as the field theta_large, alongside the rung product 4×11 = 44 and the identity φ^(−44)·φ⁴⁵ = φ. The ratio form eta_B_eq_phi_over_phi45_scale needs 0 < φ⁴⁵ to divide; it obtains that by lt_trans from this lemma. full_derivation_chain records the same positivity in the end-to-end RCL → T5/T6 → Q₃ → Gray-code flips → torsion gap → rung −44 narrative.
Within the framework landmarks, the overshoot factor φ is the T6 fixed point; the −44/45 pair is the algebraic shadow of the chirality-flip × torsion product that also seeds α⁻¹. The lemma itself is pure φ-arithmetic, not an empirical claim; empirics sit in the rung assignment η_B ≈ φ⁻⁴⁴.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.