admissibleClassCert_holds
plain-language theorem explainer
This definition assembles the four domain-specific admissibility witnesses and the quantified universal forcing theorem into the AdmissibleClassCert record. A researcher checking that the canonical strict realizations in Recognition Science carry no extra admissibility obstructions would cite this certificate. The construction is a direct record literal that substitutes the music, biology, narrative, ethics admissibility lemmas together with the trivial quantified theorem.
Claim. Let $M$, $B$, $N$, $E$ be the strict realizations for music, biology, narrative and ethics. The definition supplies an $AdmissibleClassCert$ record whose fields are $AdmissibleRealization(M)$, $AdmissibleRealization(B)$, $AdmissibleRealization(N)$, $AdmissibleRealization(E)$, and the proposition that any two admissible strict realizations $R,S$ satisfy the universal forcing equivalence.
background
AdmissibleRealization is the typeclass on StrictLogicRealization that requires a decidable cost predicate (via excluded middle), an associative composition law, and a nontrivial invariance witness under bijective relabeling. The module documentation states that StrictLogicRealization carries excluded_middle_law, composition_law and invariance_law as raw Props, while the admissible instances for the four domains instantiate them with concrete witnesses drawn from RichDomainCosts. The quantified_universal_forcing theorem then records that any two such admissible realizations have canonically equivalent forced arithmetic surfaces, with the equivalence supplied by StrictLogicRealization.universal_forcing.
proof idea
This is a definition that directly constructs the AdmissibleClassCert structure by substituting the four domain admissibility definitions (music_admissible, biology_admissible, narrative_admissible, ethics_admissible) and the quantified_universal_forcing theorem into the corresponding fields of the record.
why it matters
The definition supplies the concrete AdmissibleClassCert that certifies the four canonical domains satisfy the admissibility conditions, thereby enabling the quantified universal forcing theorem to apply without obstruction. It records that admissibility imposes no additional constraint on the strict realizations already present in the Recognition Science framework. The parent result is the quantified_universal_forcing theorem, which asserts equivalence of forced arithmetic surfaces for any admissible pair.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.