IndisputableMonolith.Cost.ContDiffReduction
ContDiffReduction supplies lemmas that differentiate the d'Alembert equation once in the second variable under C^2 assumptions. Researchers verifying the T5 J-uniqueness step cite it to convert the functional equation into an ODE. The module proceeds by successive applications of standard differentiation from Mathlib to the equation imported from FunctionalEquation.
claimLet $f$ satisfy the d'Alembert equation $f(x+y)+f(x-y)=2f(x)f(y)$. If $f$ is twice continuously differentiable, then the first partial derivative in the second variable vanishes at zero and the second derivative at zero yields the ODE $f''= ext{const} imes f$.
background
The module resides in the Cost domain and imports FunctionalEquation, whose documentation states that it supplies lemmas for the T5 cost uniqueness proof. It works inside the Recognition Science setting where the J-cost satisfies the Recognition Composition Law, from which the d'Alembert equation follows. The local notation includes contDiffTwo for twice continuous differentiability and the associated first- and second-derivative reductions.
proof idea
The module structures its argument as a sequence of differentiation lemmas: contDiffTwo_differentiable, first and second derivatives of the d'Alembert equation, then dAlembert_to_ODE_of_contDiff and the hypothesis interface. Each step applies Mathlib derivative rules to the imported functional equation.
why it matters in Recognition Science
The module supplies the continuous-differentiability reductions required by the T5 J-uniqueness argument in the forcing chain. It directly supports downstream results such as dAlembert_cosh_solution_of_contDiff and washburn_uniqueness_of_contDiff that close the step from the functional equation to the explicit cosh form.
scope and limits
- Does not prove J-uniqueness by itself.
- Does not treat non-differentiable solutions.
- Does not derive numerical constants such as phi or alpha.
- Does not address the full eight-tick octave or spatial dimension D=3.
depends on (1)
declarations in this module (10)
-
lemma
contDiffTwo_differentiable -
lemma
contDiffTwo_differentiable_deriv -
lemma
hasDerivAt_deriv_of_contDiffTwo -
theorem
dAlembert_first_deriv_of_contDiff -
theorem
dAlembert_second_deriv_at_zero_of_contDiff -
theorem
dAlembert_to_ODE_of_contDiff -
theorem
dAlembert_to_ODE_hypothesis_of_contDiff -
theorem
composition_law_forces_reciprocity -
theorem
dAlembert_cosh_solution_of_contDiff -
theorem
washburn_uniqueness_of_contDiff