totalCost_zero_at_vacuum
plain-language theorem explainer
The total Lagrangian cost functional on the Recognition manifold vanishes when the sector assignment is the constant function unity, i.e., every SM sector sits at the recognition vacuum. Workers closing the structural skeleton for the Standard Model in Recognition Science cite this to confirm tree-level vacuum energy is zero before proceeding to the Wightman/OS bridge. The proof is a one-line term reduction that unfolds the sum-of-sectors definition and simplifies with the per-sector zero-cost lemma.
Claim. Let $r$ be the constant map $r(s)=1$ for each sector $s$ in the decomposition into gauge-kinetic, fermion-kinetic, Yukawa, and Higgs-potential terms. Then the total cost, defined as the sum of the four individual sector costs, satisfies $r(s)=1$ for all $s$ implies total cost equals zero.
background
The module treats the Standard Model Lagrangian as four canonical sectors on the Recognition manifold, each equipped with a J-cost functional that vanishes at unity. totalCost is the direct sum of the four sector costs with no cross-sector mixing at tree level. This supplies the structural opening that links existing GaugeBosonLagrangian, Yukawa, and Higgs work into a form ready for the Wightman/OS bridge in S1.
proof idea
The term proof first unfolds totalCost into the explicit four-term sum of sectorCost applications. It then simplifies by invoking the upstream lemma sectorCost_zero_at_vacuum (itself reduced to Cost.Jcost_unit0), which sets each summand to zero.
why it matters
The result populates the total_vacuum_zero field of smLagrangianCert, the certificate that collects vacuum-zero, reciprocal-symmetry, and nonnegativity properties for the SM skeleton. It confirms J-cost vanishes at the recognition vacuum across all sectors, consistent with T5 J-uniqueness and the Recognition Composition Law. The theorem closes one structural prerequisite for the full A1 closure and the S1 bridge; the module itself reports zero sorry and zero axiom.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.