CompositionConsistency
plain-language theorem explainer
CompositionConsistency defines the L4 Aristotelian condition for a cost function C on positive reals: there exists a combiner P such that the summed costs of a product and quotient equal P applied to the separate costs. Recognition Science researchers cite it when separating definitional equality properties from structural requirements on multiplicative carriers. The definition is a direct existential statement over P that encodes compatibility with the algebra of positive reals.
Claim. A cost function $C : (0,∞) × (0,∞) → ℝ$ satisfies composition consistency when there exists a binary operation $P : ℝ × ℝ → ℝ$ such that $C(xy,1) + C(x/y,1) = P(C(x,1),C(y,1))$ for all $x,y > 0$.
background
In PrimitiveDistinction the equality-induced cost is built from the J-cost of recognition events, with the identity event fixed at state 1 having zero cost. The multiplicative recognizer supplies a derived cost on positive ratios, and the CostAlgebra multiplicative theorem guarantees that J-automorphisms preserve the product operation on PosReal. The local setting specializes the abstract L4 condition to the carrier (ℝ>0, ·) so that composite costs are determined by component costs via some combiner P.
proof idea
This is a definition, not a derived theorem. It directly encodes the required existential quantifier over the combiner P together with the functional equation that must hold for all positive x and y.
why it matters
The definition supplies the precise statement of L4 used in aristotelian_decomposition to isolate the definitional properties L1-L3a from the substantive content of L4. It is invoked in composition_consistency_not_definitional to prove that the equality-induced cost (hammingCostOnReal) fails the condition, showing L4 is not automatic. Within the framework it corresponds to the Composition Consistency step that must hold before the forcing chain reaches J-uniqueness, the phi fixed point, and the derivation of D=3.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.