Batch 226-A ACCEPTED -- residual #1 in the per-pair DISPLAY currency of (8.6.23)/(8.6.24): the per-pair bridge, and the step IS the residual

Definitions/MMFLM86DisplayPair.lean (336), added to FinalCheck.lean (acceptance green).

* DisplayAtPair / DisplayAllStates: FLM's (8.6.23)/(8.6.24) at ONE pair of states -- for every window K
  above which the (8.5.24) iterate family of the pair vanishes, the commutator family (8.5.15) IS the
  (8.5.13) residue of the iterate at K -- with the inert (8.6.4) labels c, r dropped (at the honest
  insertion they select nothing beyond the pair).  displayAllStates_iff_commutatorInsertion8625 (both
  ways): the label-free display IS the landed CommutatorInsertion8625 E (honestIns8625 E), so batch
  225's reduction is consumable and readable in the label-free currency.
* THE PER-PAIR BRIDGE, BOTH WAYS: displayAtPair_iff_groundedPairWindow_of_threshold -- given any N above
  which the iterate family vanishes, the display at a pair IS the existence of a grounded window at that
  pair (forward: N itself is one; backward: raise by Corollary851.of_cutoff, lower by
  MM.FLM86M8625P.corollary851_of_grounded_of_le).  At the honest field the (8.10.5) threshold exists, so
  displayAtPair_zAligned_iff_groundedPairWindow and displayAllStates_iff_groundedAllStates hold
  unconditionally.  Per pair, the campaign's two currencies coincide: "the window of Corollary 8.5.1 is
  the iterate's threshold", on the nose.
* displayAtPair_lattice_evenCocycle: the display at the LATTICE pairs is a THEOREM at the even cocycle
  (the batch-204-A corner read through the bridge), so the display step's hypothesis is satisfiable and
  the corner is the induction's base case in the display currency.
* THE STEP: DisplayModeStep -- the display at a pair is inherited by each of the pair's two
  one-creation-mode descendants, the step consuming the display at its own input pair (no groundedness
  conjunct, no mode labels, no (8.6.4) data).  With displayModeStep_iff_groundedModeStep_of_evenCocycle
  (the two steps are the same statement: grounded to display runs through residual #1's honest commutator
  half and batch 225's descendant windows at arbitrary pairs; display to grounded through the per-pair
  bridge at the spanning pairs) and the HEADLINE
  honestDisplay_iff_displayModeStep_of_evenCocycle : DisplayAllStates (ZAligned E) <-> DisplayModeStep
  (ZAligned E) -- forward: restriction; backward: the display step at the spanning pairs gives the
  batch-224 grounded step, hence the spanning eventual windows (spanningEventual_of_groundedModeStep with
  the landed corner), hence GroundedZeroFace at ALL states (MM.FLM810ASG.groundedZeroFace_of_spanningEventual),
  hence the display at every pair (the per-pair bridge, with MM.FLM810ASM.corollary851_iff_zeroFace).
  Plus displayAllStates_iff_spanningEventual_of_evenCocycle (the composition with batches 223-B/224/225).
* EXACT RESIDUAL after batch 226 (content unchanged, currency sharpened): (1) DisplayModeStep (ZAligned E)
  <-> DisplayAllStates (ZAligned E) <-> CommutatorInsertion8625 E (honestIns8625 E) -- the (8.6.23)/(8.6.24)
  cross contraction, now with no groundedness conjunct, no mode labels and no inert data; (2)
  NegativeResidual; (3) the Fock named residuals; (4) the six boundary inputs.

Verification: tools/build.ps1 Definitions/MMFLM86DisplayPair.lean OK; python Probe/forbidden_tokens.py
all zeros; tools/build.ps1 FinalCheck.lean --- OK with exit 0; every public declaration carries a
#guard_msgs #print axioms guard with footprint exactly [propext, Classical.choice, Quot.sound].  ROADMAP
batch 226 entry and NOTES section 123 appended; HANDOVER.md updated.
