theorem
proved
bilinear_family_forced
show as:
view math explainer →
The bilinear cost family is forced by the d'Alembert factorization.
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.Foundation.DAlembert.Inevitability on GitHub at line 289.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
-
all -
multiplicative -
all -
of -
bridge -
scale -
IsNormalized -
reverse -
all -
has -
add_zero -
back -
mul_one -
mul_zero -
one_mul -
zero_add -
Calibration -
Normalization -
Calibration -
F_symmetric_of_P_symmetric -
HasMultiplicativeConsistency -
IsNormalized -
IsSymmetric -
polynomial_form_forced -
symmetry_and_normalization_constrain_P -
of -
HasMultiplicativeConsistency -
mul_eq_zero -
one -
reciprocity -
forces -
cost -
cost -
identity -
is -
of -
from -
one -
is -
of
used by
-
consistency_forces_RCL_form_is_theorem -
axiom_bundle_necessary -
polynomial_consistency_implies_right_affine -
rcl_right_affine -
rcl_without_gate -
log_bilinear_positive_cost_bilinear -
J_is_unique_cost_under_logic -
laws_of_logic_imply_dalembert_hypotheses -
RCL_is_unique_functional_form_of_logic -
route_independence_implies_multiplicative_consistency
formal source
286
287This means F satisfies the generalized d'Alembert equation.
288If we choose the canonical cost normalization c = 2, we recover the RCL. -/
289theorem bilinear_family_forced (F : ℝ → ℝ) (P : ℝ → ℝ → ℝ)
290 (hNorm : IsNormalized F)
291 (hCons : HasMultiplicativeConsistency F P)
292 (hPoly : ∃ (a b c d e f : ℝ), ∀ u v, P u v = a + b*u + c*v + d*u*v + e*u^2 + f*v^2)
293 (hSymP : ∀ u v, P u v = P v u) -- Explicit symmetry of P
294 (hNonTriv : ∃ x : ℝ, 0 < x ∧ F x ≠ 0)
295 (hCont : ContinuousOn F (Set.Ioi 0)) -- Regularity: F is continuous on (0, ∞)
296 : ∃ c : ℝ, (∀ u v, P u v = 2*u + 2*v + c*u*v) ∧
297 (c = 2 → ∀ u v, P u v = 2*u + 2*v + 2*u*v) := by
298 -- Derived reciprocity from symmetry of P
299 have hSym : IsSymmetric F := F_symmetric_of_P_symmetric F P hCons hSymP
300 -- Step 1: Normalization forces P(0, v) = 2v
301 have hP0 : ∀ y : ℝ, 0 < y → P 0 (F y) = 2 * F y :=
302 symmetry_and_normalization_constrain_P F P hSym hNorm hCons
303
304 -- Use the polynomial form lemma
305 -- We need to satisfy the hypotheses of `polynomial_form_forced`.
306 -- `hNorm0`: ∀ v, P 0 v = 2 * v.
307 -- We only have `P 0 (F y) = 2 F y`.
308 -- However, since P is a polynomial and F is non-trivial (has range with at least 0 and some non-zero value),
309 -- we can determine the coefficients.
310 -- P(0, v) = a + c*v + f*v^2.
311 -- P(0, 0) = a = 2*0 = 0 (from F(1)=0).
312 -- P(0, F y) = c*(F y) + f*(F y)^2 = 2*(F y).
313 -- This holds for y=1 (0=0) and some y where F y ≠ 0.
314 -- If we only have two points, we can't uniquely determine a quadratic.
315 -- But wait, `polynomial_form_forced` derived `a=0, c=2, f=0`.
316 -- Let's reproduce that logic but being careful about the domain.
317
318 obtain ⟨a, b, c, d, e, f, hP⟩ := hPoly
319
papers checked against this theorem (showing 30 of 83)
-
NICE learns invertible maps for exact density estimation
"log(pX(x)) = log(pH(f(x))) + log(|det ∂f(x)/∂x|)"
-
emcee sampler needs only 1-2 parameters tuned for MCMC
"One major advantage of the algorithm is that it requires hand-tuning of only 1 or 2 parameters compared to ∼N² for a traditional algorithm in an N-dimensional parameter space."
-
Debate lets humans judge complex AI answers
"In an analogy to complexity theory, debate with optimal play can answer any question in PSPACE given polynomial time judges (direct judging answers only NP questions)."
-
Random square masking sets new records on CIFAR-10 and SVHN
"cutout can be used in conjunction with existing forms of data augmentation and other regularizers"
-
Taxonomy and benchmarks map LLM code generation progress
"In addition, we present a historical overview of the evolution of LLMs for code generation and offer an empirical comparison using the HumanEval, MBPP, and BigCodeBench benchmarks"
-
New tokenizer lets LLMs beat diffusion models on visuals
"A novel lookup-free quantization approach that enables improving the visual generation quality of language models by learning a large vocabulary."
-
Diffusion models plan by denoising trajectories
"We show how classifier-guided sampling and image inpainting can be reinterpreted as coherent planning strategies, and demonstrate the effectiveness of our framework in control settings that emphasize long-horizon decision-making and test-time flexibility."
-
SPT-3G CMB spectra give H0 of 66.66 km/s/Mpc
"We present measurements of the temperature and E-mode polarization angular power spectra of the cosmic microwave background (CMB) from observations of 4% of the sky with SPT-3G... Combining our TT/TE/EE spectra with previously published SPT-3G CMB lensing results, we find parameters for the standard LCDM model consistent with Planck and ACT-DR6"
-
ReTool teaches LLMs to interleave code calls via outcome rewards
"synthetic cold-start data generation to produce code-augmented long-form reasoning traces"
-
Outcome RL trains LLMs to call search tools on demand
"we propose R1-Searcher, a novel two-stage outcome-based RL approach designed to enhance the search capabilities of LLMs"
-
3D model lets robots imagine futures before acting
"we propose 3D-VLA by introducing a new family of embodied foundation models that seamlessly link 3D perception, reasoning, and action through a generative world model. Specifically, 3D-VLA is built on top of a 3D-based large language model (LLM), and a set of interaction tokens is introduced to engage with the embodied environment."
-
VQ-VAE plus transformer matches GAN video quality
"Despite the simplicity in formulation and ease of training, our architecture is able to generate samples competitive with state-of-the-art GAN models for video generation on the BAIR Robot dataset"
-
LSUN builds one million images per category via human-AI labeling loop
"To assess the effectiveness of this cascading procedure... we construct a new image dataset, LSUN. It contains around one million labeled images for each of 10 scene categories and 20 object categories"
-
One transformer learns robot policies from video and action data
"a UWM integrates an action diffusion process and a video diffusion process within a unified transformer architecture, where independent diffusion timesteps govern each modality. By controlling each diffusion timestep, UWM can flexibly represent a policy, a forward dynamics, an inverse dynamics, and a video generator."
-
ACT DR6 data set baryon density at 0.0226 and H0 at 68.22
"We find that the ACT angular power spectra … are well fit by the sum of CMB and foregrounds, where the CMB spectra are described by the ΛCDM model. Combining ACT with larger-scale Planck data, the joint P-ACT dataset provides tight limits on the ingredients, expansion rate, and initial conditions of the universe … Ω_b h² = 0.0226 ± 0.0001, Ω_c h² = 0.118 ± 0.001, H_0 = 68.22 ± 0.36 km/s/Mpc, n_s = 0.974 ± 0.003, and σ_8 = 0.813 ± 0.005."
-
SAC reaches top performance with fewer samples and stable results
"We extend SAC to incorporate a number of modifications that accelerate training and improve stability with respect to the hyperparameters, including a constrained formulation that automatically tunes the temperature hyperparameter."
-
Bilby supplies simple Python tools for gravitational-wave parameter estimation
"Bilby provides expert-level parameter estimation infrastructure with straightforward syntax... for the analysis of compact binary mergers and other types of signal model"
-
Dark compact objects show no deviations from Kerr black holes
"Any observation suggesting otherwise would be an indication of beyond-the-standard-model physics. Null results strengthen and quantify the Kerr black hole paradigm."
-
Benchmarks teach language models to guess instead of saying they are unsure
"We argue that language models hallucinate because the training and evaluation procedures reward guessing over acknowledging uncertainty"
-
ALBERT sets new SOTA on GLUE, RACE and SQuAD with fewer parameters than BERT-large
"we present two parameter-reduction techniques to lower memory consumption and increase the training speed of BERT... our best model establishes new state-of-the-art results on the GLUE, RACE, and SQuAD benchmarks while having fewer parameters compared to BERT-large."
-
Sharing parameters across tasks boosts deep learning results
"Multi-task learning (MTL) has led to successes in many applications of machine learning, from natural language processing and speech recognition to computer vision and drug discovery. This article aims to give a general overview of MTL, particularly in deep neural networks. It introduces the two most common methods for MTL in Deep Learning, gives an overview of the literature, and discusses recent advances."
-
VAPO scores 60.4 on AIME 2024 with stable RL training
"VAPO, built on the Qwen 32B pre-trained model, attains a state-of-the-art score of 60.4. In direct comparison under identical experimental settings, VAPO outperforms the previously reported results of DeepSeek-R1-Zero-Qwen-32B and DAPO by more than 10 points."
-
Any three late-universe H0 methods yield 4-5.8 sigma tension
"combining any three independent approaches to measure H0 in the late universe yields tension with the early Universe values between 4.0σ and 5.8σ"
-
Autonomous agents give RAG dynamic retrieval and planning
"Agentic RAG transcends these limitations by embedding autonomous AI agents into the RAG pipeline. These agents leverage agentic design patterns reflection, planning, tool use, and multi-agent collaboration"
-
EVA-CLIP reaches 82% ImageNet accuracy with 9 billion samples
"Our approach incorporates new techniques for representation learning, optimization, and augmentation, enabling EVA-CLIP to achieve superior performance compared to previous CLIP models with the same number of parameters but significantly smaller training costs."
-
Rule rewards in RL give VLMs better generalization than SFT
"Experimental results indicate that the RL-based model not only delivers competitive performance on visual understanding tasks but also surpasses Supervised Fine-Tuning (SFT) in generalization ability."
-
Blended diffusion sampling solves noisy nonlinear inverse problems
"the resulting posterior sampling scheme is a blended version of diffusion sampling with the manifold constrained gradient without a strict measurement consistency projection step"
-
COCO supplies 1.5 million captions for 330k images
"The evaluation server receives candidate captions and scores them using several popular metrics, including BLEU, METEOR, ROUGE and CIDEr."
-
GLUE benchmark tests language models on nine tasks for general understanding
"We introduce the General Language Understanding Evaluation benchmark (GLUE), a tool for evaluating and analyzing the performance of models across a diverse range of existing NLU tasks."
-
Attention gates raise U-Net accuracy on CT pancreas scans
"AGs automatically learn to focus on target structures of varying shapes and sizes. Models trained with AGs implicitly learn to suppress irrelevant regions in an input image while highlighting salient features useful for a specific task. This enables us to eliminate the necessity of using explicit external tissue/organ localisation modules of cascaded convolutional neural networks (CNNs)."