phi8_val
plain-language theorem explainer
Golden ratio φ obeys φ^8 = 21φ + 13. Baryon asymmetry calculations in Recognition Science cite this reduction when bounding φ^44 from below. The tactic proof recalls φ² = φ + 1, derives the next two powers by nlinarith, and closes the equality with further linear arithmetic.
Claim. For the golden ratio φ, φ^8 = 21φ + 13.
background
The module treats baryon asymmetry η_B from the phi-ladder under Recognition Science, with the prediction η_B ≈ φ^{-44} and the bound φ^44 > 10^8. The golden ratio satisfies the quadratic identity φ² = φ + 1, supplied by upstream phi_sq_eq in Constants and in PhiLadderLattice. This identity is the base for all higher-power reductions on the ladder.
proof idea
The proof binds phi_sq_eq to h2. It obtains φ^3 = 2φ + 1 and φ^4 = 3φ + 2 by nlinarith. It then applies nlinarith with the non-negativity of (φ^4)^2 to reach the target equality.
why it matters
This supplies the exact value used by phi8_gt_46 and phi44_gt_1e8 to bound the asymmetry parameter. It is referenced inside the CoherenceTimeCert structure for quantum coherence times. In the framework it realizes the exact scaling for the eight-tick octave on the phi-ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.