narrative_admissible
plain-language theorem explainer
The narrative domain realization meets the admissibility criteria for quantified universal forcing. Researchers formalizing strict logic realizations across canonical domains cite this construction when certifying that each domain satisfies the required structural laws. The definition constructs the AdmissibleRealization instance by directly supplying its three fields via decidable cost equality, an imported associativity result, and reflexivity on the zero element.
Claim. Let the narrative realization have carrier the set of event states, cost function the indicator of equality (returning 0 precisely when states coincide), and composition the componentwise sum on act and beat coordinates. Then cost equality to zero is decidable for every pair of states, composition is associative, and the zero state composed with itself equals the zero state.
background
The AdmissibleRealization structure on a strict logic realization R requires three properties: cost equality to zero is decidable for any pair of carriers; the composition operation is associative; and the distinguished one element satisfies a left-identity or generator-step condition under composition. The strict narrative realization instantiates this with event states as carriers and natural-number costs, where eventCost returns 0 on equality and 1 otherwise, while eventCompose adds the act and beat components. The module elevates the five domain realizations to this typeclass so that the headline quantified universal forcing theorem applies uniformly to any admissible instance rather than to arbitrary strict realizations.
proof idea
The definition is a one-line wrapper that refines the three fields of AdmissibleRealization. The cost-decidability field is supplied by decidable equality on the eventCost function. The associativity field is taken directly from the imported eventCompose_assoc theorem for the narrative domain. The third field is discharged by reflexivity on the composition of narrativeZero with itself.
why it matters
This definition supplies one of the four canonical domain witnesses collected in admissibleClassCert_holds, which in turn feeds the quantified universal forcing theorem. It verifies that the narrative realization (built on beat succession) carries the structural properties needed for the strict universal forcing equivalence to hold under the admissibility constraint. In the Recognition Science setting this step closes the gap between raw strict realizations and the admissible class over which the canonical arithmetic surfaces are forced to coincide.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.