PsiAffineOnImage
plain-language theorem explainer
PsiAffineOnImage encodes the property that ψ is affine on the range of the log-cost map G, taking the concrete form ψ(G(t)) = 2 + c G(t) for some fixed real c. Analysts of continuous solutions to the d'Alembert equation in the Recognition Science pipeline cite this predicate when checking the second-derivative identity that follows from smoothness. The declaration is a direct existential definition with no lemmas or proof steps.
Claim. The predicate holds when there exists a constant $c ∈ ℝ$ such that ψ(G(t)) = 2 + c ⋅ G(t) for every real t, where G is the log-coordinate reparametrization of the combiner.
background
The GeneralizedDAlembert module relaxes the polynomial-degree ≤ 2 restriction on the route-independence combiner by invoking the Aczél–Kannappan classification of continuous d'Alembert solutions. The log-cost reparametrization G, introduced in Cost.FunctionalEquation as G_F(t) = F(exp t), converts the original combiner into additive coordinates. PsiAffineOnImage captures the required affine behavior of the auxiliary function ψ on the image of this G, which is listed in the module as named analysis input 2a for the Stetkær/Aczél differentiation step.
proof idea
The declaration is a direct definition whose body is the existential statement ∃ c : ℝ, ∀ t : ℝ, ψ (G t) = 2 + c * G t. No upstream lemmas are invoked; the content is the mathematical predicate itself.
why it matters
This predicate supplies one of the two named analysis inputs needed to assemble the continuous-combiner version of SatisfiesLawsOfLogic. It supports the module's goal of replacing the polynomial restriction with continuity alone via the Aczél–Kannappan trichotomy (constant 1, cosh(αx), or cos(αx)). The definition connects to the Recognition Science move that weakens finite pairwise polynomial closure while preserving the Law-of-Logic pipeline, though the quartic-log obstruction still blocks automatic derivation of the second-derivative identity.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.