AdmissibleRealization
plain-language theorem explainer
AdmissibleRealization packages the three structural conditions (decidable cost comparison, associative composition, and one-or-generator invariance) that elevate a StrictLogicRealization to participate in quantified universal forcing. Domain modelers cite it when certifying music, biology, narrative, and ethics realizations for equivalence of forced arithmetic surfaces. The declaration is a bare structure definition with no proof body or computational content.
Claim. A strict realization $R$ is admissible when its cost comparison is decidable on the carrier, its composition operation is associative, and either $R$.compose $R$.one $R$.one equals $R$.one or $R$.compose $R$.one $R$.generator equals $R$.generator.
background
StrictLogicRealization carries raw Prop fields for excluded middle, composition, and invariance; the five domain realizations instantiate them trivially. AdmissibleRealization adds the non-trivial witnesses: decidability of compare, associativity of compose, and the one-step invariance condition. Upstream CostAxioms.Composition encodes the Recognition Composition Law (RCL): for positive $x,y$, $F(xy)+F(x/y)=2F(x)F(y)+2F(x)+2F(y)$. RichDomainCosts supplies the concrete associativity instances used by the domain admissibility definitions.
proof idea
Structure definition that directly records three field propositions. No lemmas or tactics are invoked; the declaration itself supplies the interface consumed by quantified_universal_forcing and the four domain admissibility witnesses.
why it matters
AdmissibleRealization is the prerequisite type for quantified_universal_forcing, which asserts that any two admissible realizations share the same forced arithmetic surface via StrictLogicRealization.universal_forcing. It feeds AdmissibleClassCert and the four domain admissibility definitions. In the Recognition framework it ensures the structural laws required for the universal forcing step across domains (T0-T8 chain) without obstructing the equivalence.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.