phi_pos
plain-language theorem explainer
The declaration establishes that the self-similar fixed point φ is strictly positive. Researchers deriving proton radii via the phi-ladder in Recognition Science would invoke this to keep all mass and radius expressions in the positive reals. The proof is a one-line wrapper that unfolds the definition of φ and applies the positivity tactic.
Claim. $0 < φ$, where $φ$ is the unique positive self-similar fixed point of the Recognition Composition Law.
background
In the ProtonRadius module the symbol φ is imported from JcostCore as the fixed point satisfying the self-similarity condition that follows from the J-cost functional. The module develops estimates for the proton charge radius using Recognition Science mass formulas of the form yardstick · φ^(rung − 8 + gap(Z)) on the phi-ladder. This positivity result is a prerequisite for all subsequent inequalities involving radii and form factors. The paper RS_Proton_Radius_Puzzle.tex places the proton radius puzzle inside the eight-tick octave and D = 3 spatial dimensions of the framework.
proof idea
The proof is a one-line wrapper that unfolds the definition of φ and applies the positivity tactic from Mathlib.
why it matters
This positivity statement supports the chain of results that produce proton_radius_estimate and proton_radius_positive inside the same module. It anchors the phi-ladder constructions used for mass formulas and ensures consistency with T6, where φ is forced as the self-similar fixed point, together with the positive constants ħ = φ^−5 and G = φ^5 / π.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.