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

IndisputableMonolith.ILG.CPMInstance

show as:
view Lean formalization →

ILG.CPMInstance supplies the configuration state for Infra-Luminous Gravity inside the Coercive Projection Method. It abstracts the gravitational field at a given scale to the minimal quantities required for coercivity bounds. Researchers formalizing gravity models in Recognition Science cite this module to connect the ILG kernel with CPM's projection-defect and energy-gap controls. The module consists entirely of definitions for ILGState and supporting terms such as defectMass and energyGap.

claimThe ILG configuration state abstracts the gravitational field configuration at a given scale to the essential quantities needed for coercivity bounds in the Coercive Projection Method.

background

This module sits at the intersection of the ILG kernel and the generic CPM Law of Existence. The kernel defines the weight function $w(k,a)=1+C(a/(kτ_0))^α$ with $τ_0$ the fundamental RS time quantum. CPM supplies the three-part structure: projection-defect inequality, coercivity factorization controlled by the energy gap, and the aggregation principle that local tests imply global membership. The module abstracts the ILG field configuration into ILGState together with auxiliary quantities (defectMass, orthoMass, energyGap) that make the CPM coercivity bounds directly applicable.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module supplies the ILG-specific state abstraction required to instantiate the Law of Existence for gravitational configurations. It thereby feeds the construction of ilgModel and the coercivity results that appear in the sibling declarations. Within the Recognition framework it links the ILG kernel directly to the generic CPM structure, supporting the application of the forcing chain and the eight-tick octave to gravitational bounds.

scope and limits

depends on (3)

Lean names referenced from this declaration's body.

declarations in this module (17)