Phi
plain-language theorem explainer
Phi constructs the antiderivative of a continuous function H by integrating it from 0 to t. Analysts working on smoothness for d'Alembert equations that arise from shifted cost functions in Recognition Science cite this construction to start the integration bootstrap. The declaration is a direct one-line definition that invokes the interval integral without additional steps.
Claim. $Phi(H)(t) := ∫_{0}^{t} H(s) ds$, where $H : ℝ → ℝ$ satisfies the d'Alembert equation $H(t+u) + H(t-u) = 2 H(t) H(u)$ with $H(0)=1$.
background
The module proves Aczél's smoothness theorem: any continuous solution H to the d'Alembert equation with H(0)=1 is real analytic. The shifted cost is introduced upstream as H(x) = J(x) + 1 = ½(x + x^{-1}), under which the Recognition Composition Law becomes the d'Alembert equation H(xy) + H(x/y) = 2 H(x) H(y). Phi supplies the integral representation that converts continuity into differentiability during the bootstrap phase of the argument.
proof idea
The declaration is a direct definition that sets Phi H t to the interval integral from 0 to t of H s. It is applied in downstream lemmas such as phi_hasDerivAt, which invokes intervalIntegral.integral_hasDerivAt_right together with the continuity assumption to obtain HasDerivAt (Phi H) (H t) t.
why it matters
Phi serves as the entry point for the integration bootstrap inside dAlembert_contDiff_nat, which establishes ContDiff ℝ n H for every n and thereby completes the first step toward analyticity. This step aligns with the J-uniqueness property (T5) in the forcing chain and supports the overall classification of solutions as cosh, cos, or constant, as referenced in the module documentation citing Aczél (1966).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.