pith. sign in
module module high

IndisputableMonolith.Foundation.UniversalForcing.AdmissibleClass

show as:
view Lean formalization →

The AdmissibleClass module defines when a strict realization counts as admissible by adding non-trivial structural laws to the basic identity and non-contradiction conditions. It assembles the StrictRealization interface with the domain cost theorems to enforce composition, excluded-middle, and invariance. Recognition Science researchers extending the forcing chain to rich domains cite this module when constructing admissible classes for the canonical domains. The module is organized as a set of definitions with no internal proofs.

claimA strict realization $R$ is admissible when the composition law, excluded-middle law, and invariance law hold in addition to the identity and non-contradiction conditions supplied by the strict interface.

background

The module belongs to the Universal Forcing section of the Recognition Science foundation. It upgrades the earlier lightweight LogicRealization by adopting the strict interface that removes any internal orbit field and forces native comparison only. StrictRealization supplies the domain-rich interface while RichDomainCosts replaces the placeholder True values with actual proofs of the composition law, excluded-middle (decidability), and invariance law for the five domains Music, Biology, Narrative, Ethics, and Metaphysical.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

This module feeds the sibling declarations AdmissibleRealization, music_admissible, biology_admissible, narrative_admissible, ethics_admissible, four_canonical_domains_admissible, and quantified_universal_forcing. It supplies the admissible-class layer that converts strict realizations into objects satisfying the structural laws required by the forcing chain.

scope and limits

depends on (2)

Lean names referenced from this declaration's body.

declarations in this module (9)