Pith. sign in
module module high

IndisputableMonolith.ILG.CPMInstance

show as:
view Lean formalization →

ILG.CPMInstance abstracts the gravitational field configuration from the ILG kernel into quantities required for Coercive Projection Method coercivity bounds. It supplies the state and auxiliary functions that connect the kernel weight to defect and energy controls. Researchers applying CPM to ILG models in Recognition Science reference this module to instantiate the generic Law of Existence. The module consists of definitions and supporting constants with no central theorem.

claimThe ILG configuration state at wave number $k$ and scale $a$ supplies the inputs to the projection-defect inequality, using kernel weight $w(k,a)=1+C(a/(k au_0))^eta$ where $ au_0=1$ tick.

background

The module sits inside the ILG domain and imports the generic CPM structure (projection-defect inequality, coercivity factorization, aggregation principle) together with the ILG kernel and the base time quantum. ILGState captures the gravitational field configuration at a given scale, reduced to the minimal data needed for coercivity bounds. The kernel supplies the weight function that enters the defect and energy calculations.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module supplies the concrete state that lets the generic Law of Existence apply to the ILG kernel. It therefore supports coercivity arguments inside ILG models and connects the kernel definition to the CPM aggregation principle.

scope and limits

depends on (3)

Lean names referenced from this declaration's body.

declarations in this module (17)