Jcost_phi_eq_phi_minus_half
plain-language theorem explainer
The declaration proves that the recognition cost J at the golden ratio satisfies J(φ) = φ − 3/2 exactly. Researchers resolving the Yang-Mills mass gap in Recognition Science cite this identity to fix the spectral gap Δ as the minimum excitation cost on the φ-lattice. The proof is a direct algebraic reduction that rewrites via the closed-form J(φ) = (√5 − 2)/2 and simplifies with the definition of φ.
Claim. The recognition cost functional satisfies $J(φ) = φ - 3/2$.
background
In Recognition Science the cost functional is J(x) = ½(x + x^{-1}) − 1 on the golden-ratio lattice {φ^n | n ∈ ℤ}. The module derives the Yang-Mills mass gap as the strict spectral gap between the vacuum (J = 0) and every non-trivial φ-ladder excitation, with Δ = J(φ) = (√5 − 2)/2 = φ − 3/2. Upstream Jcost_phi_exact supplies the equivalent closed form J(φ) = (√5 − 2)/2 obtained from the recognition composition law and the definition of φ.
proof idea
The proof is a one-line wrapper that rewrites the left-hand side with Jcost_phi_exact, substitutes the definition of phi, and applies the ring tactic for algebraic simplification.
why it matters
This identity supplies the elementary closed form for the mass gap constant that feeds directly into yang_mills_mass_gap_complete, the final theorem asserting Δ = φ − 3/2 > 0 is the minimum J-cost on the φ-lattice. It completes the first step of the central theorem in the module, confirming the exact RS Yang-Mills mass gap. Within the framework it follows from J-uniqueness (T5) and phi-forcing (T6) in the indisputable monolith.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.