composition_refines
For nonzero integers, joint indistinguishability under the sign recognizer and magnitude recognizer forces the pair to be equal or negatives. Researchers modeling measurement refinement in recognition geometries cite this to show how separate coarse partitions combine into a finer one. The proof reduces the joint conditions to absolute-value equality via simplification and then applies case analysis on the integer sign possibilities.
claimFor all nonzero integers $n$ and $m$, if $n$ and $m$ lie in the same sign class and the same absolute-value class, then $n = m$ or $n = -m$.
background
The sign recognizer on the integers partitions into three classes (negative, zero, positive). The magnitude recognizer partitions by absolute value, producing one class per nonnegative integer. Indistinguishability under either recognizer means the two integers map to the same class under that partition; the theorem concerns the conjunction of the two relations.
proof idea
The term proof introduces the variables and the two indistinguishability hypotheses, simplifies the recognizer definitions to obtain absolute-value equality, invokes the standard lemma that equal absolute values imply the numbers are equal or negatives, and discharges the disjunction by case split.
why it matters in Recognition Science
The result encodes the Composition Principle for these concrete recognizers and is referenced by the module's status summary. It illustrates how recognizer composition refines equivalence classes, consistent with the Recognition Composition Law that enforces multiplicative consistency across the framework. The example supports the broader claim that observables in the Recognition Science setting act as class maps whose joint action yields higher resolution.
scope and limits
- Does not address the zero integer.
- Does not claim that either recognizer alone distinguishes all nonzero pairs.
- Does not extend the statement to non-integer domains.
- Does not quantify the number of classes produced by the composition.
formal statement (Lean)
150theorem composition_refines :
151 (∀ n m : ℤ, n ≠ 0 → m ≠ 0 →
152 (Indistinguishable signRecognizer n m ∧ Indistinguishable magnitudeRecognizer n m) →
153 n = m ∨ n = -m) := by
proof body
Term-mode proof.
154 intro n m hn hm ⟨hsign, hmag⟩
155 simp only [Indistinguishable, signRecognizer, magnitudeRecognizer] at hsign hmag
156 -- Same sign and same magnitude implies n = m or n = -m
157 have h1 : n.natAbs = m.natAbs := hmag
158 -- If signs match and magnitudes match, must be equal or negatives
159 rcases Int.natAbs_eq_natAbs_iff.mp h1 with h | h
160 · left; exact h
161 · right; exact h
162
163/-! ## Physical Interpretation -/
164
165/-! ### Physical Interpretation
166
167These examples show how recognizers model measurement in physics:
168- **Discrete** = perfect measurement (eigenvalue detection)
169- **Sign/magnitude** = coarse measurements (binary outcomes)
170- **Composition** = combined measurements with finer resolution
171
172In quantum mechanics, observables ARE recognizers mapping states to eigenvalues. -/
173
174/-! ## Module Status -/
175