pith. machine review for the scientific record. sign in
module module high

IndisputableMonolith.Foundation.UniversalForcing.AdmissibleClass

show as:
view Lean formalization →

The AdmissibleClass module defines admissible strict realizations as those obeying non-trivial structural laws such as composition and invariance in addition to basic identity and non-contradiction. Researchers extending domain-specific models in Recognition Science cite it when classifying realizations for music, biology, narrative, and ethics. The module structures its content through imports of the strict realization interface and rich domain cost theorems to ground the admissible predicate.

claimA strict realization $R$ is admissible when it satisfies the excluded-middle law, composition law $J(xy)+J(x/y)=2J(x)J(y)+2J(x)+2J(y)$, and invariance law in addition to the basic identity and non-contradiction properties.

background

This module operates in the setting of domain-rich universal forcing. The upstream StrictRealization interface supplies native comparison and ordering without internal-orbit escape hatches, strengthening the earlier lightweight LogicRealization theorem. The RichDomainCosts module proves the concrete composition, excluded-middle decidability, and invariance laws for the five domains (Music, Biology, Narrative, Ethics, Metaphysical) by replacing placeholder fields with actual theorems.

proof idea

This is a definition module, no proofs. It declares the AdmissibleRealization predicate and constructs concrete instances (music_admissible, biology_admissible, narrative_admissible, ethics_admissible) by direct application of the cost theorems imported from RichDomainCosts.

why it matters in Recognition Science

The module supplies the admissible realizations required by quantified_universal_forcing and the four_canonical_domains_admissible construction. It completes the step in the universal forcing chain where domain models must carry the full set of structural laws to participate in the forcing theorem. It touches the open question of extending admissibility beyond the canonical four domains.

scope and limits

depends on (2)

Lean names referenced from this declaration's body.

declarations in this module (9)