four_canonical_domains_admissible
plain-language theorem explainer
Admissibility witnesses exist for the strict realizations of music, biology, narrative, and ethics. Researchers quantifying the universal forcing theorem over admissible classes cite this to confirm the four canonical domains meet the required structural laws. The proof is a direct term that assembles the four domain-specific admissibility definitions into a conjunction of nonemptiness statements.
Claim. There exist admissible realizations for the strict music, biology, narrative, and ethics realizations, where admissibility requires decidable cost equality on the carrier, associative composition, and a one-identity or generator-step condition.
background
The module defines AdmissibleRealization as a structure over StrictLogicRealization that adds three properties beyond basic identity and non-contradiction: cost equality is decidable, composition is associative, and the chosen one acts as a left identity or generator step. StrictLogicRealization itself carries excluded_middle_law, composition_law, and invariance_law instantiated as True for the five domain realizations. The upstream universal_forcing meta-theorem states that any two LogicRealization instances have canonically equivalent forced arithmetic objects via ArithmeticOf.equivOfInitial.
proof idea
The proof is a term-mode construction that directly packages the four sibling definitions music_admissible, biology_admissible, narrative_admissible, and ethics_admissible as witnesses for the respective Nonempty types.
why it matters
This supplies the admissibility witnesses required by the quantified universal forcing theorem in the same module, confirming that the four canonical domains satisfy the non-trivial structural laws. It allows the universal forcing equivalence to apply without admissibility as an obstruction, directly supporting the framework's claim that any two admissible strict realizations have equivalent forced arithmetic surfaces.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.