strictNarrativeRealization
plain-language theorem explainer
The strict narrative realization supplies the narrative domain as a StrictLogicRealization whose carrier consists of event states with act and beat coordinates and whose generator is the inciting beat step. Researchers verifying the four canonical domains or the quantified universal forcing equivalence cite it when assembling AdmissibleClassCert. The definition is a direct record construction that populates the interface fields from local eventCost and eventCompose definitions, with one simp discharging the nontrivial law.
Claim. The strict narrative realization is the StrictLogicRealization whose carrier is the set of pairs $(act, beat) ∈ ℕ × ℕ$, whose cost function returns 0 on equal states and 1 otherwise, whose composition adds the coordinate pairs, whose zero is narrativeZero, whose generator is incitingBeat, and whose remaining laws hold by the identities eventCost_self, eventCost_symm together with the trivial propositions for excluded middle, composition, and invariance.
background
The module Strict/Narrative.lean supplies a domain-rich realization over event states. EventState is the structure with fields act : Nat and beat : Nat. eventCost returns 0 when its arguments are equal and 1 otherwise; eventCompose adds the act and beat coordinates componentwise. The generator incitingBeat and zero narrativeZero are the remaining local constants that complete the interface. This construction sits inside the StrictLogicRealization record, which encodes the minimal algebraic structure required for the universal forcing equivalence. Upstream results include the virtue composition law and the definitions of one in LogicInt and LogicRat, though the narrative instance relies primarily on its sibling eventCost and eventCompose.
proof idea
The definition is a record literal that directly assigns Carrier := EventState, Cost := Nat, compare := eventCost, compose := eventCompose, one := narrativeZero, generator := incitingBeat, identity_law := eventCost_self, non_contradiction_law := eventCost_symm, and the three remaining laws to True. The sole nontrivial_law is discharged by the tactic simp [eventCost, incitingBeat, narrativeZero].
why it matters
This definition supplies the narrative member of the four canonical domain realizations used by four_canonical_domains_admissible and AdmissibleClassCert to witness that each domain admits a StrictLogicRealization. It is referenced by narrative_admissible, _narrative_ok, and narrative_arith_equiv_logicNat, which in turn feed the quantified universal forcing statement. The construction therefore closes one slot in the strict universal forcing chain, allowing the orbit equivalence between the arithmetic carrier and LogicNat to be instantiated for the narrative domain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.