theorem
proved
washburn_uniqueness_aczel
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Cost.FunctionalEquation on GitHub at line 1076.
browse module
All declarations in this module, on Recognition.
explainer page
Derivations using this theorem
depends on
-
H -
G -
G -
AczelSmoothnessPackage -
composition_law_equiv_coshAdd -
CoshAddIdentity -
CoshAddIdentity_implies_DirectCoshAdd -
dAlembert_cosh_solution_aczel -
DirectCoshAdd -
G -
G_zero_of_unit -
H -
IsCalibrated -
IsNormalized -
IsReciprocalCost -
Jcost_G_eq_cosh_sub_one -
SatisfiesCompositionLaw -
dAlembert_cosh_solution_aczel -
washburn_uniqueness_aczel -
IsNormalized -
G -
Cost -
F -
F -
F
used by
formal source
1073
1074 This version uses the global Aczél axiom internally and requires NO regularity
1075 hypothesis parameters from the caller. -/
1076theorem washburn_uniqueness_aczel (F : ℝ → ℝ)
1077 [AczelSmoothnessPackage]
1078 (hRecip : IsReciprocalCost F)
1079 (hNorm : IsNormalized F)
1080 (hComp : SatisfiesCompositionLaw F)
1081 (hCalib : IsCalibrated F)
1082 (hCont : ContinuousOn F (Set.Ioi 0)) :
1083 ∀ x : ℝ, 0 < x → F x = Cost.Jcost x := by
1084 intro x hx
1085 have hSymm : ∀ {y}, 0 < y → F y = F y⁻¹ := fun {y} hy => hRecip y hy
1086 have hCoshAdd : CoshAddIdentity F := composition_law_equiv_coshAdd F |>.mp hComp
1087 let Gf : ℝ → ℝ := G F
1088 let Hf : ℝ → ℝ := H F
1089 have h_G0 : Gf 0 = 0 := G_zero_of_unit F hNorm
1090 have h_H0 : Hf 0 = 1 := by
1091 show H F 0 = 1
1092 simp only [H, G, Real.exp_zero]
1093 rw [hNorm]; ring
1094 have h_G_cont : Continuous Gf := by
1095 have h := ContinuousOn.comp_continuous hCont continuous_exp
1096 have h' : Continuous (fun t => F (Real.exp t)) :=
1097 h (by intro t; exact Set.mem_Ioi.mpr (Real.exp_pos t))
1098 simp [Gf, G] at h'
1099 exact h'
1100 have h_H_cont : Continuous Hf := by
1101 simpa [Hf, H] using h_G_cont.add continuous_const
1102 have h_direct : DirectCoshAdd Gf := CoshAddIdentity_implies_DirectCoshAdd F hCoshAdd
1103 have h_dAlembert : ∀ t u, Hf (t + u) + Hf (t - u) = 2 * Hf t * Hf u := by
1104 intro t u
1105 have hG := h_direct t u
1106 have h_goal : (Gf (t + u) + 1) + (Gf (t - u) + 1) = 2 * (Gf t + 1) * (Gf u + 1) := by
papers checked against this theorem (showing 30 of 9215)
-
Regularizers fix multimodal representation collapse
"intra-modal dispersive regularization … Ld = log(1/B(B−1) ∑ exp(−t‖z̃mi − z̃mj‖²)) … inter-modal anchoring La = 1/B ∑ (‖z̃mi − z̃ni‖² − τ)²₊"
-
Symmetric equilibrium exists in distributional competitions
"I establish existence of a symmetric equilibrium... characterization via the first-order approach... convex cost... Gâteaux differentiable... Φ(F, x) = a_F(x) − c_F(x) ≤ λ_g ... equal on supp(dF)"
-
Mixup foundation model beats priors by 14% in cross-domain HSI few-shot tasks
"coalescent projection (CP) ... single learnable matrix ... SA(U) = Softmax(Q C K^T / sqrt(D')) V"
-
Global embeddings collapse distinct subject-context cases
"Context-Selective Residuals (CSR)... Compatibility Reasoning Module (CRM) fuses... text-conditioned attention"
-
Two networks explain spider silk yield and recovery
"The response is decoupled into two parallel networks: (1) an elasto-plastic network of inter- and intramolecular bonds ... and (2) an elastic network of entropic chains"
-
FIT framework processes LLM deletion streams without utility loss
"FIT stabilizes sequential updates through three synergistic mechanisms: redundancy Filtering, Importance-aware adaptive algorithm selection, and Targeted layer attribution."
-
Low-rank latent space stabilizes MoE expert routing
"SIPS ... explicitly control the Lipschitz behavior of routing functions, yielding smoother and more stable routing geometry"
-
Silicon array resolves fission excitation energy to 800 keV
"An excitation energy resolution of 800 keV (FWHM) was determined together with mass resolution of 1.1% (FWHM)."
-
CALM halves biased errors in two-speaker ASR
"speaker embedding-driven target-speaker extraction and dynamic vocabulary-based contextual biasing... FiLM-based modulation... weighted softmax... CTC self-conditioning"
-
Hyperspherical autoencoder reaches 1.96 gFID with 25.2 dB PSNR
"semantic information in contrastive representations is primarily directional... Cosine Similarity Alignment objective that enforces semantic consistency while allowing flexible feature magnitudes"
-
Scrambling generates entanglement to beat quantum sensing limit
"we experimentally establish a connection between the enhanced sensitivity and the dynamics of the out-of-time-order correlator (OTOC), and show that the buildup of scrambling-induced genuine multipartite entanglement underlies the observed sensitivity enhancement"
-
Perceptron forces attention critical points to localize on sphere
"the system can even be seen as a gradient flow for an explicit energy... critical points are generically atomic and localized on subsets of the sphere"
-
Counterfactual augmentation lifts temporal link prediction
"We propose a dynamic network learning framework CoDCL, which combines counterfactual-inspired augmentation with contrastive learning... dynamic treatments design with efficient structural neighborhood exploration"
-
Model shifts bare 2S state to Roper resonance mass
"when the model parameters are calibrated to match the 1P-wave spectrum and their widths, the pole associated with the bare 2S state is naturally shifted downward to the mass region of physical Roper resonance–N(1440)"
-
Pore loses all selectivity at bulk azeotrope composition
"neural LMFT framework... single-component repulsive reference system with a mean-field treatment of attractive interactions, inspired by the connection between cDFT and local molecular field theory"
-
DNA microgels swell twofold and dissolve on specific cue
"We present a biocompatible fabrication and characterization platform for micron-scale DNA-hydrogels (µSDs) with tunable isotropic swelling and dissolving properties... achieving up to a two-fold size increase through programmable DNA design parameters."
-
New benchmark scores virtual try-on at 0.833 human correlation
"multi-modal protocol that measures VTON quality along five interpretable dimensions... VLM-based semantic reasoning with a novel Multi-Scale Representation Metric based on SAM3 segmentation and morphological erosion"
-
Continued fractions halve parameters in large language models
"continued fraction ... w0x + 1/(w1x + 1/(w2x + ...)) ... 1/x non-linearity ... continuants Kd ... ∂f̃/∂ak = (−1)^k (Kd−k/Kd)^2"
-
Exact moment matching derived for residual network activations
"We derive exact first and second moment matching for propagating the mean and covariance matrix of a Gaussian distribution through a single layer of a (residual) neural network (Lemma 2.4). ... for probit in App. C ... GeLU in App. D ... ReLU ... Heaviside ... sine"
-
Relativistic model matches all heavy-meson data
"the Hamiltonian describing the spectrum of heavy mesons in the relativistic potential model is the sum of three terms, H = H(0) + ΔH(0) + ΔH(S), where the leading contribution H(0) reads H(0) = h1 + h2 + Ug(r) + Uconf(r), h1 = sqrt(m1² + p²), … Ug(r) = −g/r, Uconf(r) = br + C"
-
Riemannian subspaces model discrete data in low dimensions
"We equip the parameter domain with a Riemannian geometry such that the latent subspace and induced data manifold are related by isometries... geodesics become straight lines in the latent parameter space"
-
Noise tweaks revive concepts erased from image generators
"IVO optimizes initial latent variables to realign the noise distribution of unlearned models with that of their vanilla counterparts, which reconstructs the fractured mappings"
-
Metropolis samplers gain explicit gaps on non-smooth targets
"Proposition 3.2 and Theorems 4.2–4.6: Gap(P) bounded via Cheeger + Υ(δ) F(min π(Si)) from isoperimetric profile of π"
-
Calcium pairing gaps stay too small after chiral tuning
"Bayesian posterior sampling in a delta-full chiral effective field theory at third chiral order"
-
Dataset adds continuous valence-arousal scores to multilingual ABSA
"we adopt a dimensional approach that represents sentiment with continuous valence-arousal (VA) scores... propose a new unified metric, continuous F1 (cF1), which incorporates VA prediction error into standard F1"
-
CNN on Circos plots classifies SARS-CoV-2 variants at 98.7% F1
"DCA-inferred pairwise mutational couplings were transformed into Circos images, which were then used as inputs for CNN-based classification models... weighted-average F1-score of 98.68±0.75%"
-
Manifold projection makes CFG less sensitive to scale in flow models
"We demonstrate that the velocity field in flow matching corresponds to the gradient of a sequence of smoothed distance functions... reformulate the CFG sampling as a homotopy optimization with a manifold constraint."
-
LLM semantics transfer preferences across recommendation domains
"Extensive experiments on real-world datasets show that SemaCDR consistently outperforms state-of-the-art baselines"
-
LLM providers gain from excess test-time compute
"the payment is given by P(θ,p) = q_π(1)(θ_π(1)) - V_π(2)(θ_π(2), p_π(2))"
-
Minimizing monotone residuals solves Hamilton-Jacobi equations
"Under assumptions (H1)-(H3), ... DR(u) is μ-diagonally dominant ... Therefore, DR(u) is invertible with ∥(DR(u))⁻¹∥ ≤ 1/μ. ... 0 ∈ ∂L(u) iff R(u) = 0"