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`. -/
used by (5)
From the project-wide theorem graph. These declarations reference this one in their body.