pith. sign in
module module moderate

IndisputableMonolith.Physics.YangMillsLatticeFromRS

show as:
view Lean formalization →

This module constructs the Yang-Mills sector on a lattice from Recognition Science by importing the J-cost framework. It defines the vacuum state as J=0, which corresponds to the ground state carrying a mass gap. Lattice gauge theorists would cite the definitions to embed Yang-Mills dynamics inside the RS forcing chain. The module supplies a collection of definitions and basic certificates with no internal proofs.

claimThe Yang-Mills sector is equipped with vacuum state satisfying $J=0$, yielding the lattice mass gap ground state; auxiliary objects include sector count, vacuum uniqueness, and gap certificates.

background

Recognition Science derives all physics from the single J-cost functional obeying the composition law $J(xy)+J(x/y)=2J(x)J(y)+2J(x)+2J(y)$. The imported Cost module supplies this functional together with the phi-ladder and defect distance. This module applies those primitives to lattice gauge theory, introducing YMSector, ymSectorCount, ym_vacuum, ym_lattice_gap, and the certificate YMLatticeGapCert.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module supplies the lattice Yang-Mills construction that supports later derivations of gauge-theory mass gaps inside Recognition Science. It directly instantiates the J-uniqueness step (T5) and the three-dimensional spatial setting (T8) from the unified forcing chain. No downstream theorems are recorded yet.

scope and limits

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (7)