HasMultiplicativeConsistency
plain-language theorem explainer
Multiplicative consistency for a cost functional F and combiner P means that F(xy) + F(x/y) equals P applied to F(x) and F(y) for all positive real x and y. Analysts of functional equations in the Recognition Science program cite this definition when deriving the forced form of the Recognition Composition Law. The declaration is a direct predicate definition consisting of a universal quantifier over the positive reals.
Claim. Functions $F : ℝ → ℝ$ and $P : ℝ → ℝ → ℝ$ are multiplicatively consistent if $F(xy) + F(x/y) = P(F(x), F(y))$ for every pair of positive real numbers $x, y$.
background
The D'Alembert Inevitability module proves that the d'Alembert equation is the unique form satisfying multiplicative consistency for cost functionals under symmetry and normalization. A cost functional assigns a real value to each positive real, with the canonical J-cost given by J(x) = (x + 1/x)/2 - 1. The definition here supplies the consistency condition that later theorems constrain to the bilinear family P(u, v) = 2u + 2v + 2uv after normalization.
proof idea
This declaration is a definition that directly encodes the multiplicative consistency equation as a Prop. No tactics or lemmas are invoked in its body; it functions as an interface predicate for the surrounding theorems on symmetry and polynomial constraints.
why it matters
This definition underpins the entire inevitability argument by providing the consistency hypothesis used in bilinear_family_forced and axiom_bundle_necessary. The latter shows that the axiom bundle A1-A3 is transcendentally necessary, with A2 being the RCL form. It connects to the Recognition Science framework by enabling the derivation of the phi-ladder and the eight-tick octave from the forcing chain T0-T8.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.