hierarchy_phi_power_structure
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.
claimFor 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 in Recognition Science
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.
scope and limits
- Does not compute explicit mass values for named particles.
- Does not derive the phi-ladder from the forcing chain T0-T8.
- Does not incorporate gap(Z) corrections from the full mass formula.
Lean usage
have h := hierarchy_phi_power_structure 6 (by norm_num : 6 > 0)formal statement (Lean)
155theorem hierarchy_phi_power_structure (Δr : ℕ) (hΔr : Δr > 0) :
156 ∃ (ratio : ℝ), ratio = (phi : ℝ)^Δr ∧ ratio > 1 := by
proof body
Tactic-mode proof.
157 use (phi : ℝ)^Δr
158 refine ⟨rfl, ?_⟩
159 have h1 : phi > 1 := one_lt_phi
160 have h_ge : Δr ≥ 1 := hΔr
161 calc 1 = 1^Δr := (one_pow Δr).symm
162 _ < phi^Δr := by
163 apply pow_lt_pow_left₀ h1 (by norm_num)
164 exact Nat.pos_iff_ne_zero.mp hΔr
165
166/-! ## Section: Combined Registry Certificate -/
167
168/-- **CERTIFICATE**: Registry predictions with calculated bounds. -/