pith. sign in
module module moderate

IndisputableMonolith.Foundation.QRFT.SMLagrangianSkeleton

show as:
view Lean formalization →

This module introduces the four canonical sectors of the Standard Model Lagrangian and associated cost functions in the Recognition Science setting. A researcher constructing the QRFT Lagrangian or verifying vacuum properties would cite these definitions when assembling total cost from sector contributions. The module consists entirely of definitions and property statements with no proofs.

claimLet the four canonical sectors of the SM Lagrangian be denoted $S_1, S_2, S_3, S_4$. Define a cost map $c$ on each sector such that $c(s)=0$ at the vacuum configuration, $c(s) eq 0$ off vacuum, $c(s) o c(s^{-1})$ under reciprocal symmetry, and the total cost is the sum over sectors. The certification object asserts that the resulting Lagrangian satisfies the required non-negativity and vacuum-zero conditions.

background

The module imports the RS time quantum $ au_0=1$ tick from Constants and the general cost machinery from the Cost module. It works inside the QRFT sector of the Foundation layer, where the Standard Model Lagrangian is decomposed into four canonical sectors whose individual costs must obey the Recognition Composition Law and the J-cost functional.

Sector cost is required to vanish exactly at the vacuum, remain non-negative everywhere, and exhibit reciprocal symmetry. The total cost is the direct sum of the four sector costs. These properties are stated as named declarations that later modules can invoke when building the full Lagrangian or its certification.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module supplies the sector decomposition and cost skeleton that higher-level QRFT constructions rely on when assembling the complete SM Lagrangian and its certification object. It directly supports the transition from the abstract cost axioms to concrete particle-sector assignments inside the Recognition Science framework.

scope and limits

depends on (2)

Lean names referenced from this declaration's body.

declarations in this module (12)