eq_iff_toNat_eq
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.
claimFor 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 in Recognition Science
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.
scope and limits
- Does not establish the embedding of LogicNat into positive reals or its cost ordering.
- Does not prove properties of toNat beyond equality transfer.
- Does not address operations other than equality on LogicNat.
Lean usage
example {a b : LogicNat} (h : toNat a = toNat b) : a = b := (eq_iff_toNat_eq).mpr hformal statement (Lean)
302theorem eq_iff_toNat_eq {a b : LogicNat} : a = b ↔ toNat a = toNat b := by
proof body
Term-mode proof.
303 constructor
304 · exact congrArg toNat
305 · intro h
306 have := congrArg fromNat h
307 rw [fromNat_toNat, fromNat_toNat] at this
308 exact this
309
310/-! ## 5b. Order on LogicNat
311
312Order is forced by the orbit's cost ordering: in the orbit
313`{1, γ, γ², ...}` with `γ > 1`, the cost `J(γⁿ)` is strictly
314increasing in `n`. Section 6's `embed_strictMono` establishes this
315analytically. Here we define the abstract Peano order intrinsically
316to `LogicNat` (via existence of an additive complement) so the order
317content does not depend on which generator was used. The connection
318back to the orbit is `embed_le_iff` in Section 6.
319
320The standard Peano definition: `n ≤ m` iff there exists `k` with
321`n + k = m`. Strict order: `n < m` iff there exists `k` with
322`n + step k = m`. -/
323
324/-- Non-strict order on `LogicNat`. -/