pith. sign in
theorem

fromNat_toNat

proved
show as:
module
IndisputableMonolith.Foundation.ArithmeticFromLogic
domain
Foundation
line
235 · github
papers citing
2 papers (below)

plain-language theorem explainer

The theorem shows that counting iterations in LogicNat and rebuilding the structure recovers the original element exactly. Foundation researchers cite it to justify routing arithmetic proofs through standard natural numbers. The argument is a direct induction on the two-constructor inductive type, applying the successor commutation rules at the inductive step.

Claim. Let $L$ be the inductive type generated by the zero-cost identity element and the successor operation. Let $f:ℕ→L$ iterate the successor starting from identity and let $g:L→ℕ$ count the number of successor applications. Then $f(g(n))=n$ for every $n∈L$.

background

LogicNat is the inductive type whose constructors are identity (the zero-cost multiplicative identity) and step (one further application of the generator). Its doc-comment states that the structure mirrors the orbit {1, γ, γ², …} as the smallest subset of ℝ₊ closed under multiplication by γ and containing 1. The forward map toNat sends identity to 0 and step n to 1 + toNat n. The inverse map fromNat sends 0 to identity and successor k to step (fromNat k). These maps appear in the ArithmeticFromLogic module after the Peano primitives are derived as theorems rather than axioms.

proof idea

Proof by induction on the structure of the element of LogicNat. The identity case is reflexivity. In the step case the goal is rewritten by the successor lemmas toNat_succ and fromNat_succ, after which the induction hypothesis closes the equality.

why it matters

This left-inverse statement is the key lemma that lets equivNat be defined as the equivalence LogicNat ≃ Nat. It is invoked directly in eq_iff_toNat_eq, add_left_cancel, embed_injective, le_antisymm and toNat_le, all of which transfer statements between the abstract orbit and ordinary arithmetic. In the Recognition framework it completes the bridge from the Law of Logic to the natural-number arithmetic required for the forcing chain and the phi-ladder mass formula.

Switch to Lean above to see the machine-checked source, dependencies, and usage graph.

papers checked against this theorem (showing 2 of 2)