ethics_admissible
plain-language theorem explainer
The ethics_admissible definition supplies a witness that the Ethics realization meets the three structural requirements of AdmissibleRealization: decidable zero-cost equality, associative composition, and a fixed-point identity on the ethical zero. Researchers working on quantified universal forcing would cite this witness to confirm that the Ethics domain joins the other three canonical realizations in satisfying the conditions for equivalence of forced arithmetic surfaces. The construction is a direct refinement that assembles the three Admis
Claim. The Ethics realization is admissible: for all carriers $a,b$ the predicate that the action cost equals zero is decidable; the preference composition operation is associative; and the composition of the ethical zero element with itself equals the ethical zero element.
background
The module defines AdmissibleRealization as a structure over any StrictLogicRealization that adds three concrete properties: decidability of cost equality to zero (supplying excluded middle), associativity of the composition law, and a nontrivial invariance condition expressed as an or-statement on the unit element. The local theoretical setting is that StrictLogicRealization already carries the basic excluded-middle, composition, and invariance laws instantiated as True, while RichDomainCosts supplies the actual law-bearing instances for each domain. This definition provides the Ethics witness among the four canonical domains whose admissibility is collected for the quantified forcing theorem.
proof idea
The definition refines the three fields of the AdmissibleRealization structure. Decidability of zero cost is obtained by applying decEq to the Ethics actionCost predicate. Associativity is taken directly from the lemma RichDomainCosts.EthicsRich.preferenceCompose_assoc. The invariance condition is discharged by reflexivity on the equality of the ethical zero composed with itself.
why it matters
This witness is collected in admissibleClassCert_holds together with the three other domain witnesses and is used by the theorem four_canonical_domains_admissible to assert that all four canonical realizations are admissible. It thereby supports the headline claim that any two admissible realizations have canonically equivalent forced arithmetic surfaces via the universally available StrictLogicRealization.universal_forcing. In the Recognition Science framework the result contributes to the quantified version of universal forcing without depending on admissibility for the forcing equivalence itself.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.