hierarchy_phi_power_structure
plain-language theorem explainer
Mass ratios separated by a positive integer rung difference Δr on the phi-ladder equal φ^Δr and are strictly greater than 1. Researchers modeling fermion mass hierarchies cite the result when bounding the φ^6 and φ^11 structures listed under registry item P-002. The proof is a short tactic calculation that substitutes the candidate ratio and invokes the upstream fact phi > 1 together with monotonicity of real exponentiation.
Claim. For every positive integer $Δr$, there exists a real number $r$ such that $r = φ^{Δr}$ and $r > 1$.
background
The module supplies calculated proofs for registry predictions, including the fermion mass hierarchy (P-002) with explicit φ^6 and φ^11 structure. The golden ratio φ is the self-similar fixed point whose strict inequality φ > 1 is supplied by the upstream lemma one_lt_phi (imported from Constants and PhiSupport). The phi-ladder is the Recognition Science mass scaling in which ratios are integer powers of φ corresponding to rung differences Δr.
proof idea
Tactic-mode proof. The goal is witnessed by substituting the ratio (phi : ℝ)^Δr. The hypothesis phi > 1 is obtained from one_lt_phi. A calc block rewrites 1 as 1^Δr and applies pow_lt_pow_left₀ to obtain the strict inequality, using Nat.pos_iff_ne_zero.mp on the positivity assumption for Δr.
why it matters
The theorem supplies the core power inequality needed for the fermion mass hierarchy bounds inside registry_predictions_cert_exists. It directly populates the P-002 entry of the Registry Predictions certificate and encodes the self-similar fixed-point property of φ into concrete mass-ratio statements used by the unification layer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.