strictNarrativeRealization
plain-language theorem explainer
The declaration constructs the narrative strict logic realization by assigning event states as carrier, natural numbers as cost, the zero-on-equals function as comparison, coordinate addition as composition, the zero state as unit, and the inciting beat as generator. Researchers assembling admissible realizations for the four canonical domains cite it when verifying the universal forcing equivalence. The body is a direct structure instantiation with field assignments and one simp reduction for the nontriviality law.
Claim. Define the narrative realization as the structure with carrier the set of pairs $(a,b)inmathbb{N}timesmathbb{N}$, cost function returning 0 on identical pairs and 1 otherwise, composition by componentwise addition of coordinates, zero element the state with both coordinates zero, generator the inciting beat state, identity law witnessed by the self-cost identity, non-contradiction law by the symmetry of cost, excluded-middle/composition/invariance laws holding as the trivial proposition, and nontriviality verified by simplification.
background
In the Strict/Narrative module, event states are pairs of natural numbers recording act and beat coordinates. The cost between two states returns zero exactly when the states coincide and one otherwise. Composition adds the act and beat components separately. This supplies the concrete realization for the narrative domain inside the strict universal forcing construction. The module draws on the compose operation from virtue effects, which combines changes additively and multiplicatively, and on the one elements from the integers and rationals constructed from logic. These inform the choice of zero and unit. Upstream results include the self-cost theorem establishing that cost of any state with itself is zero and the symmetry theorem for non-contradiction.
proof idea
The definition populates each field of the StrictLogicRealization structure by direct reference to sibling definitions: the zero-on-equals function for comparison, coordinate addition for composition, the zero state for the unit, and the inciting beat for the generator. The identity and non-contradiction laws are witnessed by the self-cost and symmetry theorems. The excluded-middle, composition, and invariance laws are set to the trivial proposition True. Nontriviality is discharged by a single simp tactic that unfolds the cost, generator, and zero definitions.
why it matters
This supplies the narrative instance required by the AdmissibleClassCert structure, which assembles witnesses for music, biology, narrative, and ethics. It is invoked in the four-canonical-domains-admissible theorem and the narrative-admissible definition to confirm admissibility does not obstruct the universal forcing equivalence. In the Recognition Science framework it realizes one of the four canonical domains feeding the strict logic realizations, consistent with the J-uniqueness and phi fixed-point steps in the forcing chain. It closes part of the scaffolding for the axiom audit by enabling the downstream arithmetic equivalence.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.