symmetric_second_diff_limit_hypothesis
This definition packages the symmetric second difference limit hypothesis for functions H obeying the d'Alembert equation. Workers on the T5 J-uniqueness proof cite it when discharging regularity gaps inside washburn_uniqueness. The declaration is a direct Prop constructor that assembles the initial value, continuity, functional equation, derivative condition at zero, and the second-difference quotient limit statement.
claimLet $H : ℝ → ℝ$. The symmetric second difference limit hypothesis at $t$ asserts that if $H(0)=1$, $H$ is continuous, $H(t+u)+H(t-u)=2H(t)H(u)$ holds for all real $t,u$, and the derivative of $H$ at 0 equals 1, then the limit as $u→0$ of $(H(t+u)+H(t-u)-2H(t))/u^2$ equals $H(t)$.
background
The Cost.FunctionalEquation module supplies lemmas for the T5 cost uniqueness proof. Here H is the shifted cost reparametrization H_F(t) = G_F(t) + 1, which converts the Recognition Composition Law into the d'Alembert equation. The upstream dAlembert_continuous_implies_smooth_hypothesis records Aczél's classical result that continuous solutions with H(0)=1 are analytic and satisfy the ODE H''=H. This symmetric second difference limit hypothesis is one of five such regularity hypotheses that close gaps in washburn_uniqueness.
proof idea
The declaration is a direct definition of a Prop; it simply assembles the five listed assumptions and the Tendsto statement for the second-difference quotient. No lemmas or tactics are invoked beyond the built-in Filter.Tendsto and HasDerivAt constructors.
why it matters in Recognition Science
The definition supplies one of the five regularity hypotheses needed to finish the no-hypothesis version of washburn_uniqueness after the Aczél axiom is added. It therefore advances the T5 J-uniqueness step in the forcing chain, where the unique solution is forced to be the cosh form that yields the phi fixed point. The module documentation states that these hypothesis defs become provable once the single Aczél axiom is present.
scope and limits
- Does not prove the second-difference limit; it only defines the hypothesis.
- Does not apply outside the d'Alembert class with H(0)=1.
- Does not derive the ODE H''=H; that step uses separate smoothness results.
- Does not quantify over the parameter λ in the cosh solution.
formal statement (Lean)
859def symmetric_second_diff_limit_hypothesis (H : ℝ → ℝ) (t : ℝ) : Prop :=
proof body
Definition body.
860 H 0 = 1 → Continuous H → (∀ t u, H (t+u) + H (t-u) = 2 * H t * H u) →
861 HasDerivAt (deriv H) 1 0 → Filter.Tendsto (fun u => (H (t+u) + H (t-u) - 2 * H t) / u^2) (nhds 0) (nhds (H t))
862
863end Constructive
864
865/-! ## Aczél's Theorem and the ODE Derivation
866
867These results close the five regularity hypothesis gaps in `washburn_uniqueness`.
868After adding the single Aczél axiom, all five `_hypothesis` defs become provable, and
869a clean no-hypothesis version of the uniqueness theorem follows.
870-/
871
872/-- The `dAlembert_continuous_implies_smooth_hypothesis` holds for every H,
873 as a direct consequence of the Aczél axiom. -/