Foundation Qrft Smlagrangian Skeleton

The Standard Model skeleton

The Standard Model of particle physics is usually written as one long Lagrangian, a single formula that encodes the known particles and forces. That formula naturally splits into four parts: the kinetic energy of the force-carrying gauge bosons, the kinetic energy of the matter fermions, the Yukawa couplings that give fermions mass, and the Higgs potential that gives the Higgs field its shape. Physicists have used this four-way decomposition for decades; it is the canonical anatomy of the model.

In Recognition Science, the framework models each of these four sectors with the same cost function. The cost of a deviation from a preferred value is J(x) = (x + 1/x)/2 - 1, a function that is zero when x equals 1, positive otherwise, and symmetric under x going to 1/x. The framework's machine-checked library of formal theorems, a collection of proofs verified by computer, applies this cost to each sector's canonical deviation ratio. The module defines the four sectors as an enumerated type, assigns each one the same J-cost, and proves the basic properties: the cost vanishes at unity, it is symmetric under reciprocals, and it is never negative for positive inputs.

The key structural claim is additivity. The total Lagrangian cost is defined as the plain sum of the four sector costs, with no cross terms. The library proves that this total cost is zero exactly when every sector sits at its preferred value, and that it is nonnegative whenever all sectors are in the physical domain of positive ratios. This is a statement about the skeleton, not the full theory: it says the four sectors do not mix at tree level in this canonical form, a property that matches the standard model's structure.

In Recognition Science, this skeleton is a labeled step, not a finished theory. The framework models the Standard Model's four sectors as a unified cost structure, and its library proves the additivity and positivity properties that any full treatment must respect. The module explicitly notes that full closure of the program is months away; this is the structural opening that ties together existing work on gauge bosons, Yukawa couplings, and the Higgs potential into one named skeleton, shaped for a future bridge to Wightman axioms and Osterwalder-Schrader reconstruction. What the reader can now see is a precise, machine-checked claim: the Standard Model's four sectors, in this framework, form a mutually additive cost system with a unique zero at the recognition vacuum.

/-- Per-sector J-cost on the sector's canonical-deviation ratio. -/
def sectorCost (r : ℝ) : ℝ := Cost.Jcost r

/-- 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)

/-- Total cost vanishes when every sector sits at unity. -/
theorem totalCost_zero_at_vacuum :
    totalCost (fun _ => 1) = 0 := by
  unfold totalCost
  simp [sectorCost_zero_at_vacuum]

/-- 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_reciprocal_symm {r : ℝ} (hr : 0 < r) :
    sectorCost r = sectorCost r⁻¹ := Cost.Jcost_symm hr

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

What this page does not claim

This module does not derive the full Standard Model Lagrangian from the cost function. It does not prove that the four sectors are the only possible decomposition. It does not establish the Wightman or Osterwalder-Schrader bridge, which remains open.

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: