comparison_irrefl
plain-language theorem explainer
The ratio function r in a closed observable framework satisfies irreflexivity of its inequality negation for every state. Researchers building ledger reconstruction from observable ratios cite this to lock in basic consistency before regularity axioms enter. The proof is a one-line simplification that invokes reflexivity of equality on the reals.
Claim. Let $F$ be a closed observable framework with state space $S$ and ratio function $r:S→ℝ$. For every state $s∈S$, it is not the case that $r(s)≠r(s)$.
background
A closed observable framework is a structure with countable state space $S$, transition map $T$, positive ratio function $r$, conserved charge, nontriviality (distinct ratios exist), and the prohibition on continuous moduli embeddings. The module places this inside Gap 1 of the axiom-closure plan, absorbing R1–R6 as definitions and retaining only the Regularity Axiom for phase 6. The declaration depends directly on the ClosedObservableFramework structure definition that encodes C1 non-trivial observability, C2 closure, and C3 finite description.
proof idea
The proof is a one-line wrapper that applies the simp tactic. Simplification reduces the negated inequality directly to a contradiction with reflexivity of equality on the reals.
why it matters
The result confirms that C1 forces a reflexive comparison mechanism inside the closed observable framework. It supplies a consistency check that precedes sibling results on symmetry and normalization in the same module and supports the ledger reconstruction pipeline. No downstream uses are recorded, yet the declaration closes a basic consistency gap before the Regularity Axiom is invoked.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.