eq_iff_toNat_eq
plain-language theorem explainer
The declaration states that equality of two LogicNat elements holds exactly when their images under toNat coincide. Foundation researchers cite it to transfer equations into standard Nat for omega-based automation. The proof splits the biconditional, applies congruence in one direction, and recovers the original elements via the left-inverse property of fromNat in the other.
Claim. For elements $a, b$ of the inductive type LogicNat, $a = b$ if and only if toNat$(a) =$ toNat$(b)$.
background
LogicNat is the inductive type with constructors identity (the zero-cost base element) and step (one iteration of the generator), realizing the smallest subset of positive reals closed under multiplication by a fixed γ > 1 and containing 1. The map toNat counts steps from identity to send LogicNat into the standard naturals; fromNat is its inverse that rebuilds the element by iterated step. The module ArithmeticFromLogic derives Peano structure directly from the Law of Logic functional equation, with this transfer principle serving as the bridge to Nat tactics.
proof idea
The term-mode proof opens with constructor to split the biconditional. Forward direction is the single application of congrArg toNat. Reverse direction introduces the hypothesis, applies congrArg fromNat, rewrites both sides by the left-inverse theorem fromNat_toNat, and concludes by exact.
why it matters
It supplies the equality transfer used in the definitions of addition, multiplication, and negation on LogicInt, in the transitivity proof for the integer relation, and in the faithfulness statement for the ordered realization. The lemma therefore closes the route from the forced naturals back to standard arithmetic, supporting the Recognition Science derivation of integers from the single functional equation without external axioms.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.