HasMultiplicativeConsistency
plain-language theorem explainer
Multiplicative consistency for a cost function F is defined by the existence of a combiner P such that F(xy) + F(x/y) equals P applied to F(x) and F(y) for positive x and y. Researchers deriving the Recognition Composition Law from minimal comparison axioms cite this when proving that J is the unique cost satisfying the primitives. The declaration is a direct definitional statement with no additional proof steps required.
Claim. A function $F : (0,∞) → ℝ$ satisfies multiplicative consistency if there exists a combiner $P : ℝ → ℝ → ℝ$ such that $F(xy) + F(x/y) = P(F(x), F(y))$ for all $x, y > 0$.
background
In the Recognition Science framework, cost functions measure deviation from unity and arise as J-cost on positive ratios, with J(x) = (x + x^{-1})/2 - 1. The Ultimate module reduces the foundation to three primitives: symmetry (F(x) = F(1/x)), normalization (F(1) = 0), and this multiplicative consistency requirement, plus regularity conditions. Upstream results include the cost definition in ObserverForcing as J-cost of a recognition event state and the ledger factorization structure that calibrates J.
proof idea
As a definition this declaration directly encodes the existence of a combiner P satisfying the functional equation F(xy) + F(x/y) = P(F(x), F(y)) for positive arguments. No lemmas are applied and no tactics are used.
why it matters
This definition is invoked in bilinear_family_forced and axiom_bundle_necessary within the Inevitability module to establish that consistency forces the unique bilinear form of the RCL. It realizes the consistency primitive in the Ultimate Theorem, showing the Recognition Composition Law is definitional for compositional cost rather than an extra assumption. The result supports the forcing chain from T5 J-uniqueness through the eight-tick octave to D = 3.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.