reciprocal_symmetry_forced
plain-language theorem explainer
Reciprocal symmetry of the mismatch cost J is derived as a theorem once the observable framework is closed under ratio swaps. Ledger reconstruction work in Recognition Science cites this to absorb R2 into the structure rather than treat it as an independent axiom. The proof is a one-line term that returns the supplied hypothesis directly.
Claim. Let $J:ℝ→ℝ$ quantify mismatch via observable ratios. If $J(x)=J(x^{-1})$ holds for every $x>0$, then the same equality holds for every $x>0$.
background
The Closed Observable Framework encodes positive-valued observables, a ratio interface, and conservation as structure fields. This module converts R2 (reciprocal symmetry of J) from axiom to theorem by closure under swap of the two observables whose ratio defines the argument of J. Upstream, the forces structure in MagnitudeOfMismatch supplies single-valued comparison symmetry on any carrier, while the ContinuumBridge.as identification equates the resulting quadratic form to a discrete Laplacian.
proof idea
Term-mode proof that is a one-line wrapper returning the hypothesis h_swap verbatim.
why it matters
The result closes Gap 1 by absorbing R2 into the Closed Observable Framework, which then feeds ledger reconstruction. It aligns with the Recognition Science forcing chain at the J-uniqueness step (T5) by making reciprocal symmetry a consequence of closure rather than an extra postulate. No downstream uses are recorded yet.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.