phi_equation
Why this theorem is linked from Measuring Massive Multitask Language Understanding unclear
Pith linked this Lean declaration because the review connected a specific passage in the paper to this theorem. The relation tag says how strong that connection is; it is not a generic placeholder.
We propose a new test to measure a text model's multitask accuracy. The test covers 57 tasks including elementary mathematics, US history, computer science, law, and more.
Relation between the paper passage and the cited Recognition theorem.
plain-language theorem explainer
The golden ratio φ obeys φ² = φ + 1. This identity is referenced by arguments that derive φ from self-similarity on a discrete J-cost ledger and by downstream results on forcing principles and economic inevitability. The proof reduces the claim to real arithmetic by unfolding the explicit definition of φ and closing via field simplification with nlinarith on square-root identities.
Claim. Let $φ = (1 + √5)/2$. Then $φ² = φ + 1$.
background
The PhiForcing module establishes that self-similarity in a discrete ledger equipped with J-cost forces the golden ratio. φ denotes the positive real solution to x² = x + 1, written explicitly as (1 + √5)/2. The upstream Algebra.PhiRing.phi_equation records the identical algebraic identity in a ring setting; the present version re-derives it for direct use in the foundation layer.
proof idea
The tactic sequence unfolds the definition of φ together with squaring, introduces the non-negativity of 5, verifies that the square of its square root recovers 5, applies field simplification, and closes with nlinarith using the square-root identity and non-negativity of squares.
why it matters
This identity supplies the algebraic core of the phi forcing principle, which states that self-similarity on a J-cost ledger forces the scale ratio to φ. It is invoked directly by golden_constraint_unique, phi_forcing_principle, phi_inv, phi_satisfies, economic_inevitability, and StillnessGenerative results. In the Recognition framework it realizes the T6 step fixing φ as the self-similar fixed point, consistent with the eight-tick octave and D = 3.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.
papers checked against this theorem (showing 30 of 45)
-
Tweezer array traps 6100 atoms with 12.6s coherence
"Our results, along with recent developments, indicate that universal quantum computing and quantum error correction with thousands to tens of thousands of physical qubits could be a near-term prospect."
-
Reverse engineering AI internals could prevent catastrophic failures
"Superposition hypothesis: neural networks represent more features than they have neurons by encoding features in overlapping combinations of neurons."
-
Review maps the fast-growing world of large language models
"Large Language Models (LLMs) have recently demonstrated remarkable capabilities in natural language processing tasks and beyond."
-
Space interferometer to survey micro-Hz gravitational waves
"Conceived to detect massive black hole binaries from their early inspiral with high signal-to-noise ratio, and low-frequency stellar binaries in the Galaxy"
-
XLNet beats BERT on 20 tasks via permutation pretraining
"XLNet... enables learning bidirectional contexts by maximizing the expected likelihood over all permutations of the factorization order"
-
Six parameters capture Universe's history in Planck CMB maps
"Planck measures five of the six parameters to better than 1% (simultaneously), with the best-determined parameter (θ*) now known to 0.03%."
-
Sigmoidal curves predict RL performance for LLMs at 100k GPU hours
"Stable, scalable recipes follow predictable scaling trajectories, enabling extrapolation from smaller-scale runs."
-
Black hole star model fits early source with massive Balmer break
"This source provides evidence that black hole masses in the LRDs may be over-estimated by orders of magnitude"
-
Policy gradients fine-tune diffusion policies to top benchmark scores
"Through experimental investigation, we find that DPPO takes advantage of unique synergies between RL fine-tuning and the diffusion parameterization, leading to structured and on-manifold exploration, stable training, and strong policy robustness."
-
Supernovae data alone require acceleration at 5 sigma
"Using SN data alone and including systematic uncertainties we find Ω_M=0.352±0.017 in flat ΛCDM. Supernova data alone now require acceleration (q0<0 in ΛCDM) with over 5σ confidence."
-
BAO data rule out dark-energy-free models at 8 sigma
"The RSD measurements indicate a growth rate that is consistent with predictions from Planck primary data and with General Relativity"
-
Discrete text levels train LMMs to score visuals like humans
"The proposed Q-Align achieves state-of-the-art performance on image quality assessment (IQA), image aesthetic assessment (IAA), as well as video quality assessment (VQA) tasks under the original LMM structure."
-
H0 tension at 5 sigma signals need for new cosmology
"we focus on the 5.0σ tension between the Planck CMB estimate of the Hubble constant H0 and the SH0ES collaboration measurements"
-
EIC detectors must deliver gluon maps from polarized collisions
"The EIC will provide unprecedented access to the gluon-dominated structure of nucleons and nuclei and to their spin and spatial distributions through high-luminosity polarized electron-ion collisions."
-
Trillion-parameter models scale recommendation quality with compute
"HSTU-based Generative Recommenders, with 1.5 trillion parameters, improve metrics in online A/B tests by 12.4% and have been deployed on multiple surfaces of a large internet platform with billions of users. More importantly, the model quality of Generative Recommenders empirically scales as a power-law of training compute across three orders of magnitude, up to GPT-3/LLaMa-2 scale."
-
3D model lets robots imagine futures before acting
"we train a series of embodied diffusion models and align them into the LLM for predicting the goal images and point clouds"
-
ALBERT sets new SOTA on GLUE, RACE and SQuAD with fewer parameters than BERT-large
"we also use a self-supervised loss that focuses on modeling inter-sentence coherence"
-
Position Interpolation extends LLM context to 32k tokens
"Our theoretical study shows that the upper bound of interpolation is at least ∼600× smaller than that of extrapolation"
-
Quantum algorithm solves Abelian stabilizer problem in polynomial time
"Another application of this procedure is a polynomial quantum Fourier transform algorithm for an arbitrary finite Abelian group."
-
New model unifies world simulation for robot training
"These capabilities enable more reliable synthetic data generation, policy evaluation, and closed-loop simulation for robotics and autonomous systems"
-
GPT-4 chain-of-thought scores text summaries closer to humans
"G-EVAL is a prompt-based evaluator with three main components: 1) a prompt that contains the definition of the evaluation task and the desired evaluation criteria, 2) a chain-of-thoughts (CoT) ..."
-
COCO supplies 1.5 million captions for 330k images
"Instructions for using the evaluation server are provided."
-
MMBench delivers bilingual test for all-around VLMs
"MMBench is a systematically designed objective benchmark for a robust and holistic evaluation of vision-language models"
-
LIGO-Virgo catalog ten compact binary mergers from first two runs
"For all significant gravitational-wave events, we provide estimates of the source properties... using relativistic models of GWs from CBCs"
-
Open dataset of 400 million CLIP-filtered image-text pairs released
"We use CLIP to compute embeddings of the image and alt-text. Then we compute the cosine similarity of both embeddings and drop all samples with cosine similarity below 0.3"
-
Text contexts compressed optically into vision tokens at 10x with 97% accuracy
"DeepSeek-OCR consists of two components: DeepEncoder and DeepSeek3B-MoE-A570M as the decoder."
-
Smart choices cut AI training carbon by up to 1000 times
"Large but sparsely activated DNNs can consume <1/10th the energy of large, dense DNNs without sacrificing accuracy despite using as many or even more parameters"
-
Fine-tuned LLaMA beats GPT-4 at writing API calls
"Gorilla's retriever–aware training enables it to react to changes in the APIs."
-
GRPO adaptation stabilizes RL for visual generators
"outperforms baseline methods by up to 181% across... HPS-v2.1, CLIP Score, VideoAlign, and GenEval"
-
RetNet matches Transformer scaling with O(1) inference
"RetNet achieves favorable scaling results, parallel training, low-cost deployment, and efficient inference"