theorem
proved
dAlembert_cosh_solution_aczel
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Cost.FunctionalEquation on GitHub at line 1053.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
-
H -
reciprocal -
aczel_dAlembert_smooth -
AczelSmoothnessPackage -
dAlembert_even -
dAlembert_to_ODE_theorem -
even_deriv_at_zero -
H -
ode_cosh_uniqueness_contdiff -
dAlembert_cosh_solution_aczel -
dAlembert_to_ODE_theorem -
h_even -
reciprocal -
cost -
cost -
is -
from -
is -
is -
is -
calibration -
and
used by
formal source
1050 solution to d'Alembert with H(0) = 1 and H''(0) = 1 must equal cosh.
1051
1052 This is the clean version of `dAlembert_cosh_solution`, requiring no regularity params. -/
1053theorem dAlembert_cosh_solution_aczel
1054 [AczelSmoothnessPackage]
1055 (H : ℝ → ℝ)
1056 (h_one : H 0 = 1)
1057 (h_cont : Continuous H)
1058 (h_dAlembert : ∀ t u, H (t+u) + H (t-u) = 2 * H t * H u)
1059 (h_d2_zero : deriv (deriv H) 0 = 1) :
1060 ∀ t, H t = Real.cosh t := by
1061 have h_smooth : ContDiff ℝ ⊤ H := aczel_dAlembert_smooth H h_one h_cont h_dAlembert
1062 have hDiff : Differentiable ℝ H :=
1063 (h_smooth.of_le le_top : ContDiff ℝ 1 H).differentiable (by decide : (1 : WithTop ℕ∞) ≠ 0)
1064 have h_even : Function.Even H := dAlembert_even H h_one h_dAlembert
1065 have h_H'0 : deriv H 0 = 0 := even_deriv_at_zero H h_even hDiff.differentiableAt
1066 have h_ode : ∀ t, deriv (deriv H) t = H t :=
1067 dAlembert_to_ODE_theorem H h_smooth h_dAlembert h_d2_zero
1068 have h_C2 : ContDiff ℝ 2 H := h_smooth.of_le le_top
1069 exact ode_cosh_uniqueness_contdiff H h_C2 h_ode h_one h_H'0
1070
1071/-- **Theorem (Washburn, clean form)**: The J-cost function is the unique
1072 reciprocal cost satisfying the RCL, normalization, calibration, and continuity.
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
papers checked against this theorem (showing 15 of 15)
-
Polar flow matching adapts graphs while preserving topology
"Hyperbolic (H, c <0 ):The volume expands exponentially, satisfying: lim R→∞ Vol(BH(R))/exp((d−1)√|c|R) =const>0. ... Theorem 4.2 ... gradient flows for structural preservation (∇rL) and semantic alignment (∇θL) are orthogonal under the Riemannian metric: ⟨∇rL,∇θL⟩g=0."
-
Local Bernstein bounds extend Erdős lower bounds to short intervals
"Theorem 1.6 (Local Bernstein theory) … |f(x+iy)| ≤ A (1+O(e^{-πL/4y0})) cosh((1+O(1/(λ min(y0,L)))) λ y)"
-
Single-qubit process tomography reduces to linear regression
"the density matrix belongs to the quantum exponential family with the Pauli matrices serving as sufficient statistics... the BKM metric corresponds to the Hessian of the exponential family potential"
-
Newton methods converge superlinearly with nonlinear preconditioning
"ϕ(x)=cosh(|x|)-1 ... Assumption 2.2 holds relative to ϕ with constant LH"
-
Hyperbolic space gives fonts a radial style-specificity score
"entailment cones... aperture aper(x) = sin⁻¹(2K√c ∥x_space∥)... wider cones near the origin and narrower cones farther away... radial distance from the origin quantifies... style specificity"
-
Phase shift of π maps Fermi-Hubbard to Bose-Hubbard at imaginary μ
"g_B(x, ϕ) = sinh x / (cosh x − cos ϕ) and g_B(x, ϕ) = g_F(x, ϕ + π) (Eqs. 36, 76)"
-
Dual-manifold attention resolves 3D captioning trade-off
"GHL (x,y) = 1/√c arcosh(−c⟨x,y⟩L)"
-
Dual-stream radar model reaches 80.5% sign language accuracy
"explicit decibel-to-linear inversion ... Rlin = 10^(RdB/20) ... windowed FFT ... avoiding harmonic artifacts that arise from the spectral analysis of log-compressed signals"
-
HyRo decouples hyperbolic alignments for better segmentation
"HyRo aligns hierarchical levels by adjusting the hyperbolic radius and refines semantic relationships through angular alignment using an orthogonal transformation that theoretically preserves the hyperbolic radius."
-
Galileon lacks stable acceleration attractors in phase space
"We consider a Galileon scalar field endowed with a cosh type potential... V(ϕ)=V0[cosh(αϕ/Mpl)−1]p ... Γ=1−1/(2p)+pα²/(2λ²)"
-
Memory curvature causes net transport in irrotational flows
"Am(t) = ∫ K(τ) ∇u(t−τ) dτ ... [Am(t1),Am(t2)] ≠ 0 ... ℛ(t1,t2) = ∬ K(τ1)K(τ2)[∇u(t1−τ1),∇u(t2−τ2)] dτ1dτ2"
-
2D higher-spin gravity yields infinite tower of massive scalars
"M²(k)=M² cosh²(k/2) ... exponential basis (3.10)"
-
Slightly subcritical agents enable collective criticality
"L(p_micro, v_r) = |α_S − 1.5| + |α_T − 2| + KS_S + KS_T ... reference values 1.5 and 2 correspond to the classical critical exponents predicted by simple branching-process models"
-
Unconditional tangent scores bound conditional diffusion error by mutual information
"We analyze this issue through a normal–tangent decomposition of the score function. For Gaussian noising, the observed-direction score is exactly determined by the measurement; only the tangent conditional score is unknown."
-
A Noble-Gas-Centered Coordinate for Within-Period Atomic Property Trends
"Appendix A: J(xy) + J(x/y) = 2J(x)J(y) + 2J(x) + 2J(y) ... unique solution J(x) = ½(x+x⁻¹) − 1 = cosh(ln x) − 1 (Corollary 3.1 of Ref. [5])"