composition_refines
plain-language theorem explainer
The theorem shows that sign and magnitude recognizers on nonzero integers, when applied jointly, distinguish elements up to sign. Researchers modeling measurement refinement in recognition geometries cite it to illustrate how separate observables combine into a finer partition. The term proof simplifies the two indistinguishability hypotheses, extracts equality of absolute values, and splits via the natAbs equivalence lemma into the equality or negation cases.
Claim. For all nonzero integers $n, m$, if $n$ and $m$ lie in the same sign class and the same magnitude class, then $n = m$ or $n = -m$.
background
The module develops concrete recognition geometries on finite sets and on ℤ. The sign recognizer partitions ℤ into the three classes negative, zero, and positive. The magnitude recognizer partitions by absolute value, yielding classes indexed by 0, 1, 2, …. Indistinguishable r a b holds precisely when the recognizer r maps a and b to the same class. The Composition Principle in the module doc-comment asserts that the conjunction of the two recognizers separates nonzero integers up to sign. Upstream, the Composition class in CostAxioms encodes the Recognition Composition Law as the d'Alembert equation on positive reals.
proof idea
Term-mode proof. After introducing n, m and the two hypotheses, simp unfolds Indistinguishable together with the two recognizer definitions. The magnitude hypothesis directly supplies natAbs n = natAbs m. The lemma Int.natAbs_eq_natAbs_iff then splits this equality into the two exhaustive cases n = m and n = -m, each discharged by the corresponding constructor.
why it matters
The result is referenced by examples_status, which records the status of all concrete geometries in the module. It supplies the concrete instance of the Composition Principle stated in the module doc-comment and thereby supports the broader claim that recognizers model measurement. The construction aligns with the Recognition Composition Law (RCL) from Foundation.CostAxioms and with the T5–T8 forcing chain that derives J-uniqueness and the eight-tick octave.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.