pith. sign in
module module high

IndisputableMonolith.ILG.Params

show as:
view Lean formalization →

ILG.Params supplies a minimal parameter record for downstream ILG modules that operate outside the sealed Relativity subtree. Kernel verification modules cite this record when checking well-formedness. The module contains only definitions and no proofs.

claimThe minimal parameter record $Params$ for ILG modules outside the Relativity subtree.

background

ILG.Params sits in the ILG domain of Recognition Science and introduces a minimal parameter record. The record supplies the data needed by modules that avoid the sealed Relativity subtree. It relies on the upstream Recognition Composition Law and phi-ladder conventions.

proof idea

this is a definition module, no proofs

why it matters in Recognition Science

The module feeds the ParamsKernel verification predicate that requires parameters to be well-formed. It supplies the parameter definition step required by the ILG chain.

scope and limits

used by (1)

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

declarations in this module (2)