totalCost
plain-language theorem explainer
The total Lagrangian cost sums the J-costs of the four canonical SM sectors on their deviation ratios. Particle physicists and cosmologists working in Recognition Science cite this when assembling the full cost functional for vacuum balance or ledger checks. It is a direct one-line definition that adds the four independent sectorCost terms with no cross-sector mixing.
Claim. The total cost functional is $C(r) = C_g(r_g) + C_f(r_f) + C_y(r_y) + C_h(r_h)$, where $r$ assigns a positive deviation ratio to each of the four sectors (gauge kinetic, fermion kinetic, Yukawa, Higgs potential) and each $C_s$ denotes the J-cost on that sector's ratio.
background
The module decomposes the Standard Model Lagrangian into four canonical sectors on the Recognition Manifold: gauge kinetic, fermion kinetic, Yukawa, and Higgs potential. Each sector is equipped with a J-cost-on-deviation form, where sectorCost(r) := Jcost(r) for deviation ratio r > 0. This rests on upstream definitions such as the cost induced by a multiplicative recognizer (derivedCost on its comparator) and the Higgs potential defined directly as J-cost on the field ratio.
proof idea
One-line wrapper that applies sectorCost to each of the four sectors extracted from the input map r (gaugeKinetic, fermionKinetic, yukawa, higgsPotential) and returns their sum.
why it matters
This supplies the additive total cost that appears in SMLagrangianCert (total_vacuum_zero and total_nonneg) and in totalCost_nonneg. It is also referenced by LambdaRecDerivation.totalCost and by Cosmology.DarkEnergy.costDensity and isBalanced for ledger balance. In the Recognition framework it realizes the tree-level decomposition of the SM Lagrangian cost with no cross-sector mixing, consistent with the J-cost structure and the four-sector skeleton needed for the Wightman/OS bridge.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.