comparison_symm
plain-language theorem explainer
Inequality of observable ratios in a closed framework is symmetric under exchange of states. Researchers reconstructing ledgers from closure axioms cite it to confirm mismatch measures are invariant under reciprocity. The proof is a one-line term application of negation symmetry.
Claim. Let $F$ be a closed observable framework with state space $S$ and positive ratio function $r: S → ℝ$. For states $s_1, s_2 ∈ S$, if $r(s_1) ≠ r(s_2)$ then $r(s_2) ≠ r(s_1)$.
background
The ClosedObservableFramework structure equips a countable state space $S$ with a positive real ratio function $r$, a transition map $T$, and a conserved charge, satisfying nontrivial observability and absence of continuous moduli. The module treats this as Phase 2 of the axiom-closure plan, absorbing R2 (reciprocal symmetry) as a derived property rather than an independent axiom. Upstream results supply the reciprocal automorphism from CostAlgebra and the reciprocal event map from LedgerForcing that invert ratios while preserving positivity.
proof idea
The proof is a one-line term that applies the standard negation symmetry lemma Ne.symm directly to the inequality hypothesis.
why it matters
This realizes R2 as a theorem inside ClosedObservableFramework, demonstrating that closure alone forces symmetry of ratio mismatches quantified via $J(r(s_1)/r(s_2)) = J(r(s_2)/r(s_1))$. It advances the ledger reconstruction pipeline by removing R2 from the axiom list, leaving only the Regularity Axiom. The result sits upstream of any ledger reconstruction steps that rely on consistent mismatch measures under state swaps.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.