vacuum
plain-language theorem explainer
The vacuum supplies the zero-rung gauge bond configuration on the 12 edges of Q₃, serving as the reference state whose total J-cost is exactly zero. Researchers deriving the Yang-Mills mass gap or the cosmological constant from the J-functional would cite this as the ground state against which excitations are measured. It is introduced by a direct structural assignment of the constant zero function to the bonds field.
Claim. The vacuum gauge bond configuration is the record that assigns rung index 0 to each of the 12 edges of the cube graph Q₃, where rung 0 corresponds to the multiplier φ⁰ = 1.
background
Recognition Science places gauge fields on the cube graph Q₃ whose 12 edges carry integer rung indices n ∈ ℤ; the bond multiplier is then φ^n. The structure GaugeBondConfig packages these indices into a single object whose J-cost is obtained by summing J(φ^{n_e}) over the edges. The functional J(x) = ½(x + x^{-1}) − 1 is nonnegative on the positive reals and vanishes only at x = 1, a fact established by the upstream cost lemmas in MultiplicativeRecognizerL4 and ObserverForcing. The module document states that the φ-lattice is the discrete substrate forced by T2 + T6 and that the vacuum (J = 0) is separated from every nontrivial excitation by the exact gap Δ = J(φ) = (√5 − 2)/2.
proof idea
This is a direct definition that constructs the GaugeBondConfig record by setting the bonds field to the constant function returning 0 for any input.
why it matters
This definition anchors the mass gap derivation by providing the zero-cost reference against which all excitations are measured. It feeds the cosmological-constant derivations (hypothesis3, jcost_cancellation, Lambda_no_fine_tuning) and the climate nonnegativity theorems (climateJCost_nonneg, vacuum_climate_zero_cost). Within the framework it realizes the vacuum state required by T5 J-uniqueness and the spectral-gap statement that any non-unit φ-ladder excitation costs at least Δ.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.