composition_consistency_not_definitional
plain-language theorem explainer
The equality-induced cost on positive reals with nonzero weight fails to satisfy composition consistency. Foundation researchers cite this to establish that the fourth Aristotelian condition is a substantive structural requirement rather than a definitional consequence of the type signature. The proof assumes a combiner P exists, evaluates the defining equation on the pairs (2,2) and (2,3), and obtains the contradictory relation weight = 2 weight.
Claim. Let $C_w : (0,∞) × (0,∞) → ℝ$ be the equality-induced cost given by $C_w(a,1) = w$ whenever $a ≠ 1$ and $C_w(1,1) = 0$. For any real $w ≠ 0$ there does not exist a function $P : ℝ → ℝ → ℝ$ such that $C_w(xy,1) + C_w(x/y,1) = P(C_w(x,1),C_w(y,1))$ holds for all $x,y > 0$.
background
The module develops the four Aristotelian conditions on costs induced by equality on a multiplicative carrier. CompositionConsistency is the abstract form of condition (L4): there exists a combiner P such that the cost of a composite is recovered from the costs of its factors via the carrier algebra. The concrete cost in view is hammingCostOnReal weight, which specialises equalityCost to the base point 1 and returns weight on any non-identity element. The local setting is the Aristotelian decomposition, which classifies three conditions as definitional and isolates (L4) as the only substantive requirement.
proof idea
The tactic proof assumes CompositionConsistency, obtaining a witness P together with its defining equation hP. It first specialises to x = y = 2, simplifies the left-hand side with norm_num and add_zero, and concludes P(weight,weight) = weight. It then specialises to x = 2, y = 3, obtains P(weight,weight) = 2 weight after unfolding the cost definition and applying ring, and combines the two evaluations to reach weight = 2 weight. The final linarith step contradicts the hypothesis weight ≠ 0.
why it matters
The theorem supplies the negative fact required by the downstream aristotelian_decomposition result, which asserts that identity, non-contradiction and totality are definitional while composition consistency is not. It thereby shows that the Recognition Composition Law J(xy) + J(x/y) = 2J(x)J(y) + 2J(x) + 2J(y) cannot be satisfied by a Hamming-type cost and must be enforced by a non-trivial cost compatible with the multiplicative structure, consistent with the J-uniqueness and phi-ladder steps of the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.