pith. machine review for the scientific record. sign in
module module high

IndisputableMonolith.YM.OS

show as:
view Lean formalization →

YM.OS supplies the abstract interface for lattice measures in the Yang-Mills sector. It introduces LatticeMeasure, Kernel, TransferOperator, and OSPositivity as the discrete starting point for positivity and gap analysis. Researchers in constructive QFT cite it when moving from lattice regularization to continuum limits. The module is purely definitional with no theorems or proofs.

claimThe module defines an abstract lattice measure $mu$ on a finite lattice $Lambda$, together with kernel $K$ and transfer operator $T$ satisfying the Osterwalder-Schrader positivity condition.

background

Recognition Science treats Yang-Mills via lattice regularization before the continuum limit. This module supplies the interface-level definitions for the lattice measure, kernel, and transfer operator. These objects support the OS positivity axiom needed to build a positive inner product on the state space. The module imports only Mathlib and lists sibling declarations that implement or apply these structures.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module supplies the lattice measure interface required by the mass gap results in MassGap, MassGapCont, mass_gap_of_OS_PF, and mass_gap_continuum. It fills the interface step in the YM construction, preceding application of the Recognition Composition Law and extraction of the mass gap from the phi-ladder.

scope and limits

declarations in this module (12)