PsiAffineOnImage
plain-language theorem explainer
The affineness predicate states that the combiner map ψ is linear on the image of the log-cost reparametrization G. Analysts deriving the second-derivative identity for continuous d'Alembert solutions in the Recognition framework cite this predicate to relax the polynomial-degree hypothesis. The definition is introduced as a direct existential claim over a single real coefficient c.
Claim. The predicate that there exists $c ∈ ℝ$ such that ψ(G(t)) = 2 + c · G(t) for all t ∈ ℝ, where G is the log-coordinate reparametrization of the cost function and ψ is the combiner map arising in the analysis of the d'Alembert equation.
background
The module develops the third move toward discharging the polynomial regularity requirement on the route-independence combiner by substituting continuity. It invokes the Aczél–Kannappan classification: a continuous H : ℝ → ℝ with H(0) = 1 obeying H(x+y) + H(x-y) = 2 H(x) H(y) must be constant, hyperbolic cosine, or trigonometric cosine. This classification is obtained from the existing d'Alembert-to-ODE pipeline and ODE uniqueness on each branch of H''(0).
proof idea
The declaration is a definition, not a theorem. It is introduced directly by the existential statement over the affine coefficient c that enforces the linear relation on the image of G. No upstream lemmas are invoked; the predicate simply names an analysis input required for the subsequent derivative-identity step.
why it matters
The predicate supplies the precise affineness condition needed to extract the second-derivative identity 2 G''(t) = ψ(G(t)) G''(0) under continuity. It supports the continuous-combiner version of SatisfiesLawsOfLogic, which drops the total-degree-≤2 restriction on the combiner. The module records that the quartic log-cost supplies a counterexample showing continuity alone does not guarantee the identity, so finite pairwise polynomial closure remains the sharp hypothesis for the Law-of-Logic paper.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.