 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 =>

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.