embed
plain-language theorem explainer
The embed definition recursively maps the LogicNat inductive type (identity and step constructors) to positive reals by repeated multiplication with a Generator value, returning 1 at the identity. Researchers deriving arithmetic from the Law of Logic cite it to establish the concrete orbit structure in reals. The definition is given directly by pattern matching on the two constructors of LogicNat.
Claim. Let $γ$ be a Generator (positive real value $γ ≠ 1$). The embedding $e_γ : LogicNat → ℝ_{>0}$ satisfies $e_γ(identity) = 1$ and $e_γ(step n) = γ · e_γ(n)$.
background
LogicNat is the inductive type whose identity constructor represents the zero-cost multiplicative identity and whose step constructor represents iteration under a generator; its two-constructor form mirrors the orbit {1, γ, γ², …} as the smallest subset of positive reals closed under multiplication by γ and containing 1. A Generator is the structure carrying a positive real value distinct from 1, extracted from the non_trivial witness of SatisfiesLawsOfLogic. The definition appears in ArithmeticFromLogic, the module that constructs natural-number arithmetic directly from the functional equation of logic; it depends on the local Generator and LogicNat declarations together with the upstream step operation from CellularAutomata.
proof idea
The declaration is the recursive definition itself, written by pattern matching on the constructors of LogicNat: the identity case returns the constant 1 and the step case multiplies the generator value by the recursive embedding of the predecessor.
why it matters
Embed supplies the concrete map required by the downstream theorems embed_add (multiplicative homomorphism), embed_eq_pow (power representation), and embed_injective (distinct naturals map to distinct orbit points). It therefore completes the passage from the abstract LogicNat forced by the Law of Logic to the positive reals, enabling the RecognitionCategory DomainInstance functor and the CoarseGrain Riemann-sum construction in the classical bridge.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.
papers checked against this theorem (showing 8 of 8)
-
Cluster algebras perturb the Alexander polynomial for knots
"Theorem 6.13... Δ_K(T^2) .= det B̂(T)"
-
Mathematics builds from zero and one as absence and presence
"we postulate that 0 and 1 can be primitive objects... the Binary Principle: mathematics is the universal language of absence or presence of an abstract unit... Constructing Numbers Without Successor"
-
Heartbeat mechanism lets LLM agents learn their own thinking schedule
"state evolution s_{t+1} = F(s_t, d_t; Theta); macro/micro state machine; LogicNat-like orbit of activities"
-
Recursive simulator captures ring-down in fast cavity crossings
"recursive formulation of the intracavity electric field as a sum over round trips... sampling frequency... internally adjusted... consistent with the cavity round-trip structure"
-
Decoupled streams model timing mismatches in agent actions
"We define an Engagement Process (EP) over a discrete sequence of ticks T={0,1,2,…}. … actions and observations as decoupled event streams … Yt and At need not be paired."
-
Discrete linear systems as time group representations
"a linear system naturally gives rise to the map ρ: Z → GL(R^n), t ↦ A^t ... equivalent to giving V the structure of a left k[G]-module ... when G = Z/TZ, k[G] ≅ k[x]/(x^T − 1)"
-
CDF charts turn averaging linear and recover Kolmogorov means
"E_G(X) := G⁻¹(E[G(X)]) ... transporting the distribution to probability space, performing linear averaging there, and pulling back to value space."
-
Multidimensional cost geometry
"Affine geodesics on M_t are straight lines in log-coordinates, globally defined; on M_x they are restricted by xᵢ > 0."