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 110)
-
DRL agent cuts bike availability failures with one truck
"The criticality score is ψ(v′i,k)=exp(ζv′i(k))−1 ... A zone is classified as critical if ψ(v′i,k)>0"
-
Replaying early insights lifts accuracy in every LLM reasoning test
"InsightReplay ... replays them near the active generation frontier"
-
Geometric lattices produce finite orthogonal polynomials uniformly
"H(Vk) ⊆ Vk−1 ⊕ Vk+1... J ρk = βk−1 ρk−1 + βk ρk+1 with diagonal zero"
-
Visit order substitutes for labels in few-shot severity scoring
"Under the clinically plausible assumption of monotonic progression in irreversible diseases, the method learns disease-relevant representations without using any expert labels... sim(v1,v2) ≥ sim(v1,v3) for t1 < t2 < t3"
-
Lightning V2 achieves 4x lower TTS cost on Tenstorrent vs L40S
"Leveraging Tenstorrent’s Network-on-Chip (NoC), distributed SRAM, and deterministic execution model, we reduce memory movement and redundant weight fetches"
-
One logarithmically diverging eigenvalue per symmetry block
"The function G_p extends ... to a generalized hypergeometric function ... resonant expansion ... (1-u/ζ_c²)² log(1-u/ζ_c²)"
-
Silhouette loss raises top-1 accuracy from 36.7% to 39.1%
"hybrid L = L_sup + λ_sil L_sil; batch-level global cluster quality"
-
Asynchronous AI agent reaches 83% percentile on ML benchmark
"P(N, t) = 100·g(N, t)/(g(N, t) + 1), g(N, t) = α·log(γ t + 1)·log(β N + 1)"
-
Token entropy regulation sharpens LLM reasoning paths
"Bucket-based Implicit Normalization... ̃s_{i,t} = (s_{i,t} - μ_{k,𝒢}) / σ_{k,𝒢} + δ"
-
RL method picks better seeds on incomplete social graphs
"Path-Entropy-Steiner backbone + Gramian controllability views with GAT surrogate and contrastive loss J (Eqs. 5-18)"
-
Re-evaluating stale gradients cuts error from quadratic to linear in delayed decisions
"staleness amplification … bilevel Lipschitz constant L_F = L_θ + L_wθ²/μ_w … coupling constant C_0 = L_wθ/μ_w"
-
17 nm oxide thickness cuts variability in silicon quantum dot arrays
"The threshold voltages, capacitances, lever arms, and charging energies are extracted using parallel row based measurements"
-
LiBaGS selects synthetic data near boundaries to improve accuracy
"Δj(tj) = rj / (cj + tj) − rj / (cj + tj + 1)"
-
EMO grows MoE experts in stages to match full performance
"MoE capacity should grow progressively with data as an expandable memory."
-
New dwarf nova below period minimum shows 72-minute superhumps
"we estimate the superhump period to be P_sh ≈ 71.7 minutes … Since the orbital period in WZ Sge-type DNe is typically very close to the superhump period, we consider that this target would belong to the small sample of DNe below the period minimum"
-
LLM framework unifies macro and micro economic simulations
"memory module ... long-term and short-term banks ... ESIt = λ ESIt−1 + (1−λ) ESIt,LLM"
-
Multi-scale graphs improve microservice latency estimates
"multi-scale graph adaptive fusion module leveraging graph attention networks for hierarchical feature extraction"
-
Fewer trajectories yield up to 63% better agent scores
"Map-Reduce paradigm with a sliding memory mechanism ... heuristic safe-split points ... context-aware local mapping"
-
Fast-slow recurrence stabilizes long-sequence models
"energy of X(1) spikes upon arrival of new token and stabilizes … X(2) organized by stack depth … crisp spring-shaped manifold indexed by stack depth"
-
Cu-Al exchanges at precipitates drive low strain-rate sensitivity
"m(ε̇) = d ln τ / d ln ε̇ ... low strain-rate sensitivity across a broad range of intermediate quasi-static strain rates"
-
Streaming CSPs need Ω(√n/p) space to beat LP threshold
"The weight of a restriction ∥ζ∥ = sum |Vi|^2 over connected components of exposed edges."
-
Multi-aspect distillation matches baselines at fixed model size
"Lmatrix = LMHA + LFNN; Llayer = Lattn + Lhidn; hierarchical assignment to shallow/deep layers"
-
Quantum circuits solve portfolio PDE with 80x fewer parameters
"Merton HJB solution v(t,x) = exp(-k(T-t)) x^γ/γ admits rank-1 tensor decomposition (separable univariate factors)"
-
Inelastic particles yield density-capped 1D Euler equations
"A key ingredient of our result is a monotonicity property of the congested region, which allows us to reduce the dynamics to a first-order evolution in time."
-
Penalty term enables unconditional stability in biharmonic wave IGA
"CFL condition of the form h_t < C_Ω h_s² … unconditionally stable space-time isogeometric discretization"
-
Neural diffusion codec beats H.264 lossless video
"I/P-frame architecture with temporal conditioning... reference embedding (+1.3% parameters)"
-
Hyperbolic space gives fonts a radial style-specificity score
"low style-specificity impressions lie near the origin and high style-specificity impressions lie farther away... coherent progression from ambiguous to more style-specific"
-
Architecture decides whether transformer errors stay hidden from confidence checks
"both matched-width configurations form the signal at the earliest measured checkpoint, and training erases it in the 1.4B"
-
Halos store 20-30% of disk dust despite fast drift
"tdrift = (r/hg)^2 (St + St^{-1}) / ((1+ϵ)^2 γ ΩK); tgrow ..."
-
Decoupled method aligns verbalized confidence in LLMs
"Spearman correlation reward ... RSC(c, κ;C, K) = rs(C∪{c},K∪{κ})−rs(C,K)"