phi_sq_eq
plain-language theorem explainer
The golden ratio satisfies φ² = φ + 1. Recognition Science derivations of self-similar scaling, J-cost, and phi-ladder ratios cite this identity repeatedly. The tactic proof unfolds the explicit definition of phi, invokes the square identity for √5, and finishes via ring normalization plus linear combination.
Claim. Let φ = (1 + √5)/2. Then φ² = φ + 1.
background
The Constants module fixes RS-native units with the fundamental time quantum τ₀ equal to one tick. Phi is the positive root of x² - x - 1 = 0, equivalently (1 + √5)/2. The upstream theorem in PhiLadderLattice states: “The defining identity of the golden ratio: φ² = φ + 1.”
proof idea
Tactic proof: simp only [phi] reduces to the explicit form; norm_num and Real.sq_sqrt establish (√5)² = 5; ring_nf followed by linear_combination (1/4) * hsq completes the algebraic identity.
why it matters
This identity is invoked by forty downstream results, including beautyScore_at_phi (beauty score equals 3/2 − φ), adjacencyGap_eq, phi_golden_recursion, phi_cubed_eq, and alfvenToSolarWindRatio_gt_one. It encodes the self-similar fixed point T6 of the forcing chain and supplies the recurrence underlying phi-ladder mass formulas and RCL applications.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.
papers checked against this theorem (showing 6 of 6)
-
Exact solution obtained for 2D Ising model with next-nearest couplings
"The critical point for the ferromagnetic-paramagnetic phase transition is located at the golden ratio xc = e−2Kc = (√5−1)/2 , 1/Kc = 4.15617384.. for the cubic Ising lattice"
-
Pulse ordering shapes pair-creation spectra but not total yield
"quasiperiodic (Fibonacci-ordered) structure, where the amplitudes follow a deterministic but aperiodic sequence generated by the Fibonacci substitution rule"
-
Strong locality forms a tetrahedron in reduced Bell space
"V_SL/V_NS = 1/3, V_Q/V_NS = π²/16 ≈ 0.62"
-
Multi-head attention energy rises monotonically along gradient flows
"Condition 8 simplifies to (H−1)ρ ≤ 1−ρ², i.e., ρ² + (H−1)ρ − 1 ≤ 0. The positive root is c*(H) = (√((H−1)²+4) − (H−1))/2."
-
All fermion masses and α from one equation and the cube
"T6 (φ as hierarchy base): additive scale closure forces r² = r + 1; the unique positive real is φ = (1+√5)/2. Lean: Constants/phi_sq_eq, phi_irrational, PhiNecessityCert."
-
One golden-ratio curve organizes four periodic-table trends at once
"Two golden-ratio identities, IE_1(G_p)/IE_1(G_{p+1}) ≈ φ^{1/4} on three heavy noble-gas pairs and IE_1(halogen)/IE_1(alkali) ≈ φ^2 on four within-period pairs"