theorem
proved
washburn_uniqueness_aczel
show as:
view math explainer →
Reciprocal-symmetric cost has one solution: J(x) = ½(x + x⁻¹) − 1.
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 6004)
-
Two cases control distance product optimization in triangles
"Main Theorem. If ∆ is acute, φ has precisely three local maxima and three local minima. If ∆ is obtuse, then φ has either (i) three local maxima and three local minima, or (ii) four local maxima and four local minima."
-
Coordination types trade robustness for scalability in agent scheduling
"effectiveness, constraint alignment, coordination efficiency, and robustness"
-
Spike forecasting ranks brain regions consistently across models
"population metric decomposition that separates aggregate performance into temporal fidelity, spatial pattern accuracy, and magnitude-invariant alignment... pop_rate_r = Pearson(∑ y_i(t), ∑ ŷ_i(t)); spatial_r = (1/T) ∑ Pearson(y(t), ŷ(t)); cos_sim = (1/T) ∑ y·ŷ / (‖y‖ ‖ŷ‖)"
-
Early low progress raises dropout by 25 points in engineering
"time–capital misalignment hypothesis ... early trajectory misalignment between academic progress and system-imposed temporal constraints"
-
Diffusion model ranks beams from geometry to cut training overhead
"The learning objective is therefore to construct p̂_θ(b|x), a well calibrated, uncertainty-aware beam prior conditioned on compact features x∈R^d"
-
Left ideals give representation-free quantum graph morphisms
"We begin with the characterization of quantum graphs as left ideals in M ⊗_eh M ... to avoid technicalities surrounding representation dependence"
-
Data prep beats PDF tool choice in RAG accuracy
"Metadata enrichment and hierarchy-aware chunking contributed more to accuracy than the conversion framework choice alone."
-
MoSe2/PdSe2 stack lifts A-exciton emission sixfold
"pronounced ∼6-fold enhancement of room-temperature A-exciton emission in a type-I MoSe₂/PdSe₂ van der Waals heterostructure... interlayer electronic coupling that redistributes exciton populations"
-
Signal precision can lower screening accuracy when high
"s=e+ϵ/ρ ... C(e,θ)=e/θ ... marginal benefit fρ(τ−e) single-peaked ... threshold ˆθ solving 1−Fρ(τ−0)=1−Fρ(τ−ê)−ê/θ"
-
Twisted contraction yields magnetic Carroll supersymmetry
"the resulting structure contains one supercharge that squares to spatial momentum, a mixed anticommutator that yields the Hamiltonian, and a nilpotent second supercharge"
-
Single LISA-like detector measures gravitational-wave memory at SNR 10+
"the low frequency spectrum can be described by a corrected soft waveform of displacement memory... ˜h∞(f)→iΔh/(2πf)e2πift∗"
-
Ultrasound identifiability set by forward structure and variability
"the forward map from correlation length D and texture-coherence parameter T to the attenuation and velocity observables remains structurally full rank. However, the sensitivity geometry is strongly anisotropic... variance-weighted Fisher framework"
-
Localized kick extraction enables 3D proton FLASH scanning
"For each scanning spot, the functional region of the kicker along the longitudinal direction is dynamically adjusted based on real-time beam longitudinal line density measured by a beam current monitor. The corresponding region-determination algorithm is provided."
-
Multislot 5G NR meets UAV sensing accuracy targets
"The compact CRLB expressions derived in this work highlight the fundamental trade-offs between estimation accuracy and system parameters... V AR(ˆd)≥Γ·1/Δf²·1/(1/NA∑q q²−(1/NA∑q q)²)"
-
Mapping class subgroups have dense Teichmüller lengths
"λgnhn / (λng λnh) → [g+, h+, g−, h−] as n→+∞"
-
Bumblebee gravity turns black hole shadows into teardrops
"the line element is given by [44]: ds²(g) = ... with X=ξb² ... photon sphere radius ... identical to that of the Kerr metric (eq. 16)"
-
Fermi golden rule clarified for chemical physics rates
"Fermi’s golden rule (FGR) is the simplest but most widely used theory for calculating rates of quantum transitions... kF,j→f = 2π/ℏ |⟨ψf | Ĥc|ψj⟩|^2 δ(Ej − Ef)"
-
Multi-virtual twin groups admit exactly eight 2-local representation types
"The twin group Tn ... far commutation relations ... virtual twin group VTn ... multi-virtual twin group MkVTn"
-
Infinitesimals formalized without axiom of choice
"SPOT has the following three axioms... T(Transfer)... O(Nontriviality)... SP(Standard Part)"
-
Student nets beat teachers with 10x fewer parameters using hints
"a deep student network with almost 10.4 times less parameters outperforms a larger, state-of-the-art teacher network"
-
Dynamical metric order quantifies map complexity in infinite dimensions
"mdimmo(X,d,f) = lim sup ε→0+ log+ (lim sup n→∞ (1/n) log S(X,n,ε)) / |log ε|; variational principle mdimmo = max μ∈Pf(X) mdimmo(X,d,f,μ) with equilibrium states always exist"
-
Four-face SiPM readout hits 68 ps timing resolution
"multi-face readout topology, utilizing low-capacitance 4-series (4S) SiPM modules coupled to four faces of the scintillator, achieves an excellent coincidence time resolution of approximately 68 ps"
-
Wide binaries disrupt rapidly in first 10 Myr of cluster evolution
"We perform simulations containing 10,000 objects with varying binary fractions and initial bulk rotation... propose two semianalytical models... exponential model... broken power-law model"
-
Muons' synchrotron radiation spares current axion searches
"GEANT4 simulation of muon tracks... analytical estimation of angular-frequency-differential synchrotron radiation power spectra... Eq. (2)–(4) with Bessel Jn"
-
Role-playing turns chat models into cooperative agent teams
"We introduce a novel cooperative agent framework, role-playing, that allows communicative agents to collaborate autonomously toward completing tasks"
-
Diffusion model downscales weather forecasts to 30 km with added skill
"The approach transforms low-resolution ensemble forecasts into high-resolution ensembles by learning the conditional distribution of finer-scale residuals... diffusion model... EDM sampler"
-
Efficiency turns video generators into world simulators
"Efficient modeling paradigms, efficient network architectures, and efficient inference algorithms"
-
Mechanical feedback alone creates active growth layers at cell colony edges
"Coarse-graining the model yields a continuum description with no adjustable parameters... ∇²p(r,t) = 1/χ² (p(r,t) − p_c)"
-
LHS 3844 b weighs 2.27 Earth masses with rocky density
"We explore 15 competing RV models that differ in their treatment of correlated stellar variability (through different Gaussian Process kernels) and long-term drifts. ... From the evidence-weighted posterior samples we derive a planetary mass of 2.27 ± 0.23 M⊕"
-
Rank-3 lifts force Ω(q^8) cross-ratio defects in plane matrices
"leading derangement equation together with its first-order companion"