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 197)
-
Distilled policies plus online feedback yield adaptive humanoid control
"AMP-based reward... discriminator... style reward r_style"
-
Semantic progress from visuals improves navigation consistency
"Since progress should evolve monotonically with the visual observation sequence, an earlier timestep should correspond to a prefix of a later one... Lmono = E max(0, k_ti - k_tj)"
-
Zeta avoids paired zeros off the critical line
"δs(t) integral equation and sign rigidity along L"
-
Plug-in adapts foundation flow models for use as inverse problem priors
"time-dependent warm-start strategy ... min_{z,t} ℓ(y, A ∘ G_θ(α_t y + β_t z, t))"
-
Drift correction lifts CLIP robustness nearly 50% above prior methods
"τ = 1/n Σ cos(di, d-bar); f* = fx + α d-bar if τ > τ*"
-
RL skill library cuts agent steps by 26% while raising accuracy
"Skill-integrated Reward... R1 = r1 + 1[r1=1]*1[r2=1]*1skill(q2|q1)"
-
Statistical guidance adapts meta-learning for fiber sensing shifts
"dual-domain learner constructs multi-prototype class representations... query-adaptive aggregation strategy"
-
On-axis laser system reaches nanometer inter-satellite ranging
"the interferometric link achieves a pointing stability below 10 µrad/√Hz ... TTL coupling ..."
-
Chukchi myths mirror special relativity absolutes
"each timelike worldline... is associated with an ideal clock that measures the 'length' along that worldline — the proper time... non-integrable"
-
Generative model makes station-specific quake records without site inputs
"f0 distribution confusion matrices and median HVSR curves"
-
Few satellite images reconstruct entire city blocks in 3D
"Z-Monotonic SDF... yields a watertight mesh with crisp roofs and clean, vertically extruded facades"
-
Modulated oscillator converts frequencies via topological winding number
"Floquet–Sambe space ... effective electric field |E_syn|=1 ... β≡(η_P−η_γ)/η_κ"
-
GL(3) cuspidal reps lift to GL(8) via triality
"the twisted endoscopic groups ... are ... G2, SL3 and SO4 ... ˜Ad : PGL3(C) → Spin8(C)"
-
Countable compactness lets groups act on joins
"Prop 1.1: identity Z e× CιX ≅ product topology when Z compact<κ and χ(A,J)<κ"
-
3D agent jointly plans speech, prosody, and body motion
"We standardize on a 25 fps universal clock... fractional index... Rotary positional encoding."
-
Classifier detects dependence by separating aligned from shifted segments
"Theorem 1 … E{z+}−E{z−}=p(1−p)pαpβ(1−pϵx)(1−pϵy)"
-
Dual-LAO speeds RBFE calculations 15-30 times for complex changes
"Lambda-ABF-OPES framework... dual-DBC scheme... Dmin = 2.0 Å"
-
Semantic-free ray contrast disambiguates floorplan poses
"visual-geometric compatibility function ... dual-level constraints ... position-level and orientation-level"
-
Fisher selection lifts vulnerability detection F1 by 6 points
"Fisher Information Matrix (FIM) quantifies the sensitivity of classification decisions to feature perturbations"
-
P(Sufficient) probe tracks LLM evidence buildup across turns
"P(SUFFICIENT)... probes the confidence by asking model if the current information is sufficient... distinguishes meaningful information gains from conversational filler"
-
Self-alignment across masks lifts 3D point cloud accuracy
"Dual Self-Representation Alignment... Lmae−sra=1−hstudent·hteacher/|hstudent|·|hteacher|; MFT-SRA cosine alignment across time steps"
-
Metrics separate separation strength from fragment count in political networks
"we introduce a novel metric for multiscale fragmentation, the effective branching factor (EBF)"
-
Precomputed flexibility replans paths after single delays
"We represent this flexibility in the search by creating an additional safe edge ... AF[e] = ⟨ζ, β, β+f_aF(x,t),Δ⟩"
-
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)"