pith. machine review for the scientific record. sign in
theorem proved term proof high

phi_11_hierarchy_lower

show as:
view Lean formalization →

The inequality establishes phi^11 > 180 as a conservative lower bound supporting the phi-ladder for fermion mass hierarchies. Physicists modeling particle mass ratios via Recognition Science predictions would cite this result. The proof substitutes the Fibonacci closed form for phi^11 and discharges the comparison with linear arithmetic on the bound phi > 1.61.

claim$180 < phi^{11}$ where $phi = (1 + sqrt(5))/2$ is the golden ratio.

background

This theorem sits in the module of calculated proofs for registry predictions, covering the fermion mass hierarchy prediction P-002 with explicit phi^6 and phi^11 structure. The local setting uses the phi-ladder mass formula in which masses scale as yardstick times phi to a power involving rung and gap(Z), together with the Recognition Composition Law and the eight-tick octave. Upstream results supply the key identity phi^11 = 89 phi + 55 by Fibonacci recurrence and the tighter bound phi > 1.61.

proof idea

The term-mode proof first rewrites the goal via the lemma phi^11 = 89 * phi + 55, then invokes linear arithmetic on the resulting inequality using the supplied lower bound phi > 1.61.

why it matters in Recognition Science

The result supplies the phi_11 lower bound inside the registry predictions certificate that confirms the mass hierarchy prediction P-002. It aligns with the Recognition Science phi-ladder and the mass formula yardstick * phi^(rung - 8 + gap(Z)), closing one of the calculated proofs listed in the module for the COMPLETE_PROBLEM_REGISTRY.

scope and limits

formal statement (Lean)

 150theorem phi_11_hierarchy_lower : (180 : ℝ) < (phi : ℝ)^11 := by

proof body

Term-mode proof.

 151  rw [phi_eleventh_eq]
 152  linarith [phi_gt_onePointSixOne]
 153
 154/-- **HIERARCHY STRUCTURE**: Mass ratios are φ-powers of integer differences. -/

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (8)

Lean names referenced from this declaration's body.