gauge_cost_ge_gap
plain-language theorem explainer
Any non-trivial gauge bond configuration on the 12 edges of Q₃ has total cost at least the mass gap Δ = J(φ). Researchers resolving the Yang-Mills mass gap via Recognition Science cite this as the quantitative lower bound linking non-triviality to the spectral gap. The proof unpacks a witness edge from the non-triviality hypothesis and chains the per-bond spectral gap through the total cost inequality via le_trans.
Claim. For any gauge bond configuration $cfg$ on the twelve edges of $Q_3$ that is non-trivial, the mass gap satisfies $Δ ≤$ total gauge cost of $cfg$, where $Δ = J(φ) = (√5 - 2)/2$.
background
GaugeBondConfig is a structure assigning an integer rung index to each of the 12 edges of the cube Q₃, with the vacuum defined by all indices at rung 0. The mass gap Δ is J(φ) = (√5 - 2)/2, the minimal positive cost on the φ-ladder. totalGaugeCost sums the individual J-costs over the bonds. The module derives the Yang-Mills mass gap from the J-cost functional alone, as stated in the module doc: the recognition cost functional J(x) = ½(x + x⁻¹) − 1 has a strict spectral gap between the vacuum and every non-trivial excitation.
proof idea
The term proof unpacks the non-triviality witness ⟨e, he⟩, applies the spectral_gap lemma to the bond at edge e to obtain massGap ≤ cost of that bond, and chains the inequality to the total cost via le_trans with bond_le_total.
why it matters
This supplies the quantitative lower bound for the central theorem in the Yang-Mills mass gap resolution (QG-005). It connects the per-bond spectral gap to the global configuration cost, using the φ-ladder and J-cost from T5 and T6. The module doc notes that the gap emerges from the Recognition Composition Law together with the φ-forcing chain and is universal across the three gauge sectors.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.