aristotelian_decomposition
plain-language theorem explainer
Aristotelian decomposition separates definitional properties of equality-induced costs from substantive ones on the reals. Foundational work in Recognition Science cites this to streamline the rigidity theorem by treating identity, symmetry, and totality as automatic while requiring composition consistency as an independent axiom. The proof proceeds by term-mode refinement applying four sibling lemmas that establish the three definitional facts and exhibit the Hamming cost's failure of composition consistency.
Claim. Let $w$ be a nonzero real weight. For the equality-induced cost $C$ on the reals, $C(x,x)=0$ for every real $x$, $C(x,y)=C(y,x)$ for all real $x,y$, and $C$ is total. The Hamming cost on the positive reals under multiplication fails composition consistency: there is no combiner $P$ such that $C(xy,1)+C(x/y,1)=P(C(x,1),C(y,1))$ for all positive $x,y$.
background
The module PrimitiveDistinction introduces equality-induced costs on a carrier type and isolates the Aristotelian laws of logic as properties of such costs. CompositionConsistency is the abstract form of L4: for a cost function $C$ there exists a combiner $P$ satisfying $C(xy,1)+C(x/y,1)=P(C(x,1),C(y,1))$ whenever $x,y>0$. The sibling definitions equalityCost, identity_from_equality, non_contradiction_from_equality, and totality_from_function_type encode the three definitional properties directly from reflexivity, symmetry, and the function-type signature of the cost. Upstream, LogicAsFunctionalEquation.Identity states that comparing a thing with itself costs zero, while CostAxioms.Composition encodes the Recognition Composition Law as the d'Alembert equation in multiplicative form.
proof idea
The proof is a term-mode refinement of the four-way conjunction. The first three conjuncts are discharged by exact application of the sibling lemmas identity_from_equality, non_contradiction_from_equality, and totality_from_function_type. The final conjunct is discharged by exact application of composition_consistency_not_definitional, which exhibits the concrete failure of the Hamming cost on the multiplicative reals.
why it matters
This theorem reduces the foundational surface of the rigidity theorem from seven independent axioms to four substantive structural conditions plus three definitional facts. It directly supports the bridge to SatisfiesLawsOfLogic by showing that Identity and Non-Contradiction are automatic for equality-induced costs, leaving Composition Consistency, continuity, scale invariance, and non-triviality as the remaining substantive requirements. The result sits inside the chain that derives the functional equation for J from the Recognition Composition Law and feeds downstream work on the phi-ladder and eight-tick octave.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.