theorem
proved
dimension_forced
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.Foundation.DimensionForcing on GitHub at line 383.
browse module
All declarations in this module, on Recognition.
explainer page
Derivations using this theorem
depends on
used by
formal source
380
381 There is no free parameter; D is determined.
382 The 8-tick and gap-45 are now consequences, not premises. -/
383theorem dimension_forced : ∃! D : Dimension, RSCompatibleDimension D := by
384 use 3
385 constructor
386 · exact D3_compatible
387 · intro D hD
388 exact dimension_unique D hD
389
390/-! ## Physical Interpretation -/
391
392/-- The spatial dimension of the physical world. -/
393def D_physical : Dimension := 3
394
395/-- D_physical is RS-compatible. -/
396theorem D_physical_compatible : RSCompatibleDimension D_physical := D3_compatible
397
398/-- The eight-tick cycle in D = 3 dimensions. -/
399theorem physical_eight_tick : EightTickFromDimension D_physical = 8 := rfl
400
401/-- **WHY D = 3**
402
403 The dimension is not a free parameter. It is forced by:
404
405 1. **Alexander duality (PRIMARY, proved from axiom)**:
406 `SphereAdmitsCircleLinking D ↔ D = 3`, proved from the reduced
407 cohomology of S¹ axiom in `AlexanderDuality.lean`. Independent of T7.
408 H̃₁(Sᴰ \ S¹) ≅ H̃^{D-2}(S¹), nontrivial iff D = 3.
409
410 2. **Clifford algebra (CHARACTERIZATION)**: Cl₃ ≅ M₂(ℂ) gives
411 2-component complex spinors — the unique structure for spin-½.
412 (See `CliffordBridge.cl3_iso_m2c`)
413
papers checked against this theorem (showing 30 of 66)
-
Cognitive VLM plus diffusion planner tops driving benchmarks
"Extensive experiments on the NAVSIM and Bench2Drive benchmarks demonstrate that ReCogDrive achieves state-of-the-art performance."
-
MRKL systems pair language models with external knowledge modules
"Jurassic-X... some of the technical challenges in implementing it"
-
Shortcut models cut diffusion sampling to one step
"Across a wide range of sampling step budgets, shortcut models consistently produce higher quality samples than previous approaches, such as consistency models and reflow."
-
Open benchmark makes jailbreak attacks comparable across LLMs
"We have carefully considered the potential ethical implications of releasing this benchmark, and believe that it will be a net positive for the community."
-
GPT-4V and Gemini reach only 56-59% on expert multimodal benchmark
"We introduce MMMU: a new benchmark designed to evaluate multimodal models on massive multi-discipline tasks demanding college-level subject knowledge and deliberate reasoning. MMMU includes 11.5K meticulously collected multimodal questions from college exams, quizzes, and textbooks, covering six core disciplines..."
-
Qwen2.5-1M models reach 1 million token contexts
"Key techniques such as long data synthesis, progressive pre-training, and multi-stage supervised fine-tuning are employed to effectively enhance long-context performance while reducing training costs."
-
LiveBench updates monthly with fresh questions to block LLM test contamination
"LiveBench contains questions that are based on recently-released math competitions, arXiv papers, news articles, and datasets, and it contains harder, contamination-limited versions of tasks from previous benchmarks such as Big-Bench Hard, AMPS, and IFEval."
-
Open audio model tops 20+ benchmarks with public data only
"AF3 achieves new SOTA results on over 20+ (long) audio understanding and reasoning benchmarks"
-
Motion diffusion model predicts clean samples for SOTA results
"MDM is a generic approach, enabling different modes of conditioning, and different generation tasks. We show that our model is trained with lightweight resources and yet achieves state-of-the-art results on leading benchmarks for text-to-motion and action-to-motion."
-
Thyme lets AI write code to edit images on the fly
"comprehensive evaluations on nearly 20 benchmarks show that Thyme yields significant and consistent performance gains, particularly in challenging high-resolution perception and complex reasoning tasks"
-
Cosmology tensions may need new physics or better systematics
"These discordances primarily rest on the divergence in the measurement of core cosmological parameters with varying levels of statistical confidence. These possible statistical tensions may be partially accounted for by systematics in various measurements or cosmological probes but there is also a growing indication of potential new physics beyond the standard model."
-
Spotlighting cuts indirect prompt injection success to under 2%
"We introduce spotlighting, a family of prompt engineering techniques"
-
1M precise text-video pairs raise T2V quality
"Our OpenVid-1M has several characteristics: 1) Superior in quantity... 2) Superior in visual quality... 3) Expressive in caption"
-
H0 tension at 5 sigma signals need for new cosmology
"their persistence after several years of accurate analysis strongly hints at cracks in the standard cosmological scenario and the necessity for new physics or generalisations beyond the standard model"
-
1.3B model matches 5x larger ones on math and coding
"Our training data for phi-1.5 is a combination of phi-1’s training data (7B tokens) and newly created synthetic, “textbook-like” data (roughly 20B tokens) for the purpose of teaching common sense reasoning and general knowledge of the world"
-
WinoGrande shows models at 59-79% on commonsense test
"establish new state-of-the-art results on five related benchmarks - WSC (90.1%), DPR (93.1%), COPA (90.6%), KnowRef (85.6%), and Winogender (97.1%)"
-
SM effective theory reduced to 59 independent dimension-six operators
"Assuming baryon number conservation, we find 15 + 19 + 25 = 59 independent operators (barring flavour structure and Hermitian conjugations), as compared to 16 + 35 + 29 = 80 in Ref.[3]."
-
ChatGPT coordinates Hugging Face models to handle complex tasks
"HuggingGPT can tackle a wide range of sophisticated AI tasks spanning different modalities and domains"
-
SPT-3G CMB spectra give H0 of 66.66 km/s/Mpc
"We report a Hubble constant of H0=66.66±0.60 km/s/Mpc from SPT-3G alone, 6.2 sigma away from local measurements from SH0ES."
-
ReTool teaches LLMs to interleave code calls via outcome rewards
"ReTool-32B attains 72.5% accuracy... outperforming OpenAI's o1-preview by 27.9%"
-
Video pre-training lifts robot manipulation success to 94.9%
"On CALVIN benchmark, our method outperforms state-of-the-art baseline methods and improves the success rate from 88.9% to 94.9%."
-
ACT DR6 data set baryon density at 0.0226 and H0 at 68.22
"We find no evidence for excess lensing in the power spectrum, and no departure from spatial flatness."
-
RWKV hits Transformer performance at 14B parameters
"We scale our models as large as 14 billion parameters, by far the largest dense RNN ever trained, and find RWKV performs on par with similarly sized Transformers."
-
Sharing parameters across tasks boosts deep learning results
"MTL acts as a regularizer by introducing an inductive bias. As such, it reduces the risk of overfitting as well as the Rademacher complexity of the model."
-
Any three late-universe H0 methods yield 4-5.8 sigma tension
"Theoretical ideas to explain the discrepancy focused on new physics in the decade of expansion preceding recombination"
-
Data filtering produces strong 6B and 34B language models
"Building upon our scalable super-computing infrastructure and the classical transformer architecture"
-
Quantum algorithm solves Abelian stabilizer problem in polynomial time
"We present a polynomial quantum algorithm for the Abelian stabilizer problem which includes both factoring and the discrete logarithm. Our method is based on a procedure for measuring an eigenvalue of a unitary operator."
-
Black-hole oscillations encode plasma hydrodynamics via duality
"decoupling of variables in the perturbation equations, quasinormal modes (with special emphasis on various numerical and analytical methods of calculations), late-time tails, gravitational stability"
-
Hundreds of thousands of qubits needed for practical quantum advantage
"hundreds of thousands to millions of physical qubits are needed to achieve practical quantum advantage. We identify three qubit parameters, namely size, speed, and controllability"
-
Attention gates raise U-Net accuracy on CT pancreas scans
"Experimental results show that AGs consistently improve the prediction performance of U-Net across different datasets and training sizes while preserving computational efficiency."