representation_formula
The representation formula recovers any continuous solution H of the d'Alembert equation at an arbitrary point t from symmetric differences of its antiderivative Φ at t±δ, scaled by Φ(δ). Analysts working on regularity theory for functional equations cite this identity to start the bootstrap from continuity to C^∞. The proof integrates the functional equation over [0,δ] for both positive and negative shifts, applies the fundamental theorem of calculus to equate those integrals to differences of Φ, and solves the resulting linear relation after
claimLet $H : ℝ → ℝ$ be continuous and satisfy $H(t+u) + H(t-u) = 2 H(t) H(u)$ for all real $t,u$. Let $Φ(t) := ∫_0^t H(s) ds$. Then for any $δ$ with $Φ(δ) ≠ 0$ and any $t$, $H(t) = [Φ(t+δ) - Φ(t-δ)] / (2 Φ(δ))$.
background
In the cost algebra the shifted function H(x) = J(x) + 1 converts the Recognition Composition Law into the additive d'Alembert equation H(t+u) + H(t-u) = 2 H(t) H(u). The module proves every continuous solution with H(0)=1 is C^∞ by an integration bootstrap that begins with the antiderivative Φ(H,t) = ∫_0^t H(s) ds. Upstream lemmas establish that Φ is differentiable with derivative H (phi_hasDerivAt) and that Φ(0)=0 (phi_zero), both justified by continuity of H and the interval-integral form of the fundamental theorem.
proof idea
Two auxiliary lemmas first show that ∫_0^d H(t+u) du = Φ(t+d) - Φ(t) and ∫_0^d H(t-u) du = Φ(t) - Φ(t-d) by constructing the obvious difference functions F, verifying that each F has derivative zero via phi_hasDerivAt composed with the linear shift, and concluding constancy from is_const_of_deriv_eq_zero with the value at zero fixed by phi_zero. Adding the two integrals over [0,δ], substituting the d'Alembert relation inside the integrand, and evaluating the resulting constant multiple of Φ(δ) yields the linear equation solved for H(t).
why it matters in Recognition Science
The lemma supplies the explicit pointwise representation that powers the induction in dAlembert_contDiff_nat, proving H is C^n for every n and thereby discharging the former H_AczelClassification hypothesis. It therefore confirms that the only continuous solutions arising from J-automorphisms are the smooth hyperbolic and trigonometric functions, consistent with the eight-tick octave structure and the derivation of three spatial dimensions. The result closes the regularity gap between the algebraic cost axioms and the smooth physics that follows from them.
scope and limits
- Does not prove existence of a δ with Φ(δ) ≠ 0; that step is supplied by a separate lemma.
- Does not assume differentiability of H; only continuity is used.
- Does not derive the second-order ODE or classify solutions by the sign of the second derivative.
- Applies exclusively to solutions of this d'Alembert equation, not to arbitrary functional equations.
Lean usage
have h_rep := representation_formula H h_cont h_dAl hδ_neformal statement (Lean)
130private lemma representation_formula (H : ℝ → ℝ) (h_cont : Continuous H)
131 (h_dAl : ∀ t u, H (t + u) + H (t - u) = 2 * H t * H u)
132 {δ : ℝ} (hδ_ne : Phi H δ ≠ 0) (t : ℝ) :
133 H t = (Phi H (t + δ) - Phi H (t - δ)) / (2 * Phi H δ) := by
proof body
Tactic-mode proof.
134 have h_cont_add : Continuous (fun u => H (t + u)) :=
135 h_cont.comp (continuous_const.add continuous_id)
136 have h_cont_sub : Continuous (fun u => H (t - u)) :=
137 h_cont.comp (continuous_const.sub continuous_id)
138 have h_shift : ∀ d, ∫ u in (0:ℝ)..d, H (t + u) = Phi H (t + d) - Phi H t := by
139 intro d
140 let F : ℝ → ℝ := fun d => (∫ u in (0:ℝ)..d, H (t + u)) - (Phi H (t + d) - Phi H t)
141 suffices hF : F d = 0 by simp only [F] at hF; linarith
142 have hF_hasDerivAt : ∀ d, HasDerivAt F 0 d := by
143 intro d
144 have h1 := intervalIntegral.integral_hasDerivAt_right
145 (h_cont_add.intervalIntegrable 0 d)
146 h_cont_add.aestronglyMeasurable.stronglyMeasurableAtFilter
147 h_cont_add.continuousAt
148 have h2_raw := (phi_hasDerivAt H h_cont (t + d)).comp d ((hasDerivAt_id d).const_add t)
149 have h2 : HasDerivAt (fun d => Phi H (t + d)) (H (t + d)) d := by
150 simpa only [mul_one, Function.comp_def] using h2_raw
151 show HasDerivAt F 0 d
152 have h3 : HasDerivAt F (H (t + d) - H (t + d)) d := h1.sub (h2.sub_const _)
153 simpa using h3
154 have hF0 : F 0 = 0 := by simp [F, intervalIntegral.integral_same, phi_zero]
155 have hF_diff : Differentiable ℝ F := fun d => (hF_hasDerivAt d).differentiableAt
156 have hF_const := is_const_of_deriv_eq_zero hF_diff (fun d => (hF_hasDerivAt d).deriv)
157 linarith [hF_const d 0]
158 have h_refl : ∀ d, ∫ u in (0:ℝ)..d, H (t - u) = Phi H t - Phi H (t - d) := by
159 intro d
160 let F : ℝ → ℝ := fun d => (∫ u in (0:ℝ)..d, H (t - u)) - (Phi H t - Phi H (t - d))
161 suffices hF : F d = 0 by simp only [F] at hF; linarith
162 have hF_hasDerivAt : ∀ d, HasDerivAt F 0 d := by
163 intro d
164 have h1 := intervalIntegral.integral_hasDerivAt_right
165 (h_cont_sub.intervalIntegrable 0 d)
166 h_cont_sub.aestronglyMeasurable.stronglyMeasurableAtFilter
167 h_cont_sub.continuousAt
168 have h_neg_raw := (hasDerivAt_id d).const_sub t
169 have h_neg : HasDerivAt (fun d => t - d) (-1) d := by simpa using h_neg_raw
170 have h_comp := (phi_hasDerivAt H h_cont (t - d)).comp d h_neg
171 have h2 : HasDerivAt (fun d => Phi H t - Phi H (t - d)) (H (t - d)) d := by
172 have h_phi_td : HasDerivAt (fun d => Phi H (t - d)) (H (t - d) * (-1)) d := by
173 simpa only [Function.comp_def] using h_comp
174 convert (hasDerivAt_const d (Phi H t)).sub h_phi_td using 1; ring
175 show HasDerivAt F 0 d
176 have h3 : HasDerivAt F (H (t - d) - H (t - d)) d := h1.sub h2
177 simpa using h3
178 have hF0 : F 0 = 0 := by simp [F, intervalIntegral.integral_same, phi_zero, sub_zero]
179 have hF_diff : Differentiable ℝ F := fun d => (hF_hasDerivAt d).differentiableAt
180 have hF_const := is_const_of_deriv_eq_zero hF_diff (fun d => (hF_hasDerivAt d).deriv)
181 linarith [hF_const d 0]
182 have h_add_int : IntervalIntegrable (fun u => H (t + u)) volume 0 δ :=
183 h_cont_add.intervalIntegrable 0 δ
184 have h_sub_int : IntervalIntegrable (fun u => H (t - u)) volume 0 δ :=
185 h_cont_sub.intervalIntegrable 0 δ
186 have h_integral : Phi H (t + δ) - Phi H (t - δ) = 2 * H t * Phi H δ := by
187 have h1 := h_shift δ
188 have h2 := h_refl δ
189 have h3 : (∫ u in (0:ℝ)..δ, H (t + u)) + (∫ u in (0:ℝ)..δ, H (t - u)) =
190 2 * H t * Phi H δ := by
191 rw [← intervalIntegral.integral_add h_add_int h_sub_int]
192 simp_rw [show ∀ u, H (t + u) + H (t - u) = 2 * H t * H u from h_dAl t]
193 exact intervalIntegral.integral_const_mul (2 * H t) H
194 linarith
195 field_simp at h_integral ⊢; linarith
196