canonicalDistinctionAtomDecidableEq
plain-language theorem explainer
Equality on the type of canonical distinction atoms is decidable. That type is definitionally the Booleans, so any later case split, match, or equality test on absolute-floor atoms can use ordinary decidable equality. The proof is a one-line reduction to Mathlib's DecidableEq instance for Bool.
Claim. The type of canonical distinction atoms carries a decidable equality: for any two atoms $a,b$ one can algorithmically decide whether $a=b$. Definitionally those atoms are the two Boolean values, so the decision procedure is the standard one on $\mathrm{Bool}$.
background
The module UnifiedForcingChain assembles the complete inevitability chain from the cost foundation (Recognition Composition Law plus normalization and calibration) through T-1 and T0–T8. At the absolute floor, the meta-language must already support a primitive distinction: a non-singleton universe of atoms on which recognition can act.
The canonical distinction atom type is the carrier for that floor-level two-valued distinction. In this development it is identified with Bool, matching the Boolean configuration space and Boolean recognition-cost constructions that appear as siblings in the same module (bool config space, bool recognition cost, floor configs from witnesses).
Decidable equality is the minimal computational interface needed to treat those atoms as discrete data: equality tests, case analysis, and finite enumeration all require it before cost, ledger, or logic forcing lemmas can talk about concrete atom configurations.
proof idea
One-line wrapper. The instance goal is DecidableEq on the canonical distinction atom type. A show rewrites that goal along the definitional equality of the atom type with Bool, then inferInstance picks up Mathlib's standard DecidableEq Bool. No custom cases or induction are written.
why it matters
Inside the forcing chain this is pure infrastructure, not a physics step. T-1 (absolute floor) and T0 (logic forced from cost) need a discrete two-point atom type before Boolean floor configs and recognition-cost constraints can be stated. Providing decidable equality makes that type usable in constructive Lean proofs rather than a bare Prop-level distinction.
No downstream declarations currently list this instance as a dependency, so it is a local enabling instance for the atom API next to canonicalDistinctionAtom. It does not itself force φ, the eight-tick octave, or D=3; those sit later in T5–T8. It only closes the decidability obligation so atom-level reasoning can proceed without classical choice.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.