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 170)
-
Angular momentum rule boosts pion yields in collisions
"rigorous angular momentum conservation (AMC) in elastic, inelastic, and decay channels"
-
Zipped Y-notch is lowest energy at surface triple junctions
"metastable core shift structures can be obtained only when the core-shift times for the ABC stacking unit above is the same as that below or 1 more than that below... total numbers... 2^(csd/3)-1"
-
Cohomology of relative fundamental groups interprets Gauss-Manin connections
"Theorem 1 ... all maps in it are isomorphisms. ... The Gauss-Manin connection on H^i_dR(X/S, (V,∇/S)) corresponds to the action of Π(S/k) on H^i(π_geom(X/S),V) induced from the Lyndon-Hochschild-Serre sequence."
-
Single-turn anchors fix multi-turn LLM failures
"We term the root cause as Contextual Inertia... over 70%–90% of multi-turn errors traced to propagation of previous responses"
-
iFID predicts diffusion gFID at 0.85 correlation
"diffusion models generate novel samples by interpolating between training data and iFID measures the validity of these interpolated samples."
-
Tilted sum for Markov sources reduces to affine occupation count
"transfer-matrix representation of the cumulant generating function"
-
Cached skeletons speed NL-to-DSL conversion 3.6x
"an online, entity-agnostic embedding model trained via contrastive learning for robust matching"
-
Exact text histories allow precise credit in LLM agent teams
"fixed continuation distribution Db ... QDb(h, a) ≜ EDb[R|h, a]"
-
Geometric simplex method works in locally convex spaces
"We show that our definition of polytopes captures optimization over the Hilbert cube"
-
Pass-rate weighting raises math LLM scores by up to 8 points
"Under power-law regularity at the boundaries (Assumption 3(b)), any such SNR profile decomposes as p^{a'}(1-p)^{b'}·e^r(p) with bounded remainder (Proposition 2)."
-
LLMs agree moderately on APIs but diverge on open tasks
"We measure pairwise and group-level agreement using set-, rank-, and consensus-based metrics including Average Overlap, Jaccard similarity, Rank-Biased Overlap, Kendall's tau, Kendall's W, and Cronbach's alpha."
-
Autoregressive expert keeps history for smoother robot actions
"Dynamic Temporal Re-anchoring (DTR)... assigns fixed index n corresponding to the timestep when the image was captured... Score(q_m, k_VL_n) = q^T R(m-n) k_VL"
-
Dehn twist conjugacy on three-point disk solved via torus homology
"Theorem 1.1. Any Dehn twist tγ … is conjugate to tc, td, or te … in terms of Dynnikov coordinates (a,b) of γ: tγ conjugate to te if b even, …"
-
Inner products of spectral embeddings yield gauge-invariant graph operators
"gauge invariance guarantees discretization-invariant learning with bounded discretization mismatch error"
-
Partition logic translates to Prolog rules that generate visual forms
"We connect partition logic with Generative Logic by translating finite partition logics into Prolog-based Simple Generative Logic Grammars... the grammar GL constructed from Eqs.(17)–(19) preserves the incidence relation between atoms and two-valued states."
-
Learned user embeddings personalize text-to-image outputs
"When user data are scarce, new users are represented as linear combinations of existing preference embeddings learned during training"
-
Almost all n obey ||n|| ≤ C_avg log n + o(log n)
"C ≤ (1/b log b) ∑_{r=0}^{b-1} D(b,r) for any b≥2"
-
Non-centered objective stabilizes SPL representations at high UTD
"non-centered inner product form ... LRR = 1/d(d-1) Σ i≠j ([C(Z)]ij)^2 where [C(Z)]ij = 1/(N-1) Σ zb,i zb,j"
-
Shared encoder cuts variance in multi-policy causal estimates
"The encoder is trained using kernel mean embeddings, ensuring that the learned representation space reflects population-level policy dissimilarities."
-
Exact prefix factorization removes errors in diffusion language models
"Theorem 1 (Exact joint law). Under Eq. 5, the sequence produced by FeF-DLLM satisfies Pr(ˆX0,Jt=xJt|Xt,t)=∏p⋆(Xjm0=xjm|X≥jm t,x<jm0,t)=p⋆(xJt|Xt,t)."
-
Predictive Inference via Kernel Density Estimates
"Theorem 1 (Weak convergence for KDE process). Suppose 0 < hn ≤ C n^−δ ... Then P(Pn ⇀ P) = 1 ... supported on a (random) compact set V"
-
Opinions steer epidemics through graphon kinetics
"The resulting Fokker–Planck model associated with (2.18) reads ∂tfJ(x,w,t)=1/τ ∑ QJ(fJ,fH)(x,w,t)"
-
3B continuous critic outperforms 7B binary GUI models
"Functional Equivalence Hypothesis... instruction I and optimal action a* are two forms of the same underlying GUI Affordance"
-
Directed graphs gain higher-order Q-analysis via clique complexes
"Definition 6.8. ... (•)-q-connected ... directed (•)-q-chain"
-
Bounds derived for logarithmic coefficients of univalent inverses
"From the inequality (7), when x_{2p-1}=0 and p=3,4,… we have |ω11 x1 + ω31 x3|² + … ≤ |x1|² + |x3|²/3"
-
Higher-order graphs capture multiway and temporal interactions
"Superhypergraphs extend higher-order network models by allowing the vertex domain itself to be hierarchical... iterated powerset constructions"
-
Non-Hermiticity alone triggers qubit entanglement jump
"SVD generalized density matrix ρ_SVD=√(ρ†ρ)/Tr√(ρ†ρ) for bi-orthogonal entanglement"
-
Two types classify all maximal symmetry models in CR dimension 1
"Proposition 2. A graded nilpotent Lie algebra with reduced growth vector (2,1,1,…) is either Goursat … or … (5)"
-
2SLS captures total reallocation effects in rationed programs
"Assumption 2 (Ranking-list refill)... instrument and policy operate on same margin"
-
Hidden states flag when reasoning models begin overthinking
"token-level supervision anchored at the first correct solution"