theorem
proved
costAlphaLog_high_calibrated_iff
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 155.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
152 deriv (deriv (deriv (deriv G))) 0 = 1
153
154/-- The α-cost is high-calibrated iff `α² = 1`. -/
155theorem costAlphaLog_high_calibrated_iff (α : ℝ) (hα : α ≠ 0) :
156 IsHighCalibratedLog (CostAlphaLog α) ↔ α ^ 2 = 1 := by
157 unfold IsHighCalibratedLog
158 rw [costAlphaLog_fourth_deriv_at_zero α hα]
159
160/-! ## The α-pin -/
161
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
papers checked against this theorem (showing 30 of 38)
-
Hyperbolic coupling matches LP complexity for multiconic problems
"Φ(z) = F(x(z)) + F*(s) ... 2ν-logarithmically homogeneous ... self-concordant barrier for C(K) with parameter 2ν"
-
New logic QLL turns constraints into neural losses that match verifiers
"∪p and ∩p ... converge to min/max as p→∞ ... partial derivatives never vanish ... shadow-lifting."
-
Optical torque tunes nonlinear metasurface emission
"nonlinear temporal coupled-mode theory (NTCMT) ... d a / d t = −(iω1 − γ1)a + ... − i (κ/3)(a*)²b"
-
Variable Loads May Raise MV Cable Maintenance 10-300x
"Montsinger ... r(T) = 2^{(T-Tr)/ΔT}; Arrhenius r(T) = exp(B(1/Tr-1/T))"
-
Product TV distance bounded below by constant times averaged version
"admissible measures closed under convolution; mass-defect α and multilinear Ψ representation"
-
Memory functional strictly contains continuous functions
"Λ_f satisfies ||Λ_f - Λ_g||_∞ ≤ L_Λ ||f-g||_∞ and positivity at zero; historical deviation accumulation interpolates instantaneous vs history-dependent sensitivity"
-
Kolmogorov-Nagumo means capture more conditional entropies
"Definition 11 (EPKNAVG) and Lemma 1 using concavification of F by ψ"
-
Laplace kernel captures feature correlations for data-free continual learning
"the resulting covariance parameterization takes the form Σ = diag(d) + diag(w)K(a)diag(w)"
-
MDL selects among ball models for boundary-aware classification
"The intrusion penalty is defined as Lintr(B,c)=nB[−ln max(1−ρ¯(B,c),ϵnum)] ... margin penalty ... ω(B,c)=max{0,r˜B−δ−c(μB)}/r˜B"
-
Vector codebook cuts KV cache to 34x compression at 0.95 similarity
"Lemma 1 (Spherical-Beta vector marginal)... R² ~ Beta(k/2,(d-k)/2)... X/R uniform on S^{k-1}"
-
Acoustic force quantifies single-condensate viscoelasticity
"G'(f) = σo/εo(f) cos δ(f), G''(f) = σo/εo(f) sin δ(f); Maxwell interior + interfacial G_γ"
-
Frequency modules lift transformer accuracy on 3D medical scans
"FGMLP... selective frequency decomposition mechanism... low-frequency and high-frequency components"
-
Tail extrapolation approximates best-of-N gradients from m much smaller than N
"Assumption 1. ... the upper 2α tail of the reward distribution is Gaussian, namely pθ,x(r) = ϕ(r; μθ(x), σ²θ(x)), r ≥ rθ,2α(x)"
-
Adaptive KL scaling and Gaussian sampling lift LLM math pass@32
"Gaussian curriculum ... exp(−(˜p−0.5)²/2σ²)"
-
Physics sim from hand forces reconstructs deformable objects
"the force on each mass node ni is modeled as: Fi = Σ Fspring + Fdamping + Fexternal ... vt+1 = vt + Δt Fi/mi"
-
Contractive law adapts Koopman models online safely
"δ+k := vmax Ēk (1 + η vmax √w) … CBF constraint h(xnomk+1) ≥ (1−α)h(xk) + Lh δk"
-
MHD projection sliced to 1D Brent minimization
"Lemma 3.6. The mapping β↦d₂(β) is continuous on [0,+∞). ... d₂(β) is strictly convex"
-
Affective drift triggers abrupt collapse in conversation repair
"entropy-regularized best response … quantal response equilibrium"
-
RKU pruning sustains reasoning at 40% sparsity in LLMs
"Riemannian manifold pre-conditioning … ˜U(c)AGF ≈ |Yc|√Hcc / Trace(√H)"
-
Non-parametric rehearsal learning avoids assumptions on data processes
"wη(y) ≜ ∏ Φ(η(bk − m⊤k y)) ... approximation error bound O(√ln η / η)"
-
Machine-learned Fermi expansions speed density matrices 10x on GPUs
"affine rescaling H0= (β'/β0)(H'-μ'I)+μ0 I... region of validity defined by μ0/μ' β0 ≥ β' and (1-μ0)/(1-μ') β0 ≥ β'"
-
Quadratic latents uncover manifolds linear autoencoders miss
"z_i := x^T L^T diag(c_i) R x = <W_i, X>_F ... kernel trick... reconstruction of X=xx^T"
-
Bayesian method jointly infers brown dwarf map and geometry
"Σ_a[j,j′] = σ_a² exp(−d_jj′²/(2ℓ²))"
-
New algorithm achieves sublinear regret for robust Bayesian optimisation
"Lemma 4.1. For an h-smooth function f, ∀x∈X, ∀Q∈B_εt(Q_t) ... |E_{c~Q}[f(x,c)] - E_{c~Q_t}[f(x,c)]| ≤ ε_t ∥∇_c f∥_{Q_t,2} + ε_t² h(x)/2"
-
Ultrasound triggers self-similar microjets in vaporizing droplets
"Evaporative instabilities... dispersion relation Ω² + ... = 0 (Eq. 5) and instability condition Ṙb⁴ > 4γ R̈b / χ²(ρd − ρv) (Eq. 6)"
-
CORDIC iteration depth trims 33 percent of inference cycles
"unified CORDIC algorithm... hyperbolic rotation mode to compute sigmoid and tanh"
-
Dirac operator gains weighted L2 solvability for power and Gaussian weights in n≥3
"sharp constant 1/4 in the Gaussian case"
-
Heat regularization keeps continuation solvable at nonsmooth minima
"the asymptotic behavior of the regularized Hessian is determined by the local profile of the original objective: it remains uniformly positive definite in the quadratic case a=2, while in the subquadratic regime 1≤a<2 its smallest eigenvalue grows at the controlled rate t^{(a-2)/2}"
-
Classical algorithm samples noisy IQP circuits in polynomial time
"amplitude-damping channel... unique fixed point... pushes states toward low Hamming-weight subspace"
-
Bounded ratio keeps language model alignment stable and consistent
"LRDRE(θ)=E[ Bregf(r∗∥rθ) ] ... φ(t)=log(1+exp(t)) ... CLip=L1+(1/α)L2"