embed_strictMono_of_one_lt
plain-language theorem explainer
The declaration shows that the orbit embedding of the recovered natural numbers into positive reals is strictly monotone when the generator value exceeds one. Workers reconstructing arithmetic structures from the Law of Logic would reference this result to guarantee order preservation under the embedding. The argument reduces immediately to the right-to-left direction of the companion iff statement for the same embedding.
Claim. Let $γ$ be a generator with value greater than 1. The embedding map from the Peano structure on the orbit to the positive reals is strictly monotone.
background
Generator denotes a positive real number distinct from 1, extracted from the non-triviality of any comparison operator satisfying the Law of Logic. The embed function maps the identity element of the recovered naturals to 1 and each successor step to multiplication by the generator value, producing the orbit under repeated multiplication. The recovered naturals themselves arise as the abstract Peano structure on the orbit of any such generator, as constructed in the preceding lemmas of this module.
proof idea
The proof is a one-line wrapper that invokes the right-to-left implication of the companion iff lemma on the given strict inequality between embedded values.
why it matters
This result secures the order-preserving property required for the recovery of natural-number arithmetic from the functional equation. It directly supports the module summary that the Peano axioms become theorems once the orbit structure is in hand. The declaration leaves open the generator-free characterization of the orbit and the direct definition of order on the recovered naturals, both flagged for later modules.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.
papers checked against this theorem (showing 30 of 387)
-
Advanced kinks make Kibble-Zurek scaling robust to endpoints
"the density of kinks extracted in the central part of long chains obeys the predicted universal scaling for all types of boundary conditions"
-
Cartan matrix realizes Zamolodchikov metric in Narain theories
"root and weight lattices can encode the momenta... Θ_g^{(r,r)}(τ1,τ2,x) = ∑ e^{-πτ2⟨β∨·β⟩} e^{2πiτ1⟨β∨·χ⟩} e^{-πτ2⟨χ∨·χ⟩}"
-
Log-likelihood strongly concave near true tree parameters
"Strong concavity λ_min(H) ≥ C8/δ − 26 independent of tree size (Cor. 2.3) via Gershgorin + exponential off-diagonal decay"
-
Model predicts city winds from 23 simulations
"Trained on only 24 CFD simulations... mean absolute errors of 0.3 m/s for wind speed and 0.3 °C for temperature"
-
Phrase retrieval guides LLMs to accurate radiology reports
"We introduce several training techniques... in-batch contrastive loss to align text and semantic embeddings"
-
Critical marked Hawkes processes converge to stable or Gaussian limits
"branching particle system... resolvent R(s)... potential G(α)"
-
Online edge-weighted matching ratio lies between 0.662 and 0.663
"Let f(t) denote the probability that exactly one offline vertex has been matched at time t and g(t) denote the probability that both offline vertices have been matched at time t."
-
Tensor networks average spin-chain disorder without sampling
"the algorithm exploits statistical translation invariance and works directly in the thermodynamic limit"
-
Double robustness preserved for semi-supervised estimators with decaying overlap
"the observed-data influence function... ϕ(D;θ⋆)=μ⋆(X)+R/π⋆(X)(ϕF−μ⋆(X))−θ⋆"
-
Synthetic time cuts photonic hardware exponentially
"recursive architecture... fractal, self-similar structure that leads to complex and nonmonotonic transport patterns"
-
Catalytic EC yields higher rates than distillation under low noise
"For the case of EC protocols, we use Naimark’s dilation to convert the required POVMs into projective measurements by introducing auxiliary qubits... synthesis into MCX gates"
-
SCAN reveals performance gaps inside LLM sub-capabilities
"fine-grained analysis... substantial performance variations, even within sub-capabilities belonging to the same category"
-
Different LLM layers capture local versus global time series patterns
"Logo-LLM introduces lightweight Local-Mixer and Global-Mixer modules to align and integrate features with the temporal input across layers."
-
Curved BaTiO3 nanorods form domain stripes above critical bend
"The distribution of the polarization components P1, P2, and P3, and the strain components u11, u22, and u33 calculated at the surface of a curved BaTiO3 nano-slab"
-
DRP trims reasoning tokens from 917 to 328 on GSM8K
"aligning the reasoning structure of training CoTs with the student's reasoning capacity is critical"
-
Hilbert curves scale Vision Mamba to high resolutions
"FHSC selects one representative pair of spatially adjacent but sequentially distant sibling segments at each recursion level... E = union over l=1 to L of {(mid(S(1)_l), mid(S(4)_l))}"
-
Deep learning method boosts structural color accuracy by 65%
"we propose Physics-Guided Inference (PGI) to embed spectral information into input features"
-
LLM lemmas certify 0.8559 lower bound on Steiner ratio
"Steiner Spiral Chain ... every internal angle ∠Ai−1AiAi+1 ... exactly 120°"
-
M-dwarf transit survey finds 2 high-robustness candidates
"Three independent empirical tests probe complementary aspects of signal robustness: Circular shift FAR, Lightcurve inversion, Fourier phase scrambling"
-
Large spots drive 5-10 year brightness drifts in 0.4-day binary
"A reduced number of terms is appropriate ... f(φ)/fmax = A0 + A1 cos(φ) + A2 cos(2φ) + A4 cos(4φ) + B1 sin(φ)"
-
Degree-scaled frequencies force complete sync in frustrated oscillators
"optimal natural frequencies scale linearly with the node degree"
-
Geometry-aware calibration closes entropy gaps for LLM optimization
"V(x) = Σ pk Tr(Cov(g|Z=k)) + Tr(Cov(μZ)) (intra- vs inter-cluster gradient variance)"
-
Actor updates match value gradients under differentiable rollouts
"λ_t := ∂R_t / ∂s_t ... λ_t = Dr(s_t, a_t) + γ (Df_θ(s_t, a_t))^T λ_{t+1}"
-
Fractal triangles locate image content faster
"Evidence elements improve the odds of finding the desired content and are closely associated to it in terms of spatial location."
-
Video frames close the detection gap between AI images and videos
"We model video frames as image signals subjected to a complex, non-differentiable degradation function T(·)."
-
Butterfly factorization speeds manifold harmonic transforms
"We now establish asymptotic storage and complexity results ... for the flat torus M = [−π, π]². ... rε ≤ 5/2 + log(ε−4) · ⌈e/2 bR + log(ε−1)⌉"
-
One unitary propagation yields the full reduced map at finite temperature
"TFD evolution is implemented in the TT representation... leading eigenvalues of the normalized Choi state"
-
TimeGuard boosts backdoor resistance in time series forecasts by 1.96x
"Theorem 4.1 (TSF Backdoor Success Bound) using Nadaraya-Watson kernel and neighborhood distance"
-
Monitoring at one site turns entanglement growth linear then to zero
"SL,R(t) = ∫ dk/2π min(|vk|t,L) h(⟨nk(t)⟩) with Gaussian ⟨nk⟩ ∝ ⟨Ntot⟩ exp(−k²/2σ(t))"
-
GNN explanations spot disease hubs via decaying attribution
"attribution peaks in the immediate 1-hop neighborhood and decays across successive network shells... shell-based hub score"