Phi
plain-language theorem explainer
Phi defines the antiderivative of a function H from 0 to t via the Riemann integral. Researchers classifying continuous solutions of d'Alembert's equation cite this operator to initiate the regularity bootstrap from C^0 to C^∞. The definition is a direct integral expression requiring no auxiliary lemmas or reductions.
Claim. Let $H : ℝ → ℝ$. Define the antiderivative $Φ(H, t) := ∫_0^t H(s) ds$.
background
In the Recognition Science setting the shifted cost is H(x) = J(x) + 1, where J satisfies the Recognition Composition Law and the reparametrized d'Alembert equation H(t+u) + H(t-u) = 2 H(t) H(u) with H(0) = 1. The module proves every continuous solution is C^∞ by an integration bootstrap that repeatedly differentiates the representation formula. The antiderivative Phi supplies the integral appearing in that formula: H(t) = (Φ(t+δ) − Φ(t−δ)) / (2 Φ(δ)) for a suitable δ with Φ(δ) ≠ 0.
proof idea
This is a direct definition of the integral operator. It is invoked by downstream lemmas such as phi_hasDerivAt (which recovers H as the derivative of Phi H) and exists_integral_ne_zero (which locates a δ where the integral is nonzero).
why it matters
Phi supplies the integral tool that closes the former H_AczelClassification hypothesis in the AczelProof module. It feeds the induction step of dAlembert_contDiff_nat and the ODE derivation H'' = c H that yields the cosh, cos, and constant solutions. The construction aligns with T5 J-uniqueness by converting the functional equation into the second-order linear ODE whose solutions are the hyperbolic and trigonometric forms tied to the phi fixed point.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.