pith. sign in
theorem

embed_eq_pow

proved
show as:
module
IndisputableMonolith.Foundation.ArithmeticFromLogic
domain
Foundation
line
588 · github
papers citing
42 papers (below)

plain-language theorem explainer

The theorem equates the recursive orbit embedding of a LogicNat element under a generator to the explicit power of the generator value. Foundation researchers constructing arithmetic from the Law of Logic cite this to identify the abstract inductive type with concrete powers in the positive reals. The proof is a direct induction on the LogicNat constructors that reduces the successor step via the embed recursion and the power successor identity.

Claim. Let $γ$ be a generator (positive real value not equal to 1) and let $n$ be an element of LogicNat. Then the embedding satisfies $embed(γ, n) = γ.value^{toNat(n)}$, where $embed$ sends the identity constructor to 1 and each successor step to multiplication by $γ.value$.

background

The module constructs natural numbers and arithmetic from the Law of Logic. LogicNat is the inductive type with constructors identity (zero-cost element) and step (one further iteration of the generator), mirroring the orbit {1, γ, γ², …} as the smallest subset of positive reals closed under multiplication by γ and containing 1. A Generator is the structure with fields value : ℝ, pos : 0 < value, and nontrivial : value ≠ 1, whose existence follows from the non_trivial field of SatisfiesLawsOfLogic. The embed function is the recursive map defined by embed γ identity = 1 and embed γ (step n) = γ.value * embed γ n.

proof idea

The proof proceeds by induction on n. The identity case simplifies immediately by the definitions of embed and LogicNat.toNat. The step case rewrites the left-hand side using the inductive hypothesis, replaces the right-hand side via the power successor lemma pow_succ, and closes the equality with the ring tactic.

why it matters

This result is invoked by embed_injective to translate distinct LogicNat elements into distinct powers before taking logarithms, and by embed_le_iff_of_one_lt and embed_lt_iff_of_one_lt to reduce order comparisons on the orbit to the natural-number order via power inequalities. It supplies the explicit power representation that bridges the abstract LogicNat forced by the Law of Logic to the concrete multiplicative orbit, supporting the arithmetic layer of the Recognition framework.

Switch to Lean above to see the machine-checked source, dependencies, and usage graph.

papers checked against this theorem (showing 30 of 42)

The full set is indexed internally; the public theorem page shows a capped sample so high-use declarations do not become many-thousand-row pages.