theorem
proved
embed_strictMono_of_one_lt
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Foundation.ArithmeticFromLogic on GitHub at line 684.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
formal source
681 rw [embed_eq_pow, embed_eq_pow, pow_lt_pow_iff_of_one_lt hγ, ← LogicNat.toNat_lt]
682
683/-- **Embedding is strictly monotone for γ > 1**. -/
684theorem embed_strictMono_of_one_lt (γ : Generator) (hγ : 1 < γ.value) :
685 StrictMono (embed γ) :=
686 fun _ _ h => (embed_lt_iff_of_one_lt γ hγ _ _).mpr h
687
688/-! ## Summary
689
690 Law of Logic (four Aristotelian conditions on a comparison operator)
691 ↓ (forces, via Translation Theorem and Aczél)
692 J(x) = ½(x + x⁻¹) − 1 with unique zero at x = 1, positive elsewhere
693 ↓ (the orbit of any γ ≠ 1 under multiplication has Peano shape)
694 LogicNat (zero, succ, induction)
695 ↓ (recovery theorem, this module)
696 Nat with addition and multiplication
697
698The Peano axioms are theorems. Addition and multiplication are forced
699by the orbit structure. No positional representation is assumed. The
700only structural choice is the generator γ ≠ 1, which exists by
701non-triviality of the comparison operator.
702
703What this module establishes is the recovery of the abstract Peano
704structure. What it does not yet establish (left for a follow-up
705module) is:
706
707 - Injectivity of `embed γ` (forced by J-positivity off-identity)
708 - Generator-free characterization of the orbit
709 - Order on `LogicNat` (forced by the cost ordering on the orbit)
710 - Subtraction, division, the rationals, the reals (each requires
711 additional structure on top of the bare orbit)
712
713These extensions follow standard reverse-mathematics templates once
714the Peano structure is in hand.
papers checked against this theorem (showing 30 of 174)
-
Deep agents retrieve only 21% of expert-cited papers
"Sem-Path ... order-preserving minimum-cost alignment ... 1/(1+J_d)"
-
Categorizing attention heads speeds long-context LLM decoding by 3x
"temporal heterogeneity... intralayer redundancy... overlap coefficient O(K(X),K(Y))... Greedy Star Clustering"
-
New attention method yields 99% zeros without sinks
"TRA is non-dispersive ... TDA controls the expected number of spurious survivors per row to O(1)"
-
Quantile-winsorized max-test matches standard power
"Gaussian approximation (8) and (16) equating power of arithmetic-mean and winsorized max-tests to P(‖Σ_0^{1/2}Z + √n D^{-1}μ‖_∞ > c_{n,1-α})"
-
Hat tile constructions map geometry to microtonal music
"The rhythmic dynamics of Clapping Music find a connection with recent research on aperiodic tilings, such as that presented by Fujita and Niizeki"
-
Deterministic codes cap DMRA overhead at 1 + log2 e bits
"the number of uncovered patterns decays at least geometrically fast with index, and greedy algorithms suffice"
-
Tidal forces and gas drag barely shift planetary orbital ratios
"nebular drag … ρ = ρ_c (r/r_c)^d, c = c_c (r/r_c)^{s/2}; resulting K_Drag (25)"
-
Pathwidth three forces exponential ascents in local search
"T_m = 10(2^m - 1) ... m_k = 2^{k-1}(8n + 16) - 16, s_k = 8(n - k) ... doubling flow ... control flow"
-
TMD bandgap limits multijunction solar efficiency to 63%
"optimal bandgap ladders … DP optimizer yields the ladder Eg(N=5) ≈ (2.10, 1.78, 1.50, 1.24, 1.00) eV"
-
One-shot diffusion lifts few-shot accuracy up to 20 percent
"R(˜f)−R(f)=1/4(E[f(x)y]−E[fA(x)y])+1/8(E[f(x)fA(x)]−1) (accuracy gap + diversity term)"
-
Local equilibrium refines prompts in deep AI systems without signal loss
"This local approach avoids global feedback chains... TEP maintains stable performance across all scales through local optimization."
-
Regularizers fix multimodal representation collapse
"Theorem 3.2 … Rényi-2 entropy … effective rank reff(Σ) = (tr Σ)² / tr(Σ²)"
-
DNA microgels swell twofold and dissolve on specific cue
"diffusion kinetics... reaction-diffusion model... effective diffusivity... swelling-induced modulation of molecular transport"
-
Cyclic KL projections converge at rates linear in 1/γ
"Proposition 4.2 ... non-expansiveness of Ψ w.r.t. ∥·∥_V1"
-
Continuous scores cut reasoning strategy sample needs by K log K
"When preference probabilities follow the Bradley-Terry model P(yw ≻ yl|x) = σ(U(x, yw)−U(x, yl)), the DPO optimal policy satisfies rθ(x, yi)−rθ(x, yj) = U(x, yi)−U(x, yj)"
-
Single layer unifies calibration and debiasing in recommendations
"For any x1 ≤ x2, the activation vectors satisfy a(x1) ≤ a(x2) element-wise by construction. Since w+_j = ReLU(w_j) ≥ 0, the dot product preserves this ordering"
-
Averaging predictors over symmetries sharpens conformal sets
"ΠG[s;f](x,y) := ∫_G s(f(φ_{g^{-1}}(x)), ψ_{g^{-1}}(y)) dμ(g) ... E[ν(S_{f^G})] ≤ E[ν(S_f)] for increasing convex ν"
-
Meaning abstraction drives model-brain alignment
"the relation between intrinsic dimension and brain predictivity arises over model pre-training... finetuning models to better predict the brain causally increases both representations' intrinsic dimension and their semantic content"
-
Reusing prior posteriors speeds up sequential flow matching
"Proposition 3.1 one-step sampling error W₂²(pBayes,p) ≤ E Var(xt|xt−1) via temporal coupling"
-
GNN embeddings mapped to latent manifolds detect IoT intrusions at 0.83 F1
"GNN-CLS ... Ltotal = λtask · Ltask + λtopo · (Ltopo(U) + Ltopo(W))"
-
Deformed SYK reaches stretched horizon in de Sitter
"Krylov spread complexity CS = ℓy/λ with Lanczos coefficients minimizing cost function (3.31),(3.38)"
-
Krause Attention linearizes transformers with local consensus rules
"the empirical distribution µt tends toward a multi-atomic structure µt ⇀ ∑ πk δLk"
-
StreamServe: Adaptive Speculative Flows for Low-Latency Disaggregated LLM Serving
"dspec = dbase + (at · Mf · γ) · ϕload · ϕtput"
-
Monoid structure fixes space for out-of-order product
"For monoids, we establish a trichotomy: the space complexity is either Θ(1), Θ(log n), or Θ(n)... constant-space solution for commutative monoids... FL∨Com... all remaining monoids require Ω(n) space."
-
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)"
-
Neural nets parametrize convex bodies to map shape functional ranges
"interacting particle system that minimizes a Riesz energy functional ... min |F(Ω_i) − F(Ω_j)|^{-s}"
-
XRISM data show NGC 1068 iron from thin gas, not thick reflector
"The Fexxv and Fexxvi emission lines exhibit remarkably large velocity widths, of several thousand km s−1"
-
Fiber geometry sets multirotor energy-promptness limits
"ρ(v) = 2^m √det(A diag(v²) Aᵀ) as fiber density / dynamic manipulability"
-
Eye fixations at question onset double VLM accuracy on ambiguous queries
"temporal window centered on speech onset … 600 ms width … performance peaks … near speech onset (-200 ms to +400 ms)"
-
Capacity bounds derived for hard-core model on triangular lattice
"The faces of A define a 6-regular graph G_A ... contour γ is a maximal connected component ... |Γ_m_l| = O(l^2 10^l)"