embed
plain-language theorem explainer
The embed definition recursively maps LogicNat, the inductive type of naturals forced by the Law of Logic, into the positive reals by sending the identity constructor to 1 and each step constructor to multiplication by the value of a non-trivial Generator γ. Researchers deriving arithmetic primitives from functional equations cite this construction when realizing abstract orbits as concrete positive-real sequences. The definition is a direct pattern match on the two constructors of LogicNat with no auxiliary lemmas.
Claim. Let γ be a Generator (positive real value ≠ 1). The map embed(γ) : LogicNat → ℝ is defined by embed(γ)(identity) = 1 and embed(γ)(step n) = γ.value ⋅ embed(γ)(n).
background
In the ArithmeticFromLogic module the Law of Logic is treated as a functional equation that forces an inductive type LogicNat whose constructors identity and step mirror the orbit {1, γ, γ², …} inside ℝ₊. A Generator is the structure carrying a positive real value distinct from 1, extracted from the non_trivial witness of SatisfiesLawsOfLogic. The module imports LogicAsFunctionalEquation, so the local setting is the translation of logical comparison into arithmetic operations on positive reals.
proof idea
This is a recursive definition by pattern matching on the constructors of LogicNat. The identity case returns the constant 1; the step case multiplies the generator value by the recursive call. No tactics or lemmas are invoked; the definition itself supplies the required unfolding.
why it matters
Embed supplies the concrete numerical realization of LogicNat that is presupposed by the downstream theorems embed_add (multiplicative homomorphism), embed_eq_pow (identification with γ.value raised to toNat), and embed_injective (distinct LogicNat map to distinct reals). These results in turn feed DomainInstance functors and CoarseGrain constructions. The definition therefore closes the bridge from the abstract orbit forced by the Law of Logic to the positive-real arithmetic used throughout the Recognition framework.
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."