narrative_arith_equiv_logicNat
plain-language theorem explainer
Definition narrative_arith_equiv_logicNat supplies the canonical equivalence between the Peano carrier of the arithmetic extracted from the strict narrative realization and the inductive LogicNat type. Researchers tracing the logic-to-arithmetic forcing chain would cite it to verify that beat-succession event states reproduce the same naturals as the abstract orbit. The body is a one-line wrapper delegating to the orbit equivalence on the lightweight conversion of the realization.
Claim. Let $R$ be the strict narrative realization over event states whose generator is the inciting beat step. Then the Peano carrier of the arithmetic derived from $R$ is equivalent to the inductive type of natural numbers forced by the Law of Logic: $(arith R).peano.carrier ≃ LogicNat$.
background
The module Strict/Narrative.lean supplies a domain-rich narrative realization over event states equipped with act and beat coordinates; the generator is the inciting beat-step. StrictLogicRealization is the structure carrying native law data (Carrier, Cost, zeroCost, compare, compose) with no supplied orbit. The arith operation extracts the forced arithmetic from the lightweight form of any such realization. LogicNat is the inductive type with constructors identity (zero-cost element) and step, mirroring the orbit {1, γ, γ², …} closed under multiplication by the generator γ.
proof idea
The definition is a one-line wrapper that applies the orbitEquivLogicNat equivalence to the lightweight realization produced by toLightweight on strictNarrativeRealization.
why it matters
The definition confirms that the narrative realization using beat succession yields arithmetic canonically equivalent to LogicNat, closing one link in the extraction of forced arithmetic from the Law of Logic. It supports the T0–T8 forcing chain by showing that concrete event-state carriers reproduce the abstract naturals without additional hypotheses. No downstream theorems are recorded yet.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.