totalCost_nonneg
plain-language theorem explainer
If a positive real is assigned to each of the four Standard Model Lagrangian sectors, the total J-cost summed across sectors is nonnegative. This nonnegativity is invoked when building the SM Lagrangian certificate. The proof unfolds the additive definition of totalCost and reduces the claim to four independent calls to the per-sector nonnegativity lemma followed by linear arithmetic.
Claim. Let $r$ map each of the four sectors (gauge kinetic, fermion kinetic, Yukawa, Higgs potential) to a positive real. Then the sum of the four sector J-costs satisfies $0$ ≤ total cost.
background
The module decomposes the Standard Model Lagrangian into four canonical sectors named by the inductive type SMLagrangianSector. Each sector is equipped with a J-cost functional on its deviation ratio from the recognition vacuum; totalCost is defined as the direct sum of the four sector costs with no cross-sector mixing at tree level. The upstream sectorCost_nonneg theorem states that sectorCost r ≥ 0 whenever r > 0, and itself reduces to Jcost_nonneg from the Cost module.
proof idea
The term proof first unfolds totalCost to the explicit sum of four sectorCost applications. It then obtains four separate inequalities by applying sectorCost_nonneg to each component, using the hypothesis that r(s) > 0 for every sector s. The final linarith tactic combines those four inequalities into the required nonnegativity of the sum.
why it matters
The theorem supplies the total_nonneg field inside smLagrangianCert, the certificate that collects vacuum-zero, reciprocal symmetry, and nonnegativity properties for the SM skeleton. It thereby closes one structural requirement in the Recognition Science derivation of the Standard Model Lagrangian, ensuring the cost functional is bounded below in agreement with the J-cost framework and the vacuum condition stated in the module doc.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.