IndisputableMonolith.Cost.ContDiffReduction
The ContDiffReduction module supplies lemmas that differentiate the d'Alembert equation once in the second variable under twice continuous differentiability to reach an ODE form. Researchers verifying the T5 J-uniqueness step cite these reductions to connect the Recognition Composition Law to differential equations. The structure consists of direct applications of Mathlib differentiation rules to the functional equation without additional hypotheses.
claimIf a function satisfies the d'Alembert equation $J(xy) + J(x/y) = 2J(x)J(y) + 2J(x) + 2J(y)$ and is twice continuously differentiable, then its first derivative in the second variable at zero obeys the relation obtained by differentiating the equation, and the second derivative yields the ODE $f'' = k f$.
background
The module sits inside the Cost domain and imports the FunctionalEquation module, whose doc-comment states it supplies lemmas for the T5 cost uniqueness proof. It works with the Recognition Composition Law as the d'Alembert equation and introduces contDiffTwo to denote twice continuously differentiable functions. Upstream results supply the base functional equation helpers that allow differentiation to be applied term by term.
proof idea
The module proceeds by a sequence of one-line wrappers and tactic applications. contDiffTwo_differentiable and hasDerivAt_deriv_of_contDiffTwo justify existence of derivatives. dAlembert_first_deriv_of_contDiff and dAlembert_second_deriv_at_zero_of_contDiff differentiate the equation once and twice. dAlembert_to_ODE_of_contDiff and dAlembert_to_ODE_hypothesis_of_contDiff assemble the ODE, while composition_law_forces_reciprocity and dAlembert_cosh_solution_of_contDiff close the reduction to the cosh form.
why it matters in Recognition Science
The module supplies the continuous-differentiability reduction path required by the T5 J-uniqueness theorem. It feeds the washburn_uniqueness_of_contDiff sibling and ultimately the full uniqueness argument that forces J to be the self-similar fixed point. The reduction closes the step from the Recognition Composition Law to the eight-tick octave and D=3 spatial dimensions in the forcing chain.
scope and limits
- Does not prove uniqueness for non-differentiable solutions.
- Does not compute the explicit constant k without the phi-ladder.
- Does not extend the reduction beyond the one-variable functional equation.
- Does not address the Berry creation threshold or Z_cf values.
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