back
plain-language theorem explainer
The declaration defines the embedding of the natural numbers forced by the Law of Logic into the positive reals, sending each element to successive powers of a non-trivial generator. Researchers reconstructing arithmetic from the recognition cost functional equation cite it to connect the abstract Peano orbit to the multiplicative group of positive reals. The construction is a direct structural definition of the map together with its homomorphism property.
Claim. Let $N$ denote the natural numbers forced by the Law of Logic, with identity element $e$ and successor operation $s$. The structure supplies an embedding $i: N → ℝ₊$ such that $i(e) = 1$ and $i(s(n)) = γ · i(n)$ for any non-trivial generator $γ$, satisfying $i(m · n) = i(m) · i(n)$ where multiplication on $N$ is induced by the successor.
background
The module derives arithmetic primitives from the functional equation satisfied by the recognition cost $J$. The natural numbers forced by the Law of Logic form the smallest subset of positive reals containing the multiplicative identity (zero-cost element) and closed under multiplication by a generator; the two-constructor inductive type mirrors the orbit {1, γ, γ², …}. Upstream results include the multiplicativity theorem for J-automorphisms, which states that any such automorphism preserves multiplication: $f(xy) = f(x)f(y)$, and the definition of the active edge count $A = 1$ that balances the φ-power identity at three spatial dimensions.
proof idea
The structure is defined directly by recursion on the inductive type of the natural numbers forced by the Law of Logic: the identity maps to 1 and each successor applies multiplication by the chosen generator. The multiplicative homomorphism property follows immediately from the multiplicativity of J-automorphisms applied to the generator action.
why it matters
This embedding closes the loop from the abstract logic structure to the concrete multiplicative reals and feeds the uniqueness theorem for the cost function together with the calibration lemma in the functional equation. It supports the T5 J-uniqueness step in the forcing chain by realizing the Peano structure as an orbit under the generator, and appears in downstream results on continuum limits for fluids and mass-to-light derivations. The full chain establishing existence of the generator and injectivity remains open for Level 2.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.