forces
plain-language theorem explainer
The forces structure encodes the equivalence between single-valued comparison on unordered pairs and symmetry of the operator C(x,y)=C(y,x) for any carrier and cost type. This captures the structural necessity that non-contradiction (L2) must appear as symmetry once predication is required to return one value on {x,y}. Researchers working on foundations of logic or Recognition Science derivations cite it to close interpretive choices in the magnitude-of-mismatch encoding. The definition is a direct structural equivalence with no additional data
Claim. For any carrier set $K$ and cost type, a map $C:K→K→Cost$ is single-valued on the unordered pair if and only if $C(x,y)=C(y,x)$. The two statements are equivalent; the asymmetric reading yields two distinct directional maps rather than one binary operator.
background
The module formalizes the claim that a function $K→K→Cost$ coincides with a function $Sym2 K→Cost$ precisely when it is symmetric. Key sibling definitions are singleValuedOnUnorderedPair (the factoring condition) and the symmetry predicate $C x y = C y x$. The local theoretical setting is the Logic_FE rigidity theorem, which treats (L1), (L2), (L3a) as definitional once PrimitiveDistinction is assumed. Upstream results such as ObserverForcing.cost and MultiplicativeRecognizerL4.cost supply the concrete cost functions to which the symmetry condition is applied.
proof idea
The declaration is a pure structure definition with empty body. It packages the two directions singleValued_implies_symmetric and symmetric_implies_factorsThrough into a single named object that records the equivalence.
why it matters
It supplies the Lean form of Theorem 4 in the companion paper RS_Magnitude_of_Mismatch_Uniqueness.tex and removes any remaining interpretive freedom for the magnitude-of-mismatch encoding. Downstream it is used by symmetryGroupPreferenceCert, eq_self_or_inv, ml_nucleosynthesis_eq_phi, riverNetworkCert and OptimalConfig, thereby propagating the symmetry requirement into aesthetics, cost algebra, nucleosynthesis and observability limits. Within the framework it completes the step that links single-valued predication directly to the eight-tick octave and D=3 geometry via the Recognition Composition Law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.