theorem proved term proof

`vacuum_unique_zero_cost`

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

formal statement (Lean)

 246theorem vacuum_unique_zero_cost (cfg : GaugeBondConfig)
 247    (h : totalGaugeCost cfg = 0) : ∀ e : Fin 12, cfg.bonds e = 0 := by

proof body

Term-mode proof.

 248  intro e
 249  by_contra hn
 250  have hpos := spectral_gap_strict (cfg.bonds e) hn
 251  have hle := bond_le_total cfg e
 252  linarith
 253
 254/-! ## §6  Non-Abelian Specificity: Why U(1) Is Massless -/
 255
 256/-- A gauge bond is **contractible** iff its rung is 0. -/

depends on (18)

Lean names referenced from this declaration's body.

rung in IndisputableMonolith.Compat.Constants decl_use
U in IndisputableMonolith.Constants.RSNativeUnits decl_use
rung in IndisputableMonolith.Engineering.AsteroidOreSpectroscopy decl_use
A in IndisputableMonolith.Foundation.IntegrationGap decl_use
is in IndisputableMonolith.Foundation.OptionAEmpiricalProgram decl_use
is in IndisputableMonolith.Foundation.SimplicialLedger.EdgeLengthFromPsi decl_use
is in IndisputableMonolith.GameTheory.MechanismDesignFromSigma decl_use
A in IndisputableMonolith.Masses.Anchor decl_use
rung in IndisputableMonolith.Masses.AnchorPolicy decl_use
rung in IndisputableMonolith.Masses.RSBridge.Anchor decl_use
is in IndisputableMonolith.Mathematics.RamanujanBridge.MockThetaPhantom decl_use
A in IndisputableMonolith.Modal.Actualization decl_use
U in IndisputableMonolith.Recognition decl_use
rung in IndisputableMonolith.RSBridge.Anchor decl_use
bond_le_total in IndisputableMonolith.Unification.YangMillsMassGap decl_use
GaugeBondConfig in IndisputableMonolith.Unification.YangMillsMassGap decl_use
spectral_gap_strict in IndisputableMonolith.Unification.YangMillsMassGap decl_use
totalGaugeCost in IndisputableMonolith.Unification.YangMillsMassGap decl_use