instDecidableBalanced
plain-language theorem explainer
Decidability of balance for signed-orbit pairs is automatic once balance is written as equality of distinction lengths. Anyone building integer or rational arithmetic inside the primitive recognition calculus needs this instance so `decide` and related tactics can discharge balance goals. The proof unfolds the predicate to a Nat equality and reuses the ambient Decidable instance.
Claim. For any two signed orbits $a$ and $b$ (pairs of distinction-natural lengths read as $a=a_+-a_-$ and $b=b_+-b_-$), the balance relation $a_++b_-=b_++a_-$ is a decidable proposition.
background
In the primitive recognition calculus, a signed orbit is a pair of distinction-natural lengths (pos, neg), intended as the formal difference pos - neg. Two such pairs are balanced when their cross-sums of lengths agree: a.pos + b.neg = b.pos + a.neg. That equality is the internal integer relation of the calculus, stated entirely on δ-orbit positions rather than on external ℤ.
The surrounding module develops truncated subtraction, absolute difference, and the map from signed orbits to integers, so that later steps can treat balance as the kernel of the integer interpretation. Upstream, the same word “balanced” appears for ledgers (an event list whose credits and debits cancel); here it is specialized to the orbit-length form used by K4.9.
Because the underlying length type carries decidable equality, balance is a decidable Prop once unfolded. This instance records that fact for automation.
proof idea
One-line wrapper. Unfold the local balance definition to the equality a.pos + b.neg = b.pos + a.neg, then infer_instance picks up Mathlib’s decidable equality on the resulting Nat (or DistinctionNat) equation. No custom case analysis is required.
why it matters
K4.9 characterizes balanced length by Nat-level addition; this instance makes that characterization executable inside Lean. Without decidability, later constructions that quotient signed orbits by balance, or that compare integer images via toInt, cannot use decide, if, or proof-by-reflection on balance goals.
In the Recognition forcing chain the integer/rational layer sits under the ledger and cost calculus that eventually force φ, the eight-tick octave, and D = 3. The declaration itself is infrastructure rather than a physical claim: it closes the automation gap for the PRC integer relation so those later steps can treat balance as a concrete, checkable predicate. No downstream theorems currently cite it in the graph, so its value is local enablement of the IntegerRational development.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.