embed_injective
The embedding of LogicNat into the positive reals via repeated multiplication by a generator γ is injective. Researchers deriving arithmetic from the Law of Logic cite this to confirm distinct abstract numbers map to distinct orbit points. The tactic proof reduces the claim to power equality via embed_eq_pow, applies logarithms with cancellation from log_generator_ne_zero, then lifts the resulting Nat equality back through fromNat_toNat.
claimLet γ be a generator (a positive real ≠1). The orbit map embed γ : LogicNat → ℝ, defined recursively by embed γ (identity) = 1 and embed γ (step n) = γ ⋅ (embed γ n), is injective.
background
In ArithmeticFromLogic, LogicNat is the inductive type with constructors identity (zero-cost base) and step (one iteration of the generator), mirroring the orbit {1, γ, γ², …} as the smallest subset of ℝ₊ closed under multiplication by γ and containing 1. A Generator is any positive real value other than 1, extracted from the non_trivial field of SatisfiesLawsOfLogic. The embed function realizes this orbit explicitly in the positive reals.
proof idea
The tactic proof intros a b with hab, rewrites both sides via embed_eq_pow to obtain γ.value^(toNat a) = γ.value^(toNat b), applies congrArg Real.log, rewrites with Real.log_pow, obtains log_generator_ne_zero γ to cancel the nonzero factor via mul_right_cancel₀, casts the resulting real equality to Nat equality, then applies congrArg LogicNat.fromNat and simplifies with fromNat_toNat to conclude a = b.
why it matters in Recognition Science
This result is invoked by positiveRatio_interpret_injective in LogicRealization to establish injectivity of the continuous positive-ratio orbit interpretation. It closes the bridge from the abstract Peano structure of LogicNat to the concrete multiplicative orbit in ℝ₊, completing a key step in the forcing chain from the Law of Logic to arithmetic. The theorem supports the Recognition Science derivation of natural numbers directly from the functional equation without prior set-theoretic assumptions.
scope and limits
- Does not prove surjectivity onto all positive reals.
- Does not apply when the generator value equals 1 or is non-positive.
- Does not establish order preservation or monotonicity.
- Does not address embeddings into structures other than ℝ₊.
formal statement (Lean)
620theorem embed_injective (γ : Generator) : Function.Injective (embed γ) := by
proof body
Tactic-mode proof.
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`. -/