rcl_from_canonical_mismatch_encoding
plain-language theorem explainer
A comparison operator read as magnitude of mismatch, together with finite pairwise polynomial closure, forces its derived cost to obey multiplicative consistency with the specific bilinear combiner 2u + 2v + c uv. Recognition Science derivations of the composition law cite this step to obtain the RCL family directly from the canonical encoding. The proof is a one-line wrapper that first converts the mismatch structure to the operative positive-ratio comparison and then invokes the polynomial-closure theorem.
Claim. Let $C: (0,∞) × (0,∞) → ℝ$ be a comparison operator. Suppose $C$ satisfies the magnitude-of-mismatch conditions (identity at match, unordered-pair symmetry, continuous determinability, scale invariance, and nontriviality) and obeys finite pairwise polynomial closure. Then there exist a function $P: ℝ → ℝ → ℝ$ and a constant $c ∈ ℝ$ such that the derived cost $F(r) := C(r,1)$ obeys $F(xy) + F(x/y) = P(F(x),F(y))$ for all positive $x,y$, and moreover $P(u,v) = 2u + 2v + c·uv$.
background
ComparisonOperator is the type ℝ → ℝ → ℝ of maps that assign a real cost to any ordered pair of positive reals. derivedCost extracts the unary cost function F(r) = C(r,1) by fixing the second argument at the multiplicative identity; under scale invariance this is well-defined on positive ratios. MagnitudeOfMismatch packages five structural axioms on C: trivial value at match (Identity), pair symmetry (NonContradiction), continuous determinability (ExcludedMiddle), scale-free comparison (ScaleInvariant), and nontriviality (NonTrivial). HasMultiplicativeConsistency (F,P) asserts that F(xy) + F(x/y) equals P(F(x),F(y)) for all positive x,y. The module formalises the canonicality step of the paper: once a comparison operator is interpreted as a magnitude of mismatch, the operator-level conditions become the canonical structural content of that reading.
proof idea
The proof is the one-line term rcl_polynomial_closure_theorem C (mismatch_to_operative C hM) hFinite. mismatch_to_operative converts the MagnitudeOfMismatch structure into an OperativePositiveRatioComparison instance by extracting the identity and non-contradiction fields. rcl_polynomial_closure_theorem then supplies the required P and c directly from the finite pairwise polynomial closure hypothesis.
why it matters
This declaration closes the canonicality step that links the magnitude-of-mismatch reading to the Recognition Composition Law. It shows that the RCL family (J(xy) + J(x/y) = 2J(x)J(y) + 2J(x) + 2J(y)) follows once the comparison operator is read canonically and finite pairwise polynomial closure is assumed. The result sits inside the forcing chain that ultimately forces phi as the self-similar fixed point and D = 3; it supplies the algebraic bridge between the Aristotelian constraints and the functional equation used in the mass formula and alpha-band calculations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.