AdmissibleRealization
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.
claimA 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 in Recognition Science
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.
scope and limits
- Does not prove admissibility for any concrete domain realization.
- Does not derive the universal forcing equivalence itself.
- Does not apply to non-strict realizations.
- Does not encode the full invariance_law beyond the unit condition.
formal statement (Lean)
42structure AdmissibleRealization (R : StrictLogicRealization) where
43 /-- Cost equality is decidable (excluded middle on the cost predicate). -/
44 cost_decidable : ∀ x y : R.Carrier, Decidable (R.compare x y = 0)
45 /-- Composition is associative. -/
46 compose_assoc : ∀ a b c : R.Carrier,
47 R.compose (R.compose a b) c = R.compose a (R.compose b c)
48 /-- The chosen `one` is a left identity (or analog). -/
49 compose_one_or_step : R.compose R.one R.one = R.one ∨
50 R.compose R.one R.generator = R.generator
51
52/-! ## Admissibility for the existing five domain realizations -/
53