IndisputableMonolith.Foundation.ArithmeticFromLogic
IndisputableMonolith/Foundation/ArithmeticFromLogic.lean · 720 lines · 72 declarations
show as:
view math explainer →
1/-
2 ArithmeticFromLogic.lean
3
4 Recovery of the natural numbers from the Law of Logic.
5
6 Status: Level 1. The inductive structure of the natural numbers,
7 Peano's axioms, and the addition/multiplication operations are
8 recovered as forced consequences of `SatisfiesLawsOfLogic C` plus
9 the existence of a non-trivial generator. Section 5 ("Embedding into
10 ℝ₊") establishes the structural map from `LogicNat` to the
11 multiplicative group of positive reals via iteration of a generator;
12 this is what ties the abstract Peano structure back to the
13 comparison operator.
14
15 No assumption is made about base 10. The recovery works at the level
16 of the inductive structure (zero, successor) and never references a
17 positional representation.
18
19 Forcing chain made explicit by this module:
20 Law of Logic (four Aristotelian conditions on C)
21 ⊢ J = derivedCost C is the unique calibrated reciprocal cost
22 ⊢ existence of identity element (J(1) = 0) and a non-trivial
23 generator γ (J(γ) > 0 for some γ ≠ 1)
24 ⊢ orbit structure {1, γ, γ², γ³, ...} is Peano-shaped
25 ⊢ LogicNat (this module) ≃ Nat as semirings.
26
27 References:
28 - Foundation.LogicAsFunctionalEquation: SatisfiesLawsOfLogic, the
29 Translation Theorem, the J-uniqueness corollary.
30 - Cost.FunctionalEquation: washburn_uniqueness_aczel.
31 - Foundation.DAlembert.Inevitability: bilinear_family_forced.
32-/
33
34import Mathlib
35import IndisputableMonolith.Foundation.LogicAsFunctionalEquation
36
37namespace IndisputableMonolith
38namespace Foundation
39namespace ArithmeticFromLogic
40
41open IndisputableMonolith.Foundation.LogicAsFunctionalEquation
42
43/-! ## 1. The Inductive Structure Forced by the Comparison Operator
44
45The Law of Logic, applied to a non-trivial comparison operator, gives:
46
47 - an identity element (x = 1, the unique zero of the derived cost J)
48 - a non-trivial generator γ ≠ 1 with strictly positive cost
49
50The orbit of γ under repeated multiplication, together with the
51identity, has exactly two constructors: "be at the identity" and "take
52one more step." That two-constructor structure is the natural-number
53structure. We make it an inductive type below.
54
55Nothing in the construction references base 10, base 2, or any
56positional system. The only primitives are the identity element and
57the step operation. -/
58
59/-- The natural numbers as forced by the Law of Logic.
60
61`identity` represents the zero-cost element (the multiplicative
62identity in the orbit). `step` represents one more iteration of the
63generator. The two-constructor structure mirrors the orbit
64{1, γ, γ², γ³, ...} as the smallest subset of ℝ₊ closed under
65multiplication by γ and containing 1. -/
66inductive LogicNat : Type
67 | identity : LogicNat
68 | step : LogicNat → LogicNat
69 deriving DecidableEq, Repr
70
71namespace LogicNat
72
73/-! ## 2. Zero and Successor (Peano Primitives) -/
74
75/-- Zero is the identity comparison: a thing compared with itself,
76costing zero in J. -/
77@[simp] def zero : LogicNat := .identity
78
79/-- Successor is one more application of the generator. -/
80@[simp] def succ (n : LogicNat) : LogicNat := .step n
81
82/-! ## 3. Peano Axioms as Theorems
83
84Each axiom is a theorem of the inductive structure. None is posited.
85-/
86
87/-- **Peano P1 (zero is not a successor)**: the identity is
88distinguishable from any iterate of the generator. -/
89theorem zero_ne_succ (n : LogicNat) : zero ≠ succ n := by
90 intro h; cases h
91
92/-- **Peano P1, contrapositive**: every successor differs from zero. -/
93theorem succ_ne_zero (n : LogicNat) : succ n ≠ zero := by
94 intro h; cases h
95
96/-- **Peano P2 (successor injectivity)**: forced by the constructor
97disjointness of the inductive type, which itself reflects the
98injectivity of multiplication by the generator on the orbit. -/
99theorem succ_injective : Function.Injective succ := by
100 intro a b h
101 cases h
102 rfl
103
104/-- **Peano P3 (induction)**: any property closed under successor and
105holding at zero holds for every `LogicNat`. -/
106theorem induction
107 {motive : LogicNat → Prop}
108 (h0 : motive zero)
109 (hs : ∀ n, motive n → motive (succ n)) :
110 ∀ n, motive n := by
111 intro n
112 induction n with
113 | identity => exact h0
114 | step n ih => exact hs n ih
115
116/-! ## 4. Addition and Multiplication
117
118Addition is repeated successor; multiplication is repeated addition.
119Both are defined by recursion on the second argument. We register
120them as `Add` and `Mul` instances so Lean's standard `+` and `*`
121notation work on `LogicNat` directly. -/
122
123/-- Addition by recursion on the second argument. -/
124def add : LogicNat → LogicNat → LogicNat
125 | n, .identity => n
126 | n, .step m => .step (add n m)
127
128instance : Add LogicNat := ⟨add⟩
129instance : Zero LogicNat := ⟨zero⟩
130instance : One LogicNat := ⟨succ zero⟩
131
132@[simp] theorem add_def (n m : LogicNat) : n + m = add n m := rfl
133@[simp] theorem zero_def : (0 : LogicNat) = zero := rfl
134@[simp] theorem one_def : (1 : LogicNat) = succ zero := rfl
135
136@[simp] theorem add_zero (n : LogicNat) : n + zero = n := rfl
137
138@[simp] theorem add_succ (n m : LogicNat) : n + succ m = succ (n + m) := rfl
139
140theorem zero_add (n : LogicNat) : zero + n = n := by
141 induction n with
142 | identity => rfl
143 | step n ih =>
144 show zero + succ n = succ n
145 rw [add_succ, ih]
146
147theorem succ_add (n m : LogicNat) : succ n + m = succ (n + m) := by
148 induction m with
149 | identity => rfl
150 | step m ih =>
151 show succ n + succ m = succ (n + succ m)
152 rw [add_succ, add_succ, ih]
153
154theorem add_assoc (a b c : LogicNat) : (a + b) + c = a + (b + c) := by
155 induction c with
156 | identity => rfl
157 | step c ih =>
158 show (a + b) + succ c = a + (b + succ c)
159 rw [add_succ, add_succ, add_succ, ih]
160
161theorem add_comm (a b : LogicNat) : a + b = b + a := by
162 induction b with
163 | identity =>
164 show a + zero = zero + a
165 rw [add_zero, zero_add]
166 | step b ih =>
167 show a + succ b = succ b + a
168 rw [add_succ, succ_add, ih]
169
170/-- Multiplication by recursion on the second argument. -/
171def mul : LogicNat → LogicNat → LogicNat
172 | _, .identity => zero
173 | n, .step m => mul n m + n
174
175instance : Mul LogicNat := ⟨mul⟩
176
177@[simp] theorem mul_def (n m : LogicNat) : n * m = mul n m := rfl
178
179@[simp] theorem mul_zero (n : LogicNat) : n * zero = zero := rfl
180
181@[simp] theorem mul_succ (n m : LogicNat) : n * succ m = n * m + n := rfl
182
183theorem zero_mul (n : LogicNat) : zero * n = zero := by
184 induction n with
185 | identity => rfl
186 | step n ih =>
187 show zero * succ n = zero
188 rw [mul_succ, ih, zero_add]
189
190theorem mul_one (n : LogicNat) : n * succ zero = n := by
191 show n * succ zero = n
192 rw [mul_succ, mul_zero, zero_add]
193
194theorem one_mul (n : LogicNat) : succ zero * n = n := by
195 induction n with
196 | identity => rfl
197 | step n ih =>
198 show succ zero * succ n = succ n
199 rw [mul_succ, ih]
200 show n + succ zero = succ n
201 rw [add_succ, add_zero]
202
203theorem mul_add (a b c : LogicNat) : a * (b + c) = a * b + a * c := by
204 induction c with
205 | identity =>
206 show a * (b + zero) = a * b + a * zero
207 rw [add_zero, mul_zero, add_zero]
208 | step c ih =>
209 show a * (b + succ c) = a * b + a * succ c
210 rw [add_succ, mul_succ, mul_succ, ih, add_assoc]
211
212/-! ## 5. Recovery Theorem: LogicNat ≃ Nat
213
214Lean's built-in `Nat` has the same inductive shape as `LogicNat`. The
215two are isomorphic. This is the recovery: the natural numbers Lean
216already has are exactly the structure forced by the Law of Logic, with
217no base 10, no positional representation, and no arithmetic axioms
218posited. -/
219
220/-- The forward map: read off the iteration count. -/
221def toNat : LogicNat → Nat
222 | .identity => 0
223 | .step n => Nat.succ (toNat n)
224
225/-- The inverse map: build the orbit by iterating the step. -/
226def fromNat : Nat → LogicNat
227 | 0 => .identity
228 | Nat.succ n => .step (fromNat n)
229
230@[simp] theorem toNat_zero : toNat zero = 0 := rfl
231@[simp] theorem toNat_succ (n : LogicNat) : toNat (succ n) = Nat.succ (toNat n) := rfl
232@[simp] theorem fromNat_zero : fromNat 0 = zero := rfl
233@[simp] theorem fromNat_succ (n : Nat) : fromNat (Nat.succ n) = succ (fromNat n) := rfl
234
235theorem fromNat_toNat : ∀ n : LogicNat, fromNat (toNat n) = n := by
236 intro n
237 induction n with
238 | identity => rfl
239 | step n ih =>
240 show fromNat (toNat (succ n)) = succ n
241 rw [toNat_succ, fromNat_succ, ih]
242
243theorem toNat_fromNat : ∀ n : Nat, toNat (fromNat n) = n := by
244 intro n
245 induction n with
246 | zero => rfl
247 | succ n ih =>
248 show toNat (fromNat (Nat.succ n)) = Nat.succ n
249 rw [fromNat_succ, toNat_succ, ih]
250
251/-- **Recovery theorem (carrier)**: `LogicNat` and `Nat` have the same
252underlying set, witnessed by the round-trip equalities. -/
253def equivNat : LogicNat ≃ Nat where
254 toFun := toNat
255 invFun := fromNat
256 left_inv := fromNat_toNat
257 right_inv := toNat_fromNat
258
259/-- **Recovery theorem (addition)**: the addition `LogicNat` carries
260agrees with `Nat` addition under the equivalence. -/
261theorem toNat_add (a b : LogicNat) :
262 toNat (a + b) = toNat a + toNat b := by
263 induction b with
264 | identity =>
265 show toNat (a + zero) = toNat a + toNat zero
266 rw [add_zero, toNat_zero, Nat.add_zero]
267 | step b ih =>
268 show toNat (a + succ b) = toNat a + toNat (succ b)
269 rw [add_succ, toNat_succ, toNat_succ, ih, Nat.add_succ]
270
271/-- **Recovery theorem (multiplication)**: the multiplication
272`LogicNat` carries agrees with `Nat` multiplication under the
273equivalence. -/
274theorem toNat_mul (a b : LogicNat) :
275 toNat (a * b) = toNat a * toNat b := by
276 induction b with
277 | identity =>
278 show toNat (a * zero) = toNat a * toNat zero
279 rw [mul_zero, toNat_zero, Nat.mul_zero]
280 | step b ih =>
281 show toNat (a * succ b) = toNat a * toNat (succ b)
282 rw [mul_succ, toNat_succ, toNat_add, ih, Nat.mul_succ]
283
284/-- Left cancellation: `a + b = a + c ⇒ b = c`. Proved by transferring
285to `Nat` via the recovery isomorphism. -/
286theorem add_left_cancel {a b c : LogicNat} (h : a + b = a + c) : b = c := by
287 have hcast := congrArg toNat h
288 rw [toNat_add, toNat_add] at hcast
289 have hnat : toNat b = toNat c := by omega
290 have := congrArg fromNat hnat
291 rw [fromNat_toNat, fromNat_toNat] at this
292 exact this
293
294/-- Right cancellation: `a + c = b + c ⇒ a = b`. -/
295theorem add_right_cancel {a b c : LogicNat} (h : a + c = b + c) : a = b := by
296 rw [add_comm a c, add_comm b c] at h
297 exact add_left_cancel h
298
299/-- Transfer principle: an equation in `LogicNat` holds iff it holds
300under `toNat`. This is the workhorse for proofs that route through
301`omega` on `Nat`. -/
302theorem eq_iff_toNat_eq {a b : LogicNat} : a = b ↔ toNat a = toNat b := by
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`. -/
325def le (n m : LogicNat) : Prop := ∃ k : LogicNat, n + k = m
326
327/-- Strict order on `LogicNat`. -/
328def lt (n m : LogicNat) : Prop := ∃ k : LogicNat, n + succ k = m
329
330instance : LE LogicNat := ⟨le⟩
331instance : LT LogicNat := ⟨lt⟩
332
333@[simp] theorem le_def (n m : LogicNat) : n ≤ m ↔ ∃ k, n + k = m := Iff.rfl
334@[simp] theorem lt_def (n m : LogicNat) : n < m ↔ ∃ k, n + succ k = m := Iff.rfl
335
336theorem le_refl (n : LogicNat) : n ≤ n := ⟨zero, add_zero n⟩
337
338theorem zero_le (n : LogicNat) : zero ≤ n := ⟨n, zero_add n⟩
339
340theorem le_trans {a b c : LogicNat} (hab : a ≤ b) (hbc : b ≤ c) : a ≤ c := by
341 obtain ⟨k1, hk1⟩ := hab
342 obtain ⟨k2, hk2⟩ := hbc
343 refine ⟨k1 + k2, ?_⟩
344 rw [← add_assoc, hk1, hk2]
345
346theorem le_succ (n : LogicNat) : n ≤ succ n := ⟨succ zero, by
347 show n + succ zero = succ n
348 rw [add_succ, add_zero]⟩
349
350theorem succ_le_succ {a b : LogicNat} (h : a ≤ b) : succ a ≤ succ b := by
351 obtain ⟨k, hk⟩ := h
352 refine ⟨k, ?_⟩
353 show succ a + k = succ b
354 rw [succ_add, hk]
355
356theorem lt_iff_succ_le {n m : LogicNat} : n < m ↔ succ n ≤ m := by
357 constructor
358 · rintro ⟨k, hk⟩
359 refine ⟨k, ?_⟩
360 show succ n + k = m
361 rw [succ_add]
362 show succ (n + k) = m
363 rw [← add_succ]
364 -- need n + succ k = m, but we have n + succ k = m via hk; succ_add transforms
365 -- Wait: hk : n + succ k = m, and succ (n + k) = n + succ k by add_succ. So succ (n + k) = m.
366 exact hk
367 · rintro ⟨k, hk⟩
368 refine ⟨k, ?_⟩
369 show n + succ k = m
370 rw [add_succ]
371 show succ (n + k) = m
372 rw [← succ_add]
373 exact hk
374
375theorem lt_irrefl (n : LogicNat) : ¬ n < n := by
376 rintro ⟨k, hk⟩
377 -- n + succ k = n. Apply toNat: toNat n + toNat (succ k) = toNat n on Nat.
378 have := congrArg toNat hk
379 rw [toNat_add, toNat_succ] at this
380 -- this : toNat n + Nat.succ (toNat k) = toNat n
381 omega
382
383theorem lt_trans {a b c : LogicNat} (hab : a < b) (hbc : b < c) : a < c := by
384 rw [lt_iff_succ_le] at hab hbc ⊢
385 exact le_trans hab (le_trans (le_succ b) hbc)
386
387theorem zero_lt_succ (n : LogicNat) : zero < succ n :=
388 ⟨n, by show zero + succ n = succ n; rw [zero_add]⟩
389
390theorem lt_iff_le_and_ne {a b : LogicNat} : a < b ↔ a ≤ b ∧ a ≠ b := by
391 constructor
392 · rintro ⟨k, hk⟩
393 refine ⟨⟨succ k, hk⟩, ?_⟩
394 intro hab
395 rw [hab] at hk
396 -- b + succ k = b means succ k = 0 by additive cancellation; impossible.
397 have := congrArg toNat hk
398 rw [toNat_add, toNat_succ] at this
399 omega
400 · rintro ⟨⟨k, hk⟩, hne⟩
401 -- a + k = b, a ≠ b, so k ≠ 0; k = succ k' for some k'.
402 cases k with
403 | identity =>
404 exfalso
405 apply hne
406 simpa using hk
407 | step k' => exact ⟨k', hk⟩
408
409theorem le_antisymm {a b : LogicNat} (hab : a ≤ b) (hba : b ≤ a) : a = b := by
410 obtain ⟨k1, hk1⟩ := hab
411 obtain ⟨k2, hk2⟩ := hba
412 have h1 := congrArg toNat hk1
413 have h2 := congrArg toNat hk2
414 rw [toNat_add] at h1 h2
415 -- toNat a + toNat k1 = toNat b, toNat b + toNat k2 = toNat a.
416 have hnat : toNat a = toNat b := by omega
417 -- Lift to LogicNat via the equivalence.
418 have := congrArg fromNat hnat
419 rw [fromNat_toNat, fromNat_toNat] at this
420 exact this
421
422/-- `LogicNat` carries a partial order via the Peano definition. -/
423instance : Preorder LogicNat where
424 le := le
425 lt := lt
426 le_refl := le_refl
427 le_trans := fun _ _ _ => le_trans
428 lt_iff_le_not_ge := by
429 intro a b
430 -- Unfold lt and le to avoid notation-instance loop in the instance
431 -- definition itself.
432 show lt a b ↔ le a b ∧ ¬ le b a
433 have hiff : lt a b ↔ le a b ∧ a ≠ b := lt_iff_le_and_ne
434 rw [hiff]
435 constructor
436 · rintro ⟨hab, hne⟩
437 refine ⟨hab, ?_⟩
438 intro hba
439 exact hne (le_antisymm hab hba)
440 · rintro ⟨hab, hnba⟩
441 refine ⟨hab, ?_⟩
442 intro habeq
443 exact hnba (habeq ▸ le_refl b)
444
445/-- `LogicNat` is a partial order. -/
446instance : PartialOrder LogicNat where
447 __ := (inferInstance : Preorder LogicNat)
448 le_antisymm := fun _ _ => le_antisymm
449
450/-! ## Recovery (Order): Peano order matches `Nat` order. -/
451
452theorem toNat_le (a b : LogicNat) : a ≤ b ↔ toNat a ≤ toNat b := by
453 constructor
454 · rintro ⟨k, hk⟩
455 have := congrArg toNat hk
456 rw [toNat_add] at this
457 omega
458 · intro h
459 refine ⟨fromNat (toNat b - toNat a), ?_⟩
460 have hroundtrip : ∀ n : LogicNat, fromNat (toNat n) = n := fromNat_toNat
461 -- toNat (a + fromNat (toNat b - toNat a)) = toNat a + (toNat b - toNat a) = toNat b
462 have hadd : toNat (a + fromNat (toNat b - toNat a)) = toNat b := by
463 rw [toNat_add, toNat_fromNat]
464 omega
465 -- Apply equivNat injectivity
466 have : a + fromNat (toNat b - toNat a) = b := by
467 have h1 := congrArg fromNat hadd
468 rw [hroundtrip, hroundtrip] at h1
469 exact h1
470 exact this
471
472theorem toNat_lt (a b : LogicNat) : a < b ↔ toNat a < toNat b := by
473 rw [lt_iff_succ_le, toNat_le]
474 constructor
475 · intro h
476 rw [toNat_succ] at h
477 omega
478 · intro h
479 rw [toNat_succ]
480 omega
481
482/-- `LogicNat` is a linear order: any two elements are comparable, and
483the order is decidable. Both follow from the recovery isomorphism with
484`Nat`. -/
485instance : LinearOrder LogicNat where
486 __ := (inferInstance : PartialOrder LogicNat)
487 le_total := fun a b => by
488 rcases Nat.le_total (toNat a) (toNat b) with h | h
489 · left
490 exact (toNat_le a b).mpr h
491 · right
492 exact (toNat_le b a).mpr h
493 toDecidableLE := fun a b =>
494 decidable_of_iff (toNat a ≤ toNat b) (toNat_le a b).symm
495 toDecidableEq := inferInstance
496
497/-- `LogicNat` is well-founded under strict order: induction on size is
498admissible. Transfer from `Nat`'s well-foundedness via the recovery
499isomorphism. -/
500instance : WellFoundedLT LogicNat where
501 wf := by
502 have hNat : WellFounded (fun a b : LogicNat => toNat a < toNat b) :=
503 InvImage.wf toNat (Nat.lt_wfRel.wf)
504 apply Subrelation.wf (h₁ := ?_) hNat
505 intro a b h
506 exact (toNat_lt a b).mp h
507
508end LogicNat
509
510/-! ## 6. Embedding into ℝ₊ via a Generator
511
512Section 5 recovers the abstract Peano structure. Section 6 ties that
513structure back to the comparison operator that started the chain. The
514embedding `LogicNat → ℝ₊` sends `n` to `γⁿ` for any non-trivial
515generator `γ` of the multiplicative group of positive reals. This is
516the structural witness that the abstract Peano structure of
517`LogicNat` is the orbit structure of any non-trivial element under
518multiplication.
519
520The full chain (existence of γ from `non_trivial`, injectivity of the
521embedding from the J-cost positivity off-identity, generator-free
522characterization of the embedding's image) is left for Level 2. The
523content of this section is the embedding map and its multiplicative
524homomorphism property. -/
525
526/-- A non-trivial generator: any positive real other than the
527identity. The Law of Logic guarantees existence via the
528`non_trivial` field of `SatisfiesLawsOfLogic`. -/
529structure Generator where
530 value : ℝ
531 pos : 0 < value
532 nontrivial : value ≠ 1
533
534/-- **Chain closure**: a comparison operator satisfying the Law of Logic
535yields an explicit non-trivial generator. The construction extracts the
536witness from `non_trivial` and uses `identity` to rule out `value = 1`.
537
538This is the structural completion of the chain. Before this lemma,
539`Generator` was a free structure; now it is *literally* derived from
540`SatisfiesLawsOfLogic`. -/
541noncomputable def generatorOfLawsOfLogic
542 {C : ComparisonOperator} (hLaws : SatisfiesLawsOfLogic C) : Generator :=
543 let x := Classical.choose hLaws.non_trivial
544 have hx : 0 < x ∧ derivedCost C x ≠ 0 := Classical.choose_spec hLaws.non_trivial
545 { value := x
546 pos := hx.1
547 nontrivial := by
548 intro hx_eq_one
549 apply hx.2
550 show derivedCost C x = 0
551 rw [hx_eq_one]
552 show C 1 1 = 0
553 exact hLaws.identity 1 one_pos }
554
555/-- The orbit embedding: `LogicNat` into the positive reals. -/
556def embed (γ : Generator) : LogicNat → ℝ
557 | .identity => 1
558 | .step n => γ.value * embed γ n
559
560@[simp] theorem embed_zero (γ : Generator) : embed γ LogicNat.zero = 1 := rfl
561
562@[simp] theorem embed_succ (γ : Generator) (n : LogicNat) :
563 embed γ (LogicNat.succ n) = γ.value * embed γ n := rfl
564
565/-- The embedding lands in the strictly positive reals. -/
566theorem embed_pos (γ : Generator) (n : LogicNat) : 0 < embed γ n := by
567 induction n with
568 | identity => exact one_pos
569 | step n ih =>
570 show 0 < γ.value * embed γ n
571 exact mul_pos γ.pos ih
572
573/-- **Multiplicative homomorphism**: addition in `LogicNat` corresponds
574to multiplication of orbit elements. This is the structural fact that
575`LogicNat` *is* the orbit, parameterized by iteration count. -/
576theorem embed_add (γ : Generator) (a b : LogicNat) :
577 embed γ (a + b) = embed γ a * embed γ b := by
578 induction b with
579 | identity =>
580 show embed γ (a + LogicNat.zero) = embed γ a * embed γ LogicNat.zero
581 rw [LogicNat.add_zero, embed_zero, mul_one]
582 | step b ih =>
583 show embed γ (a + LogicNat.succ b) = embed γ a * embed γ (LogicNat.succ b)
584 rw [LogicNat.add_succ, embed_succ, embed_succ, ih]
585 ring
586
587/-- The embedding is the natural-number power of `γ.value`. -/
588theorem embed_eq_pow (γ : Generator) (n : LogicNat) :
589 embed γ n = γ.value ^ (LogicNat.toNat n) := by
590 induction n with
591 | identity => simp [embed, LogicNat.toNat]
592 | step n ih =>
593 show γ.value * embed γ n = γ.value ^ (Nat.succ (LogicNat.toNat n))
594 rw [ih, pow_succ]
595 ring
596
597/-! ## Embedding Injectivity (J-positivity off identity)
598
599The key fact: a non-trivial generator `γ ≠ 1` cannot have `γⁿ = γᵐ`
600for `n ≠ m`. Structurally, this is forced by J-positivity off
601identity: `J(γᵏ) > 0` for any `k ≥ 1` (since `γᵏ ≠ 1` whenever
602`γ ≠ 1` and `k ≥ 1`), and `J(x) = 0 ↔ x = 1`. Analytically, it
603follows from `Real.log γ.value ≠ 0` and the rule `log(γⁿ) = n · log γ`
604on positive reals. The latter route is shorter and is what we use
605here. -/
606
607/-- Logarithm of a non-trivial generator is non-zero. -/
608private theorem log_generator_ne_zero (γ : Generator) :
609 Real.log γ.value ≠ 0 := by
610 intro h
611 -- Real.log_eq_zero_iff: log x = 0 ↔ x = 0 ∨ x = 1 ∨ x = -1
612 rcases (Real.log_eq_zero.mp h) with h0 | h1 | hneg
613 · exact (lt_irrefl (0 : ℝ)) (h0 ▸ γ.pos)
614 · exact γ.nontrivial h1
615 · linarith [γ.pos]
616
617/-- **Embedding injectivity**: distinct natural numbers map to distinct
618points in the orbit. This closes the bridge from the abstract `LogicNat`
619to the concrete orbit `{1, γ, γ², ...}` in ℝ₊. -/
620theorem embed_injective (γ : Generator) : Function.Injective (embed γ) := by
621 intro a b hab
622 -- Translate to powers.
623 rw [embed_eq_pow, embed_eq_pow] at hab
624 -- Take logs.
625 have hpos_a : 0 < γ.value ^ (LogicNat.toNat a) := pow_pos γ.pos _
626 have hpos_b : 0 < γ.value ^ (LogicNat.toNat b) := pow_pos γ.pos _
627 have hlog : Real.log (γ.value ^ (LogicNat.toNat a))
628 = Real.log (γ.value ^ (LogicNat.toNat b)) := by
629 exact congrArg Real.log hab
630 rw [Real.log_pow, Real.log_pow] at hlog
631 -- Cancel the non-zero log γ.value.
632 have hne := log_generator_ne_zero γ
633 have hcast : ((LogicNat.toNat a : ℝ)) = ((LogicNat.toNat b : ℝ)) := by
634 have := mul_right_cancel₀ hne hlog
635 exact this
636 have h_nat : LogicNat.toNat a = LogicNat.toNat b := by exact_mod_cast hcast
637 -- Lift back to LogicNat via the equivalence.
638 have := congrArg LogicNat.fromNat h_nat
639 rw [LogicNat.fromNat_toNat, LogicNat.fromNat_toNat] at this
640 exact this
641
642/-! ## Order via the Embedding (γ > 1 case)
643
644When `γ > 1`, the orbit is strictly increasing under multiplication
645by `γ`, and `embed γ` is a strictly monotone embedding of the Peano
646order on `LogicNat` into `(ℝ, ≤)`. This is the analytic counterpart
647of the abstract Peano order from Section 5b. -/
648
649/-- For `γ > 1`, `γⁿ ≤ γᵐ ↔ n ≤ m` on `Nat`. -/
650private theorem pow_le_pow_iff_of_one_lt {γ : ℝ} (hγ : 1 < γ) (n m : Nat) :
651 γ ^ n ≤ γ ^ m ↔ n ≤ m := by
652 constructor
653 · intro h
654 by_contra hlt
655 push_neg at hlt
656 have : γ ^ m < γ ^ n := pow_lt_pow_right₀ hγ hlt
657 linarith
658 · intro h
659 exact pow_le_pow_right₀ (le_of_lt hγ) h
660
661/-- For `γ > 1`, `γⁿ < γᵐ ↔ n < m` on `Nat`. -/
662private theorem pow_lt_pow_iff_of_one_lt {γ : ℝ} (hγ : 1 < γ) (n m : Nat) :
663 γ ^ n < γ ^ m ↔ n < m := by
664 constructor
665 · intro h
666 by_contra hle
667 push_neg at hle
668 have := pow_le_pow_right₀ (le_of_lt hγ) hle
669 linarith
670 · intro h
671 exact pow_lt_pow_right₀ hγ h
672
673/-- **Embedding monotonicity (γ > 1)**: the embedding is order-preserving. -/
674theorem embed_le_iff_of_one_lt (γ : Generator) (hγ : 1 < γ.value) (a b : LogicNat) :
675 embed γ a ≤ embed γ b ↔ a ≤ b := by
676 rw [embed_eq_pow, embed_eq_pow, pow_le_pow_iff_of_one_lt hγ, ← LogicNat.toNat_le]
677
678/-- **Embedding strict monotonicity (γ > 1)**. -/
679theorem embed_lt_iff_of_one_lt (γ : Generator) (hγ : 1 < γ.value) (a b : LogicNat) :
680 embed γ a < embed γ b ↔ a < b := by
681 rw [embed_eq_pow, embed_eq_pow, pow_lt_pow_iff_of_one_lt hγ, ← LogicNat.toNat_lt]
682
683/-- **Embedding is strictly monotone for γ > 1**. -/
684theorem embed_strictMono_of_one_lt (γ : Generator) (hγ : 1 < γ.value) :
685 StrictMono (embed γ) :=
686 fun _ _ h => (embed_lt_iff_of_one_lt γ hγ _ _).mpr h
687
688/-! ## Summary
689
690 Law of Logic (four Aristotelian conditions on a comparison operator)
691 ↓ (forces, via Translation Theorem and Aczél)
692 J(x) = ½(x + x⁻¹) − 1 with unique zero at x = 1, positive elsewhere
693 ↓ (the orbit of any γ ≠ 1 under multiplication has Peano shape)
694 LogicNat (zero, succ, induction)
695 ↓ (recovery theorem, this module)
696 Nat with addition and multiplication
697
698The Peano axioms are theorems. Addition and multiplication are forced
699by the orbit structure. No positional representation is assumed. The
700only structural choice is the generator γ ≠ 1, which exists by
701non-triviality of the comparison operator.
702
703What this module establishes is the recovery of the abstract Peano
704structure. What it does not yet establish (left for a follow-up
705module) is:
706
707 - Injectivity of `embed γ` (forced by J-positivity off-identity)
708 - Generator-free characterization of the orbit
709 - Order on `LogicNat` (forced by the cost ordering on the orbit)
710 - Subtraction, division, the rationals, the reals (each requires
711 additional structure on top of the bare orbit)
712
713These extensions follow standard reverse-mathematics templates once
714the Peano structure is in hand.
715-/
716
717end ArithmeticFromLogic
718end Foundation
719end IndisputableMonolith
720