equivNat
plain-language theorem explainer
Equivalence between the naturals forced by the law of logic and the standard naturals is witnessed by iteration counting and orbit reconstruction. Researchers recovering arithmetic from the functional equation cite this carrier bijection when transferring Peano results into the orbit setting. The definition assembles the equivalence directly from the forward map, its inverse, and the two round-trip lemmas established by induction.
Claim. The naturals forced by the law of logic are in canonical bijection with the standard natural numbers, realized by the iteration-counting map that sends the identity element to zero and each successive step to the successor, together with its inverse that rebuilds the orbit by iterated application of the step constructor.
background
Logic naturals form an inductive type whose identity constructor represents the zero-cost multiplicative identity and whose step constructor iterates the generator once more. This two-constructor structure mirrors the orbit {1, γ, γ², γ³, …} as the smallest subset of the positive reals that contains 1 and is closed under multiplication by γ.
proof idea
The definition constructs the equivalence structure by designating the iteration counter as the forward map and the orbit builder as the inverse map, then supplying the round-trip theorems fromNat_toNat and toNat_fromNat as the left and right inverse proofs.
why it matters
This declaration supplies the carrier identification that lets standard arithmetic results transfer to the logic naturals. It is used to prove that the partial order on logic naturals coincides with the order on their counts and to construct the equivalence between ticks and logic naturals. The step completes the recovery of the natural-number carrier inside the arithmetic-from-logic development, bridging the orbit forced by the functional equation to conventional Peano arithmetic.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.
papers checked against this theorem (showing 14 of 14)
-
Pi-0-1 arithmetic validity equals validity in minimal separation logic
"a formula in Peano arithmetic is valid in the standard model if and only if its translation in this fragment is valid in the standard interpretation"
-
Every lattice vector equals difference of two -2 vectors
"As a consequence, every unnodal Enriques surface admits an Ulrich line bundle"
-
Derived equivalence preserves h^{0,p} numbers
"Let X_1 and X_2 be derived equivalent smooth projective varieties over the field of complex numbers."
-
Diagonal cycles form bipartite Euler system for symmetric cube
"We show that the Gross-Schoen diagonal cycles form a Bipartite Euler system for the symmetric cube motive of a modular form."
-
K-theory removes semi-simplicity from zeta-value formula
"Theorem 2.14. We have that K₀(Arith_{S¹}(R)) ≃ (⊕_{p∈Spec(R)(0)} Z) ⊕ Z, where the extra copy of Z is the image of a canonical splitting K₀(C(S¹,F)) → K₀(Arith_{S¹}(R)). Each copy of Z indexed by a height 1 prime p ... generated by the class of R/p."
-
Lie algebras structure unstable homotopy groups
"Quillen famously showed that simply connected rational homotopy theory can be modeled by simplicial Lie algebras over Q [Qui69]."
-
Hardness assumption stops PV1 proving every number has a prime divisor
"Assuming that no family of polynomial-size Boolean circuits can factorize a constant fraction of all products of two n-bit primes, we show that the bounded arithmetic theory PV1, even when augmented by the sharply bounded choice scheme BB(Σ^b_0), cannot prove that every number has some prime divisor."
-
MSO recovers laminar trees from set systems
"We show that from a laminar set system we can obtain the corresponding laminar tree by means of a monadic second order logic (MSO) transduction. This resolves an open question originally asked by Courcelle."
-
Splitting and merging unify graphs, vines and single-peaked domains
"Theorem 3.7. ... the pair (F, σ_F) is unique ... η is a natural isomorphism."
-
Galois qudits match s qubits exactly in Pauli group and Clifford hierarchy
"A Galois qudit of dimension q = 2^s is exactly the same thing as a collection of s qubits, not only in its Hilbert space, but also in its Pauli group, and Clifford hierarchy."
-
Cyclotomic analysis gives all exact Floquet recurrence times
"Leveraging techniques from algebraic field theory, we construct an arithmetic framework that identifies all possible recurrence times by analyzing the cyclotomic structure of the Floquet unitary's spectrum... ϕ(n) divides d![K:Q]"
-
Goodstein theorem generalizes to Π¹₁-CA₀
"We generalize Goodstein’s theorem and Cichon’s independence proof to Π¹₁-CA₀ using results from Wilken [3]. The method is generalizable to stronger notation systems that provide or enable unique terms for ordinals and enjoy Bachmann property."
-
Two agents invent numbers to handle unseen visual cases
"two agents, without prior mathematical knowledge, can develop a shared symbolic protocol to solve a visually grounded task where the use of a numerical system facilitates extrapolation"
-
Language models fail at extended rule following
"model behavior is consistent neither with open-ended logic nor with stable application of a learned rule, but instead with use of a finite set of count-like internal states"