hammingCostOnReal
plain-language theorem explainer
Defines the equality-induced cost function on the reals for a given weight, using the multiplicative identity as base point. Researchers working on the separation of definitional logical laws from the Recognition Composition Law cite this construction. It is realized as a direct delegation to the general equalityCost on the carrier ℝ.
Claim. For a real weight $w$, the function $C_w : ℝ → ℝ → ℝ$ is the equality-induced cost on the reals, $C_w(x,y)$ measuring the weighted distinction between $x$ and $y$ with base point the multiplicative identity.
background
In the PrimitiveDistinction module the equalityDistinction supplies the base relation on any carrier, from which equalityCost derives a weighted real-valued cost. The module tests this cost on ℝ to isolate which laws of logic follow from the equality construction alone. The Composition class from CostAxioms encodes the Recognition Composition Law: for positive $x,y$, $F(xy) + F(x/y) = 2F(x)F(y) + 2F(x) + 2F(y)$. Upstream results on multiplicative recognizers and observer forcing supply the J-cost interpretation used to calibrate the weight.
proof idea
The definition is a one-line wrapper that applies equalityCost to the real numbers with the supplied weight.
why it matters
This supplies the concrete cost function invoked by the Aristotelian decomposition theorem, which separates the definitional parts (identity, non-contradiction, totality) from the substantive L4 condition. It is also used in the proof that equality cost fails CompositionConsistency, confirming that the Recognition Composition Law imposes a non-trivial constraint. The construction sits at the primitive-distinction level before the forcing chain reaches J-uniqueness, the phi fixed point, and the eight-tick octave.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.