theorem
proved
hierarchy_emergence_forces_phi
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Foundation.HierarchyEmergence on GitHub at line 95.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
-
scale -
lt_trans -
locality_forces_additive_composition -
UniformScaleLadder -
MinimalHierarchy -
closed_ratio_is_phi -
GeometricScaleSequence -
ledgerCompose -
from -
uniform -
and -
L -
L -
S -
isClosed
used by
formal source
92
93/-- **Bridge B1 (unconditional)**: from a zero-parameter scale ladder
94with additive composition, the scale ratio is forced to `φ`. -/
95theorem hierarchy_emergence_forces_phi
96 (L : UniformScaleLadder)
97 (additive_closure : L.levels 2 = L.levels 1 + L.levels 0) :
98 L.ratio = φ := by
99 let S : GeometricScaleSequence :=
100 { ratio := L.ratio
101 ratio_pos := lt_trans (by norm_num) L.ratio_gt_one
102 ratio_ne_one := by linarith [L.ratio_gt_one] }
103 have h_closed : S.isClosed := by
104 unfold GeometricScaleSequence.isClosed
105 unfold ledgerCompose
106 unfold GeometricScaleSequence.scale
107 have hrec := locality_forces_additive_composition L additive_closure
108 nlinarith [hrec]
109 exact closed_ratio_is_phi S h_closed
110
111/-- Combined emergence theorem: from ledger primitives (uniform scale
112ladder + additive composition), derive the `MinimalHierarchy` package
113and conclude `φ`. -/
114theorem ledger_forces_phi
115 (L : UniformScaleLadder)
116 (additive_closure : L.levels 2 = L.levels 1 + L.levels 0) :
117 ∃ H : MinimalHierarchy, H.scales.ratio = φ := by
118 let S : GeometricScaleSequence :=
119 { ratio := L.ratio
120 ratio_pos := lt_trans (by norm_num) L.ratio_gt_one
121 ratio_ne_one := by linarith [L.ratio_gt_one] }
122 have h_closed : S.isClosed := by
123 unfold GeometricScaleSequence.isClosed
124 unfold ledgerCompose
125 unfold GeometricScaleSequence.scale
papers checked against this theorem (showing 30 of 66)
-
Variance reduction lifts diffusion language model alignment by several points
"the resulting model, LLaDA 1.5, outperforms its SFT-only predecessor consistently and significantly across mathematical (GSM8K +4.7), code (HumanEval +3.0, MBPP +1.8), and alignment benchmarks"
-
TD-MPC2 hits strong results on 104 tasks with one hyperparameter set
"We further show that agent capabilities increase with model and data size, and successfully train a single 317M parameter agent to perform 80 tasks across multiple task domains, embodiments, and action spaces."
-
WinoGrande shows models at 59-79% on commonsense test
"systematic bias reduction using a novel AfLite algorithm that generalizes human-detectable word associations to machine-detectable embedding associations"
-
Latent Action Pretraining from Videos
"Experimental results demonstrate that our method significantly outperforms existing techniques that train robot manipulation policies from large-scale videos."
-
Pixel ops lift 7B VLM to 84% on visual reasoning tests
"Our 7B model, Pixel Reasoner, achieves 84% on V* bench, 74% on TallyQA-Complex, and 84% on InfographicsVQA"
-
One reward model improves both vision understanding and generation
"jointly learning to assess diverse visual tasks yields substantial mutual benefits... achieving consistent improvements across each domain"
-
Reward design lifts LLM tool use 17% above base models
"Empirical evaluations across diverse benchmarks demonstrate that our approach yields robust, scalable, and stable training, achieving a 17% improvement over base models and a 15% gain over SFT models."
-
ChatGPT coordinates Hugging Face models to handle complex tasks
"By leveraging the strong language capability of ChatGPT and abundant AI models in Hugging Face"
-
Multi-teacher approach tops driving planner benchmark
"Hydra-MDP learns how the environment influences the planning in an end-to-end manner instead of resorting to non-differentiable post-processing"
-
PyTorch Geometric accelerates graph learning with sparse GPU kernels
"NeighborhoodAggregation... message passing scheme... gather and scatter operations"
-
Diffusion models plan by denoising trajectories
"The core of our technical approach lies in a diffusion probabilistic model that plans by iteratively denoising trajectories."
-
Inverted dimension swap lifts Transformer forecasting accuracy
"The iTransformer model achieves state-of-the-art on challenging real-world datasets, which further empowers the Transformer family with promoted performance, generalization ability across different variates, and better utilization of arbitrary lookback windows"
-
EHT resolves the shadow of the Milky Way's central black hole
"Using a large suite of numerical simulations, we demonstrate that the EHT images of Sgr A* are consistent with the expected appearance of a Kerr black hole with mass ∼4 × 10^6 M⊙"
-
1.7B model beats peers after 11T token data mix
"we demonstrate that SmolLM2 outperforms other recent small LMs including Qwen2.5-1.5B and Llama3.2-1B"
-
DCGANs learn image parts to scenes without labels
"We use the trained discriminators for image classification tasks, showing competitive performance with other unsupervised algorithms"
-
LSUN builds one million images per category via human-AI labeling loop
"we propose to amplify human effort through a partially automated labeling scheme, leveraging deep learning with humans in the loop"
-
Video pre-training lifts robot manipulation success to 94.9%
"We provide inaugural evidence that a unified GPT-style transformer, augmented with large-scale video generative pre-training, exhibits remarkable generalization to multi-task visual robot manipulation."
-
SnapKV compresses KV caches from end-of-prompt attention window
"SnapKV achieves a consistent decoding speed with a 3.6x increase in generation speed and an 8.2x enhancement in memory efficiency"
-
Benchmarks teach language models to guess instead of saying they are unsure
"This “epidemic” of penalizing uncertain responses can only be addressed through a socio-technical mitigation: modifying the scoring of existing benchmarks"
-
Android benchmark shows agents complete 30.6% of dynamic tasks
"Our best agent can complete 30.6% of AndroidWorld's tasks, leaving ample room for future work."
-
Deep nets fit random labels as easily as real ones
"simple depth two neural networks already have perfect finite sample expressivity as soon as the number of parameters exceeds the number of data points"
-
Decoupled feedback raises both helpfulness and safety in LLMs
"Through a three-round fine-tuning using Safe RLHF, we demonstrate a superior ability to mitigate harmful responses while enhancing model performance"
-
ReST aligns LLMs offline for better translations
"ReST produces a dataset by generating samples from the policy, which are then used to improve the LLM policy using offline RL algorithms. ReST is more efficient than typical online RLHF methods because the training dataset is produced offline, which allows data reuse."
-
No LLM agent tops 60% on new safety benchmark
"AGENT-SAFETY BENCH encompasses 349 interaction environments and 2,000 test cases, evaluating 8 categories of safety risks and covering 10 common failure modes"
-
Evolutionary search recovers scientific equations from data
"we also introduce a new benchmark, 'EmpiricalBench,' to quantify the applicability of symbolic regression algorithms in science."
-
DeepSpeed-Ulysses trains 4x longer sequences 2.5x faster
"DeepSpeed-Ulysses trains 2.5x faster with 4x longer sequence length than the existing method SOTA baseline."
-
Linear bias lets models train short and test long
"ALiBi's inductive bias towards recency also leads it to outperform multiple strong position methods on the WikiText-103 benchmark."
-
Hundreds of thousands of qubits needed for practical quantum advantage
"We develop a framework for quantum resource estimation, abstracting the layers of the stack"
-
Vanilla PPO scales reasoning on base models with one-tenth the steps
"Using the same base model, Qwen2.5-32B base, as DeepSeek-R1-Zero-Qwen-32B, our implementation achieves superior performance across AIME2024, MATH500, and GPQA Diamond"
-
Multilingual E5 models match English SOTA
"Additionally, we introduce a new instruction-tuned embedding model, whose performance is on par with state-of-the-art, English-only models of similar sizes."