Foundation Qrft Smlagrangian Skeleton Total Cost Nonneg

The nonnegativity bound

The Standard Model Lagrangian is the equation that summarizes how the known elementary particles interact. In the Recognition Science framework, its four canonical sectors, gauge kinetic, fermion kinetic, Yukawa, and Higgs potential, each carry a per-sector cost. The declaration totalCost_nonneg proves that the sum of these four sector costs is always greater than or equal to zero, provided every sector's deviation ratio is positive. The proof is machine-checked in the framework's library of formal theorems, with no unproven assumptions.

The cost function itself is the framework's central object: a measure of how far a system sits from its recognition vacuum. At unity, where a sector exactly matches its vacuum value, the cost is zero. The nonnegativity theorem extends this to the whole skeleton: no combination of positive sector ratios can drive the total cost below zero. Each sector's cost is nonnegative on its own, and the total is simply their sum, so the bound follows by adding four nonnegative numbers.

What the theorem does not claim is as important as what it proves. It says nothing about the actual values of the Standard Model's parameters, such as particle masses or coupling strengths. It does not assert that the skeleton reproduces any measured quantity. It only establishes a structural property: the total cost, as defined on this four-sector skeleton, cannot be negative. The physical content of the sectors, and any empirical comparison, lies outside this declaration.

In Recognition Science, this nonnegativity is a sanity condition on the skeleton. A cost that could go negative would signal an instability or an error in the framework's construction. The theorem certifies that the skeleton is well-formed in this one respect: its total cost has a floor at zero, reached exactly when every sector sits at its vacuum value.

/-- Total cost is nonnegative when every sector is in the physical
domain `r > 0`. -/
theorem totalCost_nonneg (r : SMLagrangianSector → ℝ)
    (h : ∀ s, 0 < r s) : 0 ≤ totalCost r := by
  unfold totalCost
  have h1 := sectorCost_nonneg (h .gaugeKinetic)
  have h2 := sectorCost_nonneg (h .fermionKinetic)
  have h3 := sectorCost_nonneg (h .yukawa)
  have h4 := sectorCost_nonneg (h .higgsPotential)
  linarith

theorem sectorCost_zero_at_vacuum : sectorCost 1 = 0 := Cost.Jcost_unit0

theorem sectorCost_nonneg {r : ℝ} (hr : 0 < r) : 0 ≤ sectorCost r :=
  Cost.Jcost_nonneg hr

What this page does not claim

The theorem does not determine any Standard Model parameter values. It does not assert that the skeleton reproduces any measured physical quantity. It says nothing about the physical interpretation of the deviation ratios beyond their positivity.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Foundation/QRFT/SMLagrangianSkeleton.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: