pith. machine review for the scientific record. sign in
theorem

embed_add

proved
show as:
view math explainer →
module
IndisputableMonolith.Foundation.ArithmeticFromLogic
domain
Foundation
line
576 · github
papers citing
22 papers (below)

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Foundation.ArithmeticFromLogic on GitHub at line 576.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

formal source

 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