narrativeRealization
plain-language theorem explainer
NarrativeRealization supplies a concrete LogicRealization whose carrier is the natural numbers viewed as beat counts generated by an inciting event. Researchers tracing the logic-to-arithmetic forcing chain would cite it to embed narrative order into the same Peano structure carried by LogicNat. The definition proceeds by direct field assignment that delegates the orbit and its axioms to LogicNat while verifying the remaining conditions by reflexivity and the already-proved injectivity and induction theorems.
Claim. The narrative realization is the structure with carrier set $N$ (natural numbers), cost function given by beat-count comparison, zero element $0$, successor $n+1$, orbit given by the inductive type with constructors identity and step, and interpretation map that sends the orbit to $N$ while preserving zero and successor.
background
A LogicRealization equips a carrier with a cost function, an orbit under a generator, and an interpretation map satisfying the axioms of arithmetic derived from logic. NarrativeBeat is the abbreviation for the type of natural numbers that represent beat counts. LogicNat is the inductive type with constructors identity and step that encodes the orbit generated by repeated application of the generator, as detailed in ArithmeticFromLogic where successor injectivity and induction are already theorems.
proof idea
The definition constructs the LogicRealization by assigning Carrier to NarrativeBeat, Cost to Nat, zero and step to the corresponding Nat and LogicNat operations, and interpret to narrativeInterpret. interpret_zero and interpret_step hold by reflexivity; orbit_no_confusion applies zero_ne_succ; orbit_step_injective reuses succ_injective; orbit_induction applies LogicNat.induction; nontriviality is witnessed by the element 1 together with a direct computation of narrativeCost.
why it matters
This definition realizes the structural claim that narrative order carries the same forced Peano object, feeding directly into narrative_arith_equiv_nat which establishes the equivalence (arithmeticOf narrativeRealization).peano.carrier ≃ LogicNat. It supplies the concrete model needed in the UniversalForcing module to identify beat counts with the orbit forced by logic, supporting the transition from logic to arithmetic in the T0-T8 chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.