embed_pos
plain-language theorem explainer
Embed_pos asserts that the recursive embedding of any LogicNat element into the positive reals under a Generator is strictly positive. Researchers deriving arithmetic from the Law of Logic in Recognition Science cite it to guarantee that orbit elements remain in ℝ₊. The proof proceeds by induction on the two constructors of LogicNat, invoking one_pos on the identity case and mul_pos on the step case using the generator's positivity.
Claim. Let $γ$ be a Generator (a real $γ > 0$ with $γ ≠ 1$) and let $n$ be an element of LogicNat (the inductive type with constructors identity and step). Then $0 < embed(γ, n)$, where $embed(γ, identity) = 1$ and $embed(γ, step n) = γ · embed(γ, n)$.
background
Generator is the structure with fields value : ℝ, pos : 0 < value, and nontrivial : value ≠ 1; it is extracted from any comparison operator satisfying the Law of Logic. LogicNat is the inductive type whose identity constructor stands for the multiplicative identity 1 and whose step constructor iterates multiplication by the generator value, thereby realizing the orbit {1, γ, γ², …} inside ℝ₊. The embed function is the recursive map sending identity to 1 and step n to γ.value times the image of n.
proof idea
The proof is by induction on n. The identity case applies the lemma one_pos. The step case rewrites the target as γ.value * embed γ n and closes with mul_pos applied to γ.pos and the induction hypothesis.
why it matters
The result secures positivity of the orbit embedding, a prerequisite for the multiplicative homomorphism between LogicNat and ℝ₊ that the module doc-comment identifies as the structural fact that LogicNat is the orbit. It supplies the positivity needed for constructions that embed this arithmetic into HamiltonianEmergence and ObserverForcing. In the Recognition framework it anchors the positive reals required for the J-function and the phi-ladder before the forcing chain reaches T5–T8.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.