pith. sign in
module module high

IndisputableMonolith.Foundation.UniversalForcing.Strict.Metaphysical

show as:
view Lean formalization →

This module supplies the strict metaphysical ground, a theology-neutral structural package assigning forced arithmetic to every strict realization while proving invariance across them. It completes the five-domain set (Music, Biology, Narrative, Ethics, Metaphysical) for domain-rich strict logic realizations. Researchers auditing the universal forcing completion would cite it when assembling the full StrictLogicRealization instances. The module is purely definitional, importing the Ethics realization and exporting the metaphysical instance.

claimA strict metaphysical ground is a structural package $G$ such that for every strict realization $R$, $G(R)$ assigns the forced arithmetic and the composition, excluded-middle, and invariance laws hold uniformly across all strict realizations.

background

The module sits inside the strict universal forcing layer of the Foundation, importing the Ethics module that defines domain-rich ethical realization over action states equipped with agent and improvement-rank coordinates, generated by the smallest recognized improvement step. It introduces StrictMetaphysicalGround as the package that equips every strict realization with its forced arithmetic while remaining theology-neutral, naming only the mathematical role of a ground of distinguishability. This continues the pattern established by the sibling domain modules that each supply a StrictLogicRealization instance with the three law placeholders.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module feeds the AxiomAudit surface for the strict domain-rich Universal Forcing completion pass and supplies the metaphysical instance to RichDomainCosts, which converts the five domain placeholders into the actual composition, excluded-middle (decidability), and invariance laws. It thereby closes the metaphysical slot required for the full strict logic realization package in the universal forcing chain.

scope and limits

used by (2)

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 (3)