Foundation Qrft Smlagrangian Skeleton Sector Count

The four sectors

The Standard Model Lagrangian, the compact expression from which particle physicists derive the behavior of known matter, separates into four traditional parts: the kinetic energy of the force carriers, the kinetic energy of the matter particles, the Yukawa couplings that give particles mass, and the Higgs potential that drives symmetry breaking. In the Recognition Science framework, a machine-checked library of formal theorems names these four as canonical structures and proves, by direct computation, that there are exactly four. The declaration sector_count states this as a theorem: the cardinality of the set of sectors equals 4.

The framework models each sector's deviation from a preferred state using a single cost function, the recognition cost, which measures how far a ratio has moved from unity. For each sector, this cost is zero when the sector sits exactly at the recognition vacuum, the state of no deviation. The cost is nonnegative for all physical values, and it is positive whenever the sector is away from the vacuum. These properties are proved for each sector individually and then summed: the total Lagrangian cost is the sum of the four sector costs, with no cross-sector mixing at tree level on the canonical sector.

The theorem that there are four sectors is a structural statement about the skeleton, not a derivation of the full Standard Model. The module names the four sectors and proves their mutual additivity, but it does not construct the actual gauge kinetic, fermion kinetic, Yukawa, or Higgs terms with their physical coefficients. The full closure of the program is described as multi-month work. The sector count is a counted fact about the named decomposition, a certificate that the skeleton has the right shape, not a complete Lagrangian.

What the theorem does not claim is equally precise. It does not claim that the four sectors are the only possible decomposition of the Lagrangian. It does not claim that the cost function for each sector is derived from the Standard Model's actual couplings. It does not claim that the recognition vacuum corresponds to the physical vacuum of the Standard Model. The sector count is a structural opening, a named skeleton with the right shape for future work, not a finished physical theory.

/-- Sector count = 4 (matches the canonical SM Lagrangian decomposition). -/
theorem sector_count : Fintype.card SMLagrangianSector = 4 := by decide

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

theorem sectorCost_pos_off_vacuum {r : ℝ} (hr : 0 < r) (hne : r ≠ 1) :
    0 < sectorCost r := Cost.Jcost_pos_of_ne_one r hr hne

/-- Total Lagrangian cost is the sum of per-sector costs (no
cross-sector mixing at tree level on the canonical sector). -/
def totalCost (r : SMLagrangianSector → ℝ) : ℝ :=
  sectorCost (r .gaugeKinetic) + sectorCost (r .fermionKinetic) +
    sectorCost (r .yukawa) + sectorCost (r .higgsPotential)

What this page does not claim

The four sectors are not proved to be the only possible decomposition of the Lagrangian. The cost function for each sector is not derived from the Standard Model's actual couplings. The recognition vacuum is not claimed to be the physical vacuum of the Standard Model.

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: