ordered_faithful
plain-language theorem explainer
The ordered realization natOrderedRealization satisfies the FaithfulArithmeticInterpretation interface by preserving equality of LogicNat terms and ensuring the successor never collapses to zero. Researchers tracing the universal forcing chain cite it to confirm that the ordered arithmetic layer embeds without loss of distinctness. The tactic proof splits into an injectivity step that invokes the LogicNat-to-Nat transfer theorem and a non-collapse step that reduces directly to the standard successor axiom.
Claim. The ordered realization of arithmetic via natOrderedRealization is faithful: the interpretation map is injective on LogicNat, and the successor of any term is never equal to the zero term.
background
The module constructs an ordered faithful realization for universal forcing. LogicNat is the inductive type whose constructors identity (zero-cost element) and step (one iteration of the generator) mirror the multiplicative orbit {1, γ, γ², …} inside the positive reals. natOrderedRealization equips this type with the ordered structure that recovers the standard Peano order on the image. The upstream transfer theorem states that an equation in LogicNat holds if and only if the corresponding equation holds after mapping to Nat; the companion lemma succ_ne_zero is the contrapositive of Peano’s first axiom.
proof idea
The proof proceeds by two separate tactics. The injective field applies the mpr direction of eq_iff_toNat_eq to the equality hypothesis. The zero_step_noncollapse field uses congrArg id to obtain a Nat-level equality, simplifies the definition of natOrderedRealization, and finishes with Nat.succ_ne_zero.
why it matters
This result anchors the ordered arithmetic interpretation inside the foundation layer that supports the T0–T8 forcing chain. It supplies the faithfulness guarantee required before the J-uniqueness step (T5) and the emergence of three spatial dimensions (T8) can be derived from the same ordered carrier. With no downstream uses yet recorded, the theorem functions as a base case that later ordered-logic constructions can invoke without re-proving injectivity.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.