theorem
proved
embed_injective
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.Foundation.ArithmeticFromLogic on GitHub at line 620.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
-
of -
via -
back -
embed -
embed_eq_pow -
fromNat -
fromNat_toNat -
Generator -
log_generator_ne_zero -
LogicNat -
toNat -
of -
embed -
is -
of -
from -
is -
of -
is -
of -
fromNat -
is -
and -
value
used by
formal source
617/-- **Embedding injectivity**: distinct natural numbers map to distinct
618points in the orbit. This closes the bridge from the abstract `LogicNat`
619to the concrete orbit `{1, γ, γ², ...}` in ℝ₊. -/
620theorem embed_injective (γ : Generator) : Function.Injective (embed γ) := by
621 intro a b hab
622 -- Translate to powers.
623 rw [embed_eq_pow, embed_eq_pow] at hab
624 -- Take logs.
625 have hpos_a : 0 < γ.value ^ (LogicNat.toNat a) := pow_pos γ.pos _
626 have hpos_b : 0 < γ.value ^ (LogicNat.toNat b) := pow_pos γ.pos _
627 have hlog : Real.log (γ.value ^ (LogicNat.toNat a))
628 = Real.log (γ.value ^ (LogicNat.toNat b)) := by
629 exact congrArg Real.log hab
630 rw [Real.log_pow, Real.log_pow] at hlog
631 -- Cancel the non-zero log γ.value.
632 have hne := log_generator_ne_zero γ
633 have hcast : ((LogicNat.toNat a : ℝ)) = ((LogicNat.toNat b : ℝ)) := by
634 have := mul_right_cancel₀ hne hlog
635 exact this
636 have h_nat : LogicNat.toNat a = LogicNat.toNat b := by exact_mod_cast hcast
637 -- Lift back to LogicNat via the equivalence.
638 have := congrArg LogicNat.fromNat h_nat
639 rw [LogicNat.fromNat_toNat, LogicNat.fromNat_toNat] at this
640 exact this
641
642/-! ## Order via the Embedding (γ > 1 case)
643
644When `γ > 1`, the orbit is strictly increasing under multiplication
645by `γ`, and `embed γ` is a strictly monotone embedding of the Peano
646order on `LogicNat` into `(ℝ, ≤)`. This is the analytic counterpart
647of the abstract Peano order from Section 5b. -/
648
649/-- For `γ > 1`, `γⁿ ≤ γᵐ ↔ n ≤ m` on `Nat`. -/
650private theorem pow_le_pow_iff_of_one_lt {γ : ℝ} (hγ : 1 < γ) (n m : Nat) :
papers checked against this theorem (showing 30 of 139)
-
Filtration on automorphic functions transfers from spectral support
"Conjecture 2.1.5: Tr(Frob, IndCoh_O(LS_restr)) is concentrated in degree 0 ... Ramanujan-Arthur over Q_ℓ (Conjecture 3.4.6)"
-
Modal exchangeability decomposes Kripke frames into orbit-directed credal measures
"The orbit decomposition of the centered symmetry group governs the within-orbit structure: worlds in the same orbit are conditionally identically distributed, and on orbits satisfying a richness condition and countable infinitude they are conditionally i.i.d. given a rigid orbit-specific directing measure."
-
AI use stabilizes emotions and focuses developers on code verification
"Developers retrospectively labeled their self-reported intentions, tool-supported actions, and emotions from screen recordings"
-
Rank of hypergraph tightens bound on Berge k-factors
"incidence graph B(X,Y) … parity(g,f)-factor … discharging rules (i)–(iv)"
-
Two agents invent numbers to handle unseen visual cases
"two agents, without prior mathematical knowledge, can develop a shared symbolic protocol to solve a visually grounded task where the use of a numerical system facilitates extrapolation"
-
Normalization creates point identification unless parameter is class-constant
"A counterfactual parameter is normalization-free if and only if it is constant on equivalence classes; otherwise any point identification is created by the normalization rather than by the model."
-
SCOLAR extends vision-language latent reasoning 30 times
"Information Gain Collapse—autoregressive generation makes each step highly dependent on prior outputs"
-
Chemical order sets rigidity threshold at coordination 2.4
"The Maxwell count is fM(⟨r⟩)=6−5⟨r⟩/2... GRC fraction S∞=α[1−(u*)³]"
-
Horizontal currents in Heisenberg group decompose via Smirnov
"Theorem 5.1. For every ℓ > 0 and every horizontal charge μ ... there is a finite positive measure ν on K_ℓ with μ = ∫ [γ] dν(γ)"
-
Spectral gap in updates controls neural training transitions
"k*=argmax σj/σj+1 ... gap ratio R(t)=σk*/σk*+1"
-
2D grid turns multiplication into local 3x3 steps
"a neural cellular automaton with only 321 learnable parameters achieves perfect length generalization"
-
LTL with data reduces to standard LTL+P synthesis
"By theorem 1, any formula ϕ(¯x) with k free variables can be encoded as a finite set of types. ... M |= ϕ(¯a) iff tp(¯a) ∈ ι(ϕ)"
-
Lattice Gauging Interfaces and Noninvertible Defects in Higher Dimensions
"the topological nature of gauging interfaces is obscured by the fact that the constrained Hilbert space depends on the location of the interface"
-
Phase rotations on unit circle stabilize explicit memory
"Mt = (Mt−1 + ΔM) (mod 2π)... |eiθ| ≡ 1 regardless of sequence length"
-
Switching successor measures enable hierarchical zero-shot RL
"Corollary 1. A^{π_w→π}_s(r) = V^{π_w}(s;r) + [M^{π_w}_s(w)/M^{π_w}_w(w)] (V^π(w;r) − V^{π_w}(w;r)) − V^π(s;r)."
-
One LLM generates and ranks candidates via phase-factorized policy optimization
"Factorized credit assignment... phase-specific gradient weighting"
-
Language thresholds lift F1 by 2-5% in multilingual slur detection
"Data augmentation via GPT-4o-mini back-translation to alternate languages effectively tripled the training corpus while preserving semantic content and class distribution ratios."
-
Metrics predict reasoning data utility before training
"Redundancy Ratio: Information density calculated as (1 - len_compressed / len_original)"
-
Anchored memory rules boost realism in LLM social simulations
"four-namespace memory system (episodic, semantic, reflection, working) … anchor update strategies: EMA, Retrieval, Hybrid"
-
3-torsion fields solve cyclotomic Galois embedding problems infinitely often
"Theorem 4.1 … Galois embedding problem … solvable iff K is the splitting field of the 3-division polynomial of an elliptic curve E/Q"
-
Library builds O(m) circuits for ten quantum amplitude patterns
"Walsh functions... correspondence between Walsh series and diagonal operator compilation"
-
Predefined vectors cut million-class NN prediction to constant time
"if NN latent space geometry is known and possesses specific properties, label prediction complexity can be significantly reduced... by associating label prediction with the O(1) complexity closest cluster center search in a vector system used as target for latent space configuration (LSC)... finding indexes of several largest and lowest values in the embedding vector"
-
LLMs hold memories in entangled states needing active suppression
"letter alignment and inter-class decodability persist into the network and are gradually suppressed across layers... memory representations are initially overlapping, become more separated through the middle... target alignment... rises sharply near the end"
-
Screening matches Transformer loss with 30% fewer parameters
"the screening unit can also represent the absence of relevant context"
-
Self-prior lets simulated infant pass mirror mark test
"the self-prior captures visual–proprioceptive associations, functioning as a probabilistic body schema"
-
Agents build complex skills via co-evolving verifier
"The Surrogate Verifier... operates in a completely independent LLM session... information isolation ensures that the verifier’s test generation is conditionally independent of the generator’s internal state"
-
Framework lets models pick dataset targets with no training
"manifold complexity itself functions as an implicit supervisory signal—enabling single-neuron ANNs to distinguish correct mappings without pretraining"
-
Vision suppresses audio in AVLLM final outputs on conflicts
"We observe that these decoded tokens meaningfully capture sound sources... meaningful audio information emerging in the last 5 layers"
-
RLSD splits self-distillation to lift LLM convergence ceiling
"the signals governing update direction and update magnitude have asymmetric requirements: the directional signal can be sparse but must be reliable ... the magnitude signal ... benefits from being as dense as possible"
-
Max-entropy sampling raises diversity in citizen panels
"Theorem 3.3. ... samples a panel uniformly from the set of all panels."