embed_strictMono_of_one_lt
The declaration shows that the orbit embedding of the recovered natural numbers into positive reals is strictly monotone when the generator value exceeds one. Workers reconstructing arithmetic structures from the Law of Logic would reference this result to guarantee order preservation under the embedding. The argument reduces immediately to the right-to-left direction of the companion iff statement for the same embedding.
claimLet $γ$ be a generator with value greater than 1. The embedding map from the Peano structure on the orbit to the positive reals is strictly monotone.
background
Generator denotes a positive real number distinct from 1, extracted from the non-triviality of any comparison operator satisfying the Law of Logic. The embed function maps the identity element of the recovered naturals to 1 and each successor step to multiplication by the generator value, producing the orbit under repeated multiplication. The recovered naturals themselves arise as the abstract Peano structure on the orbit of any such generator, as constructed in the preceding lemmas of this module.
proof idea
The proof is a one-line wrapper that invokes the right-to-left implication of the companion iff lemma on the given strict inequality between embedded values.
why it matters in Recognition Science
This result secures the order-preserving property required for the recovery of natural-number arithmetic from the functional equation. It directly supports the module summary that the Peano axioms become theorems once the orbit structure is in hand. The declaration leaves open the generator-free characterization of the orbit and the direct definition of order on the recovered naturals, both flagged for later modules.
scope and limits
- Does not establish injectivity of the embedding map.
- Does not supply a generator-free description of the orbit.
- Does not introduce an intrinsic order on the recovered naturals.
- Does not construct subtraction or the rationals.
formal statement (Lean)
684theorem embed_strictMono_of_one_lt (γ : Generator) (hγ : 1 < γ.value) :
685 StrictMono (embed γ) :=
proof body
Tactic-mode proof.
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