theorem
proved
embed_injective
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
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 197)
-
Coupled-cluster ansatz works for any reference determinant
"ΔCC reduces to single-reference CC for M=1; size-extensive via cancellation of unlinked diagrams after C-condition"
-
Metropolis samplers gain explicit gaps on non-smooth targets
"Lemma 4.1, 4.4, 4.5: close-coupling via acceptance probability and Gaussian proposals under non-smooth composite potential"
-
DP training correlates noise only with prior step to cut memory
"sensk,b(C) = || sum_{j=0}^{k-1} C[:, jb+1] ||_2 for lower-triangular Toeplitz C"
-
Test-time scaling samples optimal RL policies without training
"TV(q(x0|y)∥p(x0|y)) ≤ I(2ϵ + h(ϵ,M,λ,D)/(C−ϵ−h)) + Iϵ = Õ(I/√M + Iϵ)"
-
Perturbation sensitivity detects uncertain steps in LLM reasoning
"Pert.(xt) = Var_Δ [P̃_Δ(xt)]"
-
Framework unifies cavity, circuit and spin axion detectors
"axion quality factor Qa ≡ (c/v)^2 ... coherence time τa ≈ Qa/νa ... stochastic lineshape"
-
Action replacement lifts BC performance ceiling in offline RL
"Theorem 3.2 (Instability via Policy Divergence) ... min L(Q) ≥ μ·E[∥πθ(s′)−πβ(s′)∥²]"
-
LLM agents fix code issues at the same rate with or without writing tests
"value-revealing prints consistently outnumber assertions"
-
Posterior-deterministic POMDPs make reachability approximable
"support end component (SEC)... Reachf(S) ... maximal SECs"
-
1965 model full solution matches RT spike-bubble asymmetry
"to leading order, RT mixing is governed by the competing dynamics between diffusion of ln ρ-bar and mass conservation"
-
Symmetry spans enforce gaplessness without anomalies
"i*_C TQFT(C) ∩ i*_(ϕ,β) TQFT(Vect G) ≠ {0}"
-
Tight detection thresholds derived for masked bipartite latent graphs
"Λ_α(X_R) := (-1)^ℓ / (2^ℓ ℓ!) ∑ ... ∏ (1/d <x_rj(1), x_rj(2)> - bσ² I) ⋅ ∏ φ^(s_e-1)(τ)"
-
Graph topology directs token allocation in multimodal RAG
"Graph-Guided Policy Optimization ... pruning memory nodes associated with redundant actions ... critical path from the root to the answer node"
-
Test-time fix curbs hubness in video-text retrieval
"query shifts amplify the hubness phenomenon"
-
Two obstruction maps decide transversal diagonal gates in CSS codes
"V^{(m)}_{LD} ≅ H^1(C;Z_2) ⊗_H S_m with S_m = ⊕_{ν=1}^m 2^{ν-1} (ker H_Z)⊗_H^{(ν-1)}"
-
Linear surrogates unify non-convex optimization beyond DR-submodular
"Restrict to maximal convex subset K* = conv(K_m) away from origin to bound α away from 0 (Corollary 6, Remark 10)"
-
Recommenders bootstrap performance from their own generated data
"recursive error bound E(θk+1)≤(1−λ)E0+λ[(1−p̃k)ρE(θk)+p̃kEmax] (Eq. 7)"
-
Entropy affects only variance in Bayesian portfolio control
"Posterior dynamics dm_t = P_t dŴ_t, dP_t = −P_t² dt independent of policy; entropy regularization orthogonal to learning."
-
Rough common noise in LQ mean-field games yields unique FBSDE solutions
"A novel Volterra-type (or mild) formulation allows to keep technical (rough-stochastic) consideration to a minimum."
-
Models mistake attacker text for trusted instructions by judging style over source
"the degree of role confusion strongly predicts attack success even before generation"
-
Polynomial root decides if vectors admit equal-angle sectors
"Corollary 1 … root among the divisors of its constant term … rational root theorem"
-
Sim-trained tactile policy works zero-shot on real robot
"unifying both domains through a shared deform map representation"
-
Block quadrifocal tensor has fixed multilinear rank (4,4,4,4)
"Theorem 3.1. ... Q_n = G_Q ×1 C ×2 C ×3 C ×4 C ... mlrank(Q_n)=(4,4,4,4)"
-
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"