Jcost_phiLadder_zero
plain-language theorem explainer
Recognition Science sets the vacuum cost to zero by evaluating the J-functional at the zero rung of the phi-ladder. This base result is cited in derivations of the mass gap for Yang-Mills theories within the framework. The term proof simplifies the ladder definition at n=0 directly to the unit cost lemma.
Claim. The recognition cost of the zero-rung element on the golden-ratio ladder vanishes: $J(1) = 0$, where $J(x) = ½(x + x^{-1}) - 1$.
background
In the Yang-Mills mass gap module the phi-ladder is defined by PhiLadder n := phi^n for n in Z, supplying the discrete substrate for gauge excitations. The J-cost functional satisfies J(1) = 0 by the upstream lemma Jcost_unit0, which follows from the algebraic form J(x) = (x-1)^2/(2x). The module doc states that the vacuum sits at n=0 on this lattice, with the gap emerging from the recognition composition law together with the phi-forcing chain.
proof idea
One-line term-mode wrapper that unfolds PhiLadder 0 to 1 and applies the lemma Jcost_unit0.
why it matters
This base case anchors contractible_bond_zero_cost (massless U(1) photons) and vacuum_cost_zero (total gauge cost zero). It fills the n=0 slot in the module's spectral gap argument, where the minimum nonzero excitation costs J(phi) = (√5-2)/2 > 0, consistent with T5 J-uniqueness and T6 phi fixed point.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.