IndisputableMonolith.Cost.ContDiffReduction
ContDiffReduction supplies lemmas that differentiate the d'Alembert form of the Recognition Composition Law once in the second variable under C^2 assumptions. Researchers proving T5 J-uniqueness cite these reductions to reach ODE form and the cosh solution. The module consists of direct calculus applications imported from FunctionalEquation and executed via Mathlib derivative tactics.
claimUnder the hypothesis of continuous differentiability of order two, the d'Alembert equation $J(xy)+J(x/y)=2J(x)J(y)+2J(x)+2J(y)$ yields a first partial derivative in the second variable that satisfies the corresponding first-order ODE, together with a second derivative at zero that recovers the hyperbolic cosine solution.
background
The module belongs to the Cost domain and imports FunctionalEquation, whose doc-comment states it supplies lemmas for the T5 cost uniqueness proof. It also imports Mathlib to access contDiffTwo and hasDerivAt. Sibling declarations introduce the concrete reductions: contDiffTwo_differentiable, dAlembert_first_deriv_of_contDiff, dAlembert_to_ODE_of_contDiff, and washburn_uniqueness_of_contDiff. The local setting is the passage from the Recognition Composition Law to its differential consequences under regularity.
proof idea
Each declaration applies standard differentiation rules from Mathlib to the imported functional equation. First-derivative lemmas use the chain rule on the two terms involving y; second-derivative lemmas evaluate at y=1; ODE-conversion lemmas rearrange the resulting identity; uniqueness lemmas invoke the known solution of the resulting linear ODE.
why it matters in Recognition Science
The reductions close the regularity step required for the T5 J-uniqueness argument inside the forcing chain T0-T8. They feed the parent lemmas in FunctionalEquation that establish J(x)=cosh(log x)-1. The module therefore supplies the missing differentiability bridge between the algebraic form of the Recognition Composition Law and the explicit hyperbolic solution used downstream in the phi-ladder construction.
scope and limits
- Does not prove the base Recognition Composition Law.
- Does not treat cases lacking C^2 regularity.
- Does not derive numerical values of phi or alpha.
- Does not address non-commutative extensions.
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