pith. sign in
module module high

IndisputableMonolith.ILG.ParamsKernel

show as:
view Lean formalization →

The ParamsKernel module supplies the verification predicate that the ILG parameter kernel consists of well-formed parameters. Researchers building the Indisputable Logic Graph cite it when importing the minimal parameter record for modules outside the Relativity subtree. The module is a thin wrapper around the imported Params record that adds only the well-formedness check.

claimLet $p$ be a parameter record. The predicate $ParamsKernelVerified(p)$ holds precisely when $p$ is well-formed.

background

The module sits in the ILG domain and imports the minimal parameter record defined in IndisputableMonolith.ILG.Params. That record is the minimal parameter record used by downstream ILG modules outside the sealed Relativity subtree. The present module adds only the verification predicate stating that parameters must be well-formed.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module supplies the verified parameter kernel to IndisputableMonolith.ILG.NOfRMono. It therefore serves as the entry point that guarantees well-formed parameters before any further ILG constructions are attempted.

scope and limits

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (2)