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
depends on (28)
Lean names referenced from this declaration's body.