AdmissibleRealization
plain-language theorem explainer
AdmissibleRealization packages the extra structural conditions that turn a StrictLogicRealization into an admissible one for universal forcing. Domain modelers in Recognition Science cite it when they verify that concrete realizations (music, biology, narrative, ethics) carry decidable costs, associative composition, and a unit identity. The declaration is a bare structure whose three fields directly record the required witnesses.
Claim. A strict logic realization $R$ is admissible when cost equality is decidable ($R$.compare$(x,y)=0$ is decidable for all carriers), composition is associative ($R$.compose$(R$.compose$(a,b),c)=R$.compose$(a,R$.compose$(b,c))$), and the unit satisfies $R$.compose$(R$.one$,$R$.one$)=R$.one$ or $R$.compose$(R$.one$,$R$.generator$)=R$.generator$.
background
A StrictLogicRealization supplies a carrier with compare, compose, one and generator together with the raw propositions excluded_middle_law, composition_law and invariance_law. The upstream Composition class from CostAxioms encodes the Recognition Composition Law: for positive $x,y$, $F(xy)+F(x/y)=2F(x)F(y)+2F(x)+2F(y)$, the multiplicative form of d'Alembert's equation that forces compatibility with the multiplicative structure of the positive reals. The module doc states that the five domain realizations instantiate the basic laws as True while RichDomainCosts supplies the concrete associativity and decidability facts for each domain.
proof idea
The declaration is a structure definition with no proof body. Its three fields are the direct witnesses: a Decidable instance for cost equality, an equality proof of associativity, and a disjunction witnessing the unit-or-generator identity.
why it matters
AdmissibleRealization supplies the typeclass used by quantified_universal_forcing and AdmissibleClassCert, which together assert that any two admissible realizations induce canonically equivalent forced arithmetic surfaces. It therefore lifts the strict universal-forcing equivalence from arbitrary StrictLogicRealization instances to the admissible subclass, closing the step from the basic forcing chain (T0-T8) and the Recognition Composition Law to domain-specific applications.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.