AdmissibleClassCert
plain-language theorem explainer
AdmissibleClassCert records four domain admissibility witnesses together with the claim that any two admissible strict realizations share the universal forcing equivalence. Researchers extending forcing across domains cite the certificate to confirm admissibility imposes no extra obstruction. The definition is a direct record of the four AdmissibleRealization instances plus the trivial quantified statement.
Claim. An admissible class certificate consists of witnesses that the music, biology, narrative, and ethics realizations are admissible, together with the assertion that for all admissible strict realizations $R$ and $S$ the strict universal forcing equivalence holds.
background
A StrictLogicRealization comprises a carrier type, cost type with zero instance, compare map, and compose operation. AdmissibleRealization R adds three conditions: cost equality is decidable, compose is associative, and the one element satisfies a left-identity or generator step condition. The module supplies four concrete realizations (music via frequency ratios and octave stacking, biology via lineage states and reproduction, narrative via event states and succession, ethics via action states and preference composition) and elevates them to the admissible class.
proof idea
Direct record construction that assembles the four domain admissibility instances and the quantified universal forcing statement. The quantified statement itself is discharged by a one-line wrapper applying trivial after two introductions.
why it matters
The structure supplies the master certificate consumed by admissibleClassCert_holds. It records that admissibility is not an obstruction to the quantified universal forcing theorem, which states that any two admissible realizations have canonically equivalent forced arithmetic surfaces. This closes the step from domain-specific realizations to the general claim that the forcing equivalence is available once the three structural laws hold.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.