embed_injective
plain-language theorem explainer
Distinct elements of the inductive natural-number type map to distinct points under the orbit embedding generated by any non-trivial positive real γ. Workers on realizing the Law of Logic in real-number models cite this result to guarantee faithful representation of abstract numbers. The argument reduces equality of embedded values to equality of exponents by taking logarithms and canceling the nonzero factor log γ.
Claim. Let γ be a positive real not equal to one. The map from the inductive natural numbers (built from an identity element and a successor step) to the positive reals, sending the identity to 1 and each successor step to multiplication by γ, is injective.
background
The Generator structure consists of a positive real value distinct from one, extracted from the non-triviality condition in the Law of Logic. The inductive type of natural numbers is the smallest set containing the identity and closed under the step operation, corresponding to the orbit under multiplication by the generator. The embedding function is defined recursively to realize this orbit in the positive reals.
proof idea
The tactic proof assumes two logic naturals map to the same real under the embedding. It rewrites both sides using the power equivalence, takes the real logarithm of both sides, cancels the common nonzero multiplier log of the generator value, casts the resulting equality back to natural numbers, and applies the round-trip property of fromNat and toNat to recover equality of the original elements.
why it matters
This result is invoked by the injectivity theorem for the positive-ratio orbit interpretation in the LogicRealization module. It completes the demonstration that the abstract Peano structure forced by the Law of Logic embeds injectively into the multiplicative group of positive reals. Within the Recognition Science framework, the construction supports the transition from the abstract forcing chain to concrete numerical realizations used in mass and astrophysical derivations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.
papers checked against this theorem (showing 30 of 485)
-
Rectifying curves preserve normal component under homothetic maps
"α(s) = ξ(s) t(s) + μ(s) b(s) (rectifying condition)"
-
Algorithm draws any DAG in k dimensions where k ≤ n/2
"Lemma 2. The minimum size of a channel decomposition of G is equal to the width w_G of G."
-
Tensor networks extended to continuous 2D and higher
"the continuous extensions of tensor networks maintain ... expressiveness ... invariance under gauge transformations"
-
Smart contracts generate public random numbers no one can control
"Our contract eliminates the ability of a producer to predict or control the generated random numbers, including the stored history of random numbers. ... Merlin chain ... Vx = SHA3(Vx+1)"
-
Strategies shroud their identities until n-1 actions revealed
"Minimal Nonfaces as Informative Attribute Release Sequences... Lemma 1"
-
Thermalization holds without stochasticity in Hamiltonian systems
"the deterministic entropy Sd... dSd ≡ DN dJ/J... the entropy of a dynamical system is its adiabatic invariant."
-
One-to-one codes bound mismatch cost by divergence
"the cost of mismatch vanishes if and only if ν lies on the tilted family of the true distribution μ"
-
Cubic partition counts obey congruences mod powers of 3
"Theorem 1.1 … a3(3^{2α}n + (3^{2α}-1)/4) ≡ 0 (mod 3^α) … proved via the matrix recurrence (2.19) and valuation bounds (4.1)–(4.5)"
-
200 ms sampling leaves legged balance error unchanged
"Z = ⊕_{i=0}^∞ (A+BK)^i B W, ˜p ∈ KZ ⊕ W, Jury stability triangle for q1,q2"
-
Mailbox encapsulation measures cognitive value shifts in data transmission
"mailbox theory ... encapsulating the information as a mailbox ... cognition is continuously implemented during the transmission process"
-
Forest counts in circulant graphs equal p a(n)^2
"f_G(n)=p a(n)^2 with p depending on parity of n; Chebyshev roots of ∑(2T_{s_j}(w)−2)=1"
-
One LLM internalizes reasoning by posing, solving, and judging itself
"ALIVE unifies problem posing, solving, and judging within a single policy model to internalize the logic of correctness. By coupling adversarial learning with instructive verbal feedback..."
-
Agents evolve image generation by distilling trajectory differences
"LGenEvolve = LGRPO + λSDL LSDL with importance-weighted sampled-token reverse-KL"
-
Attributes replace category lists for remote sensing pre-training
"Random Shuffling... Random Dropout... approximates sampling from the attribute power set... Attribute Replacement... hard antagonist from the same dimension"
-
r-value scores shrink conformal sets by excluding unstable candidates
"the r-value estimates how likely a candidate’s latent score belongs to the top-ranked group after accounting for both its mean score and its uncertainty"
-
VLMs fail to ground numbers in spatial layouts
"current VLMs rely heavily on shallow spatial cues, struggle to build stable coordinate-aware representations"
-
Bipolar ramp loss beats MRT on weak seq2seq tasks
"τ+m,j = 0 if y+m,j ∈ y− else 1; τ−m,j = 0 if y−m,j ∈ y+ else −1 (token-level sign flips that leave shared tokens untouched)"
-
Generative edits answer what-if questions for neural net predictions
"We use both of these formulations in our framework depending on whether actionable attributes are known or unknown, where the latter uses the latent representations as our attributes (§3.1)"
-
Niemeier lattice theta series obey congruences
"Theorem 2.1 (Böcherer–Nagaoka) and application of Θ operator to Leech lattice theta series"
-
Gravitational radiation produces vorticity tied to super-energy flux
"the vorticity vector Ω... super-Poynting vector Pα = ηαβγδ Eβρ Hγρ uδ... non-vanishing component of the latter associated to a state of gravitational radiation"
-
Three views explain information flow and loss in distributed systems
"Theorem 1 (Observability of X at S by R): ... π+ : Si +Xi→ Rj, π− : Rj −Xj→ Si, Xj ⊆ Xi"
-
Upper bound derived for radar interference from massive MIMO cells
"While these worst-case elevation angles are correlated for neighboring BSs due to the structure of the PV tessellation, it does not explicitly appear in our analysis because of our focus on the average interference."
-
Sum of fractional-part differences ~ (2/π)ζ(3/2) sqrt(c x)
"van der Corput estimates on {x/k−a}−{x/k−b}"
-
Explicit solutions derived for Levi-Civita equation on monoids
"Proposition 1.1 … any set of distinct nonzero multiplicative functions is linearly independent"
-
ChebNets stabilize deep RePU nets via Chebyshev series
"Theorem 1. For n ≥ 1, assume p(x) = ∑ cj Tj(x) ... there exists a σ2 neural network with at most ⌊log2 n⌋ + 1 hidden layers ... O(n) neurons and total non-zero weights."
-
P-adic valuation increments get independent arithmetic
"The arithmetic of the p-adic increments is proposed... Δv_p(n!)=(1-Δs_p(n))/(p-1)... Δs_p(n)=1-(p-1)v_p(n+1)"
-
Sensitivity decays exponentially with distance in graph NLPs
"graph-induced bandwidth ... inverse of a graph-induced banded matrix (Theorem 3.6)"
-
Spin fluctuations create residual resistivity linked to Tc in heavy fermions
"A(ℓ) = F²_ℓ |λ(ℓ)–μ*/(1+λ(ℓ))|² and Tc(ℓ)=θ exp(–1–λ(ℓ))/(λ(ℓ)–μ*)"
-
Perturbation in doping parameters solves Hubbard sign problem
"The first order for the vertex in particle-hole (PH) channel is given by the diagram shown in Fig.7 ˜Σ(1)12 = −∑s−QMC ∑3,4 γd1234(s) ˜G034"
-
Listwise model with boosted trees tops review helpfulness benchmarks
"Theorem 4 … E(f listD) ≤ E(f pairD)"