operative_derived_cost_symmetric
plain-language theorem explainer
Operative positive-ratio comparisons produce derived cost functions invariant under argument inversion. Workers formalizing the Recognition Composition Law cite this result to establish the symmetry property of the cost function from the operative hypotheses alone. The proof reduces immediately to the translation lemma linking non-contradiction and scale invariance to reciprocity.
Claim. If $C$ is a comparison operator satisfying identity, non-contradiction, continuity, scale invariance, and non-triviality on positive reals, then the derived cost $F(r) := C(r,1)$ obeys $F(x) = F(x^{-1})$ for all $x > 0$.
background
A comparison operator takes two positive reals and returns a real cost. The derived cost fixes the second argument at 1, producing a function on positive ratios once scale invariance is assumed. IsSymmetric requires this function to equal its value at the reciprocal argument. OperativePositiveRatioComparison packages identity, non-contradiction (symmetric single-valued comparison), continuity via excluded middle, scale invariance, and non-triviality into a single hypothesis. The module isolates the operative case as a direct route to the Recognition Composition Law, bypassing full route independence.
proof idea
The proof is a one-line wrapper that applies the upstream lemma non_contradiction_and_scale_imply_reciprocal to the non_contradiction and scale_invariant fields extracted from the operative hypothesis.
why it matters
This theorem supplies the reciprocity step required to embed an operative comparison into the SatisfiesLawsOfLogic structure. It supports the direct RCL path in the module by confirming symmetry without invoking finite pairwise polynomial closure. The result aligns with the Recognition framework's translation of Aristotelian constraints into functional equations, a prerequisite for deriving the J-cost and the phi-ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.