module module high

`IndisputableMonolith.Foundation.QRFT.SMLagrangianSkeleton`

This module introduces the four canonical sectors of the Standard Model Lagrangian expressed in Recognition Science terms. It supplies sector and total cost functions that vanish at vacuum and remain nonnegative off vacuum. QRFT model builders cite these definitions when assembling the effective action from J-cost principles. The module is purely definitional.

claimThe module declares the four sectors of the Standard Model Lagrangian together with associated cost functions that equal zero at the vacuum state and are nonnegative elsewhere.

background

The module sits in the Foundation.QRFT domain and imports the RS time quantum τ₀ = 1 tick from Constants together with the J-cost machinery from Cost. It introduces SMLagrangianSector as the type enumerating the four canonical sectors and defines sectorCost and totalCost that measure deviation from vacuum. The local setting is a skeleton for the SM Lagrangian prior to full certification via the recognition composition law.

proof idea

this is a definition module, no proofs

why it matters in Recognition Science

This module supplies the Lagrangian-sector definitions that feed into QRFT constructions of the full effective action. It underpins later certification steps such as SMLagrangianCert by establishing the cost structure for each sector. No downstream theorems are recorded yet.

scope and limits

Does not derive explicit Lagrangian densities for any sector.
Does not link costs to the phi-ladder mass formula.
Does not apply the recognition composition law to these sectors.
Does not address the alpha band or spatial dimension D = 3.

depends on (2)

Lean names referenced from this declaration's body.

IndisputableMonolith.Constants module_import
IndisputableMonolith.Cost module_import

declarations in this module (12)

inductive SMLagrangianSector L36
def sectorCost L44
theorem sectorCost_zero_at_vacuum L46
theorem sectorCost_reciprocal_symm L48
theorem sectorCost_nonneg L51
theorem sectorCost_pos_off_vacuum L54
def totalCost L59
theorem totalCost_zero_at_vacuum L64
theorem totalCost_nonneg L71
theorem sector_count L81
structure SMLagrangianCert L83
def smLagrangianCert L93