theorem
proved
alpha_pin_under_high_calibration
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.Foundation.AlphaCoordinateFixation on GitHub at line 165.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
162/-- **The α-pin theorem.** Within the bilinear `α`-family with the
163rigidity-paper convention `α ≥ 1`, higher-derivative calibration forces
164`α = 1`. -/
165theorem alpha_pin_under_high_calibration
166 (α : ℝ) (h_pos : 1 ≤ α)
167 (h_calib : IsHighCalibratedLog (CostAlphaLog α)) :
168 α = 1 := by
169 have hα_ne : α ≠ 0 := by linarith
170 have hα_sq : α ^ 2 = 1 :=
171 (costAlphaLog_high_calibrated_iff α hα_ne).mp h_calib
172 -- α ≥ 1 and α² = 1 forces α = 1.
173 nlinarith
174
175/-! ## J is the unique high-calibrated bilinear cost -/
176
177/-- The `α = 1` bilinear cost is exactly `Jcost`. -/
178theorem alpha_pinned_to_one_implies_J (x : ℝ) (hx : 0 < x) :
179 CostAlpha 1 x = Jcost x :=
180 cost_alpha_one_eq_jcost x hx
181
182/-- **The full uniqueness theorem.** Within the bilinear `α`-family,
183under the convention `α ≥ 1`, higher-derivative calibration forces
184`α = 1`, and the cost on positive reals is exactly `Jcost`. -/
185theorem J_uniquely_calibrated_via_higher_derivative
186 (α : ℝ) (h_pos : 1 ≤ α)
187 (h_calib : IsHighCalibratedLog (CostAlphaLog α)) :
188 ∀ x : ℝ, 0 < x → CostAlpha α x = Jcost x := by
189 intro x hx
190 have hα_eq : α = 1 := alpha_pin_under_high_calibration α h_pos h_calib
191 rw [hα_eq]
192 exact cost_alpha_one_eq_jcost x hx
193
194/-! ## Headline Certificate -/
195
papers checked against this theorem (showing 30 of 170)
-
Normalization creates point identification unless parameter is class-constant
"Definition 3 (Normalization) … selects exactly one representative from each equivalence class … induces a bijection between Q∼ and the normalized parameter space"
-
Radial symmetry forges triality among Riccati, Schrödinger and HJB equations
"0 < ϕ(r) < g(r) … lim r→∞ ϕ(r) = √L / σ² (Corollary 5.4, Proposition 4.2)"
-
Mixed-density synthetic fog at 75% scale beats full fixed-density training
"tenfold increase over the default fine-tuning learning rate overcomes negative transfer"
-
Reference plan selectively weights tokens in failed rollouts
"σi,t := log πθ(y⋆i,t | qi, Si, y⋆i,<t) / πθ(y⋆i,t | qi, y⋆i,<t) ... plan-regret bound under Assumption 3"
-
Naive LLM confidence intervals are 40-60% too narrow
"D-study projections... cost-efficiency frontier for safety evaluation (Fig. 4)"
-
Distillation turns reranker into linear-time retriever
"We adopt the JEPA paradigm, where a predictor first converts the query embedding into a new latent space with the document embedding played as the latent control"
-
Temperature adjustment turns reward models into a calibrated SLOP
"reference-model temperature adjustment leading to sharpened logarithmic opinion pool"
-
Gap counting sets critical scale for attention softmax
"Corollary 4.9 (Coordinate decomposition of ξ_Λ). ... ξ_Λ = ξ_α - ξ_Δ + 1."
-
Adaptive multi-marginal couplings cut MCMC meeting times by half
"Adaptive Proposal for Fast Coupling... mixture barycenter measure μ ≜ 1/C ∑ Pj"
-
D-optimal irregular sampling boosts FRF estimate accuracy
"Maximizing the determinant of the FIM E[Φ^H_N Φ_N] = A^H R_0 A"
-
Thermal cameras fingerprint VR apps remotely
"thermal drift... per-cell temperature statistics... spatial gradients... baseline-derived temporal-delta subtraction"
-
Correlation-driven tunability of altermagnetism in RuO$_2$
"the AM solution is not stabilized unless U is sufficiently large... itinerant-to-localized crossover"
-
Post-AGB disc inner rims show diverse substructures
"The inner disc regions are highly diverse and dynamic, harbouring a significant amount of substructure candidates"
-
Dimer fields remove cutoff dependence in nucleon scattering EFT
"The systematic inclusion of dimer fields as propagating degrees of freedom in the effective theory to account for those poles results in cut-off insensitive fits at order Q^0"
-
Black hole mass fixed at 4 million suns in Milky Way center
"12-dimensional parameter space... MCMC... 30 walkers"
-
Rashomon set turns many good embeddings into one reliable visualization
"PCA-informed alignment ... Ltotal = LDR + λPCA · E[i∉kNN(j)] [(1 - ⟨y1-y2, yPCA,1-yPCA,2⟩ / (∥y1-y2∥∥yPCA,1-yPCA,2∥))²]"
-
SVD factors cut LLM training memory 199x
"all ranks converge to the same loss floor ... identifying the learning rate schedule—not MLP rank—as the primary bottleneck"
-
Recombination freeze-out leaves relic EM field peaked at 10-20 Mpc
"By a canonical transformation, the reduced evolution equation is recast into a forced oscillator with a smooth effective potential"
-
Recipe embeddings already encode 15 flavor dimensions
"An LLM-augmented curation pipeline consolidates 6,653 raw FlavorGraph ingredients into 1,032 canonical entries... using Gemini 3.1 Pro with structured JSON output."
-
Pseudo-RGB format raises physical consistency in video diffusion
"parallel branches... pixel-wise consistency... single-stream student"
-
Calibrated rewards lift 4B model past GPT-4 on airline tasks
"GTPO hybrid advantage formulation eliminates the advantage misalignment problem... Ahybrid i,k = GN(∑ γ^{l-k} r_{i,l} + γ^{K-k} o_i) + λ · A^O_i (λ=0.3)"
-
Self-consistent matching sharpens video at 2-4 steps
"Cache-conditioned feature alignment L_align on relational matrices R_low and R_ref for mixed K∈{2,4,8} rollouts."
-
Satellite fusion lifts radar nowcasts of intense storms 48 percent
"IR 10.8 dominates intensity-relevant attribution ... BTD helps suppress false alarms"
-
Sketch-based GPU solver handles 5000-asset portfolios in seconds
"STR pipeline... ridge stabilization... conditioning improvement"
-
ERM projections convolve non-Gaussian and Gaussian parts
"any C² regularizer is asymptotically equivalent to a quadratic form determined solely by its Hessian at zero and gradient at μ̂θ"
-
Noise injection turns diffusion denoisers into plug-and-play generative priors
"SGPnP iteration x_{k+1}=x_k - γ_k (∇g + U_σk), annealed σ_k→0 yields convergence to critical point of un-smoothed f_0 (Thm 2, Assump 4)"
-
Human-Robot Copilot for Data-Efficient Imitation Learning
"xf =α(x l −c l) +c t,(1) ... for precision-demanding tasks, such as object insertion, a smaller scaling factor (α= 0.5) is adopted"
-
ODEs recover any-regularization solutions in semi-discrete transport
"uniform boundedness of ψ(t)/t when F* m-strongly convex; continuity at t=1 via local uniform convergence of ∇K"
-
BWTA quantization nears full-precision BERT accuracy at 16-24x GPU speed
"Smooth Multi-Stage Quantization... Levelwise Degradation Strategy... {L0, L1, ..., Ll} with Ll=1"
-
LLM embeddings fused and aligned boost tail-item recommendations
"dual-level alignment... item-level contrastive... feature-level... curriculum learning scheduler"