pith. sign in
module module high

IndisputableMonolith.ILG.CPMInstance

show as:
view Lean formalization →

ILG configuration state abstracts the gravitational field configuration at a given scale to the quantities required for coercivity bounds. The module supplies the state and related definitions that connect the ILG kernel to the generic Coercive Projection Method. It draws on the upstream Law of Existence for the A/B/C structure and on the kernel weight function. Researchers applying CPM to gravity models cite this module. This is a definition module with no proofs.

claimThe ILG configuration state is an abstraction of the gravitational field configuration at a given scale, reduced to the essential quantities needed to apply coercivity bounds from the Coercive Projection Method.

background

This module operates in the Infra-Luminous Gravity domain. It imports the generic CPM Law of Existence module, which supplies the Projection-Defect inequality, the Coercivity factorization (energy gap controls defect), and the Aggregation principle. It also imports the ILG Kernel, which defines the weight function $w(k, a) = 1 + C \cdot (a / (k au_0))^eta$ where $ au_0$ is the fundamental RS time quantum equal to one tick, and the Constants module.

The module DOC_COMMENT states that the ILG configuration state captures the gravitational field configuration at a given scale and, for the CPM formalization, abstracts this to essential quantities needed for the coercivity bounds. Sibling definitions in the module (ILGState, defectMass, orthoMass, energyGap) implement this abstraction.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

This module supplies the ILG-specific instance that allows the generic Law of Existence (CPM core) to apply to infra-luminous gravity. It feeds the coercivity factorization and aggregation steps by providing the concrete state and gap quantities for the ILG kernel. The module thereby links the kernel formalization to the broader Recognition Science structure that includes the forcing chain and native constants.

scope and limits

depends on (3)

Lean names referenced from this declaration's body.

declarations in this module (17)