Composition
plain-language theorem explainer
The multiplicative consistency axiom encodes Axiom 2 of Recognition Science: the Recognition Composition Law for a cost functional F. Researchers deriving the explicit form of the cost function J or constructing algebraic structures for costs would cite this. It is introduced as a direct class definition packaging the d'Alembert equation without additional proof steps.
Claim. Let $F : ℝ → ℝ$. Then $F$ satisfies the Recognition Composition Law when ∀ $x, y > 0$, $F(xy) + F(x/y) = 2 F(x) F(y) + 2 F(x) + 2 F(y)$. This axiom ensures compatibility with the multiplicative group structure on $ℝ_+$.
background
The CostAxioms module formalizes the three primitive axioms from which Recognition Science derives all physics. Axiom 1 requires normalization with F at unity equal to zero. Axiom 2 is the present law, the Recognition Composition Law in multiplicative form. Axiom 3 is the calibration condition that the second derivative of the log-reparametrized function at zero equals one.
proof idea
The declaration is a class definition that directly states the required identity for all positive x and y. No upstream lemmas are invoked; the axiom is taken as primitive.
why it matters
This axiom sits at the base of the axiomatic hierarchy and is referenced by the CostAlgebraData structure that packages the full algebraic data for costs. It enables the proof that the explicit J satisfies the law and the characterization of defects. Within the framework it is the Recognition Composition Law that, combined with the other two axioms, forces the unique solution J(x) = (x + 1/x)/2 - 1 and leads to the eight-tick octave and three spatial dimensions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.