bond_cost_nonneg
plain-language theorem explainer
The lemma shows that each of the twelve bonds in a gauge configuration on Q3 carries non-negative J-cost. Researchers deriving the Yang-Mills mass gap from the Recognition Science J-functional would cite it to bound total excitation energy from below. The proof is a one-line term application of the general Jcost non-negativity result once positivity of the phi-ladder rung is supplied.
Claim. For any gauge bond configuration $cfg$ and edge index $e$, $0 ≤ J(φ^{cfg.bonds(e)})$, where $J(x) = ½(x + x^{-1}) - 1$.
background
In the Yang-Mills mass gap module a GaugeBondConfig is a structure that assigns an integer rung index to each of the twelve edges of the Q3 lattice; the vacuum configuration places every bond at rung zero. PhiLadder(n) denotes the nth power of the golden ratio φ, so each bond multiplier is realized as an element of the phi-lattice. The upstream lemma Jcost_nonneg states that J(x) ≥ 0 for every positive real x, proved via the AM-GM inequality or the equivalent squared representation J(x) = (x-1)^2 / (2x).
proof idea
The proof is a direct term-mode application of Jcost_nonneg to the positivity fact phiLadder_pos (cfg.bonds e). No additional rewriting or case analysis is performed.
why it matters
The result is invoked by the sibling lemma bond_le_total to conclude that any single bond cost is at most the total gauge cost. It thereby supports the module's central claim that every non-vacuum phi-ladder excitation carries J-cost at least Δ = J(φ) > 0, furnishing the strict spectral gap required for the Recognition Science resolution of the Yang-Mills mass gap (T5-T8 forcing chain and RCL).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.