embed_eq_pow
The theorem equates the recursive orbit embedding of a LogicNat under a generator to the explicit power of the generator value. Researchers deriving arithmetic from the Law of Logic in Recognition Science cite it to identify abstract steps with concrete powers in the positive reals. The proof runs by induction on LogicNat, applying the recursive clause of embed at the successor step and reducing via pow_succ and ring.
claimLet $g > 0$, $g ≠ 1$ be a generator value and let $n$ be an element of the inductive type LogicNat (with constructors identity and step). The orbit embedding satisfies $embed(γ, n) = g^{toNat(n)}$, where $toNat$ converts LogicNat to the ordinary naturals.
background
LogicNat is the inductive type whose constructors mirror the multiplicative orbit {1, γ, γ², …} forced by the Law of Logic: identity is the zero-cost base and step appends one multiplication by the generator. Generator is the structure carrying a positive real value ≠ 1 together with the positivity and nontriviality witnesses. The sibling definition embed is the recursive map sending identity to 1 and step n to γ.value times the image of n. The present theorem supplies the closed-form expression that converts the recursion into ordinary exponentiation.
proof idea
Proof by induction on n. The identity case reduces directly by simp on the definitions of embed and toNat. The successor case rewrites the left-hand side by the inductive hypothesis, replaces the right-hand side by pow_succ, and closes with ring.
why it matters in Recognition Science
The result is invoked by embed_injective (which translates distinct LogicNat elements to distinct orbit points via logarithms) and by the two monotonicity theorems embed_le_iff_of_one_lt and embed_lt_iff_of_one_lt. It therefore completes the concrete identification of LogicNat with the powers of γ, a necessary step before J-positivity arguments can be applied to the orbit and before the arithmetic layer can be lifted into the forcing chain (T5–T8).
scope and limits
- Does not assert existence of any generator.
- Does not extend to zero or negative bases.
- Does not address non-integer exponents.
- Does not derive the Law of Logic itself.
formal statement (Lean)
588theorem embed_eq_pow (γ : Generator) (n : LogicNat) :
589 embed γ n = γ.value ^ (LogicNat.toNat n) := by
proof body
Term-mode proof.
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
607/-- Logarithm of a non-trivial generator is non-zero. -/