CostFunctional
plain-language theorem explainer
Cost functionals are formalized as structures pairing a map F from reals to reals with the domain condition that nonzero outputs occur only for positive inputs. Researchers deriving the uniqueness of the d'Alembert equation from symmetry and multiplicative consistency cite this definition as the base type. The declaration is a direct structure introduction with no lemmas or computational reduction.
Claim. A cost functional is a function $F : ℝ → ℝ$ such that $F(x) ≠ 0$ implies $x > 0$.
background
The module establishes that any cost functional on positive reals obeying symmetry, normalization at unity, and multiplicative consistency with a symmetric quadratic polynomial must reduce to the d'Alembert form. CostFunctional supplies the minimal carrier type with the function field and the positivity guard that restricts meaningful support to ℝ₊. Upstream aliases supply concrete instances, including the gap map F(Z) = log(1 + Z/φ)/log(φ) and the generating functional F(z) = log(1 + z/φ).
proof idea
The declaration is a structure definition that directly introduces the two fields F and domain_pos with no proof obligations or tactic steps.
why it matters
This definition supplies the carrier for the module's central claim that symmetry plus quadratic multiplicative consistency forces the bilinear family and hence the recognition composition law. It anchors the transcendental argument that closes normalization, RCL, and calibration axioms, feeding the forcing chain T0-T8 and the uniqueness of the phi-ladder. No open scaffolding remains at this level.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.