Batch 227-A ACCEPTED -- residual #1 IS the source's Theorem 8.6.1 display (8.6.3), in the source's own carrier

Definitions/MMFLM86SourceBridge.lean (226), added to FinalCheck.lean (acceptance green).

* corollary851_iff_sourceUnshifted / corollary851_iff_sourceStatement: at ONE pair and window, the
  factor-free source carrier MM.FLM86SG.sourceResidue861Unshifted IS the landed (8.5.13) (the landed
  sourceResidue861Unshifted_eq_corollary851Residue is rfl), and the carrier WITH the source's
  operator-valued grading factor (z_1/z_2)^a of (7.1.34)--(7.1.35) is the same statement because the
  factor's finite-support sector sum is the identity (sourceResidue861_eq_unshifted).  The spine's
  carriers introduce nothing.
* corollary851_iff_theorem861SourceStatement: at a labelled (8.6.2) pair (u' (x) iota(a), v' (x) iota(b))
  and under the source's hypothesis (8.6.1), MM.FLM86SG.Theorem861SourceStatement at window K IS the
  landed Corollary851 at that window (the Prop is the (m,n)-pointwise reshaping of the same operator
  identity).
* displayAtPair_iff_forall_theorem861SourceStatement: residual #1 at a labelled pair (batch 226's
  per-pair display) IS the source's (8.6.3) at EVERY window above which the (8.5.24) iterate family
  vanishes -- the honest reading of the source's window K (its "finite sum" for the states of (8.6.2)).
* HEADLINE (BOTH WAYS, even cocycle, the (8.6.1) hypothesis discharged by
  MM.FLM86.hypothesis861_of_evenCocycle): displayAllStates_iff_sourceStatements_of_evenCocycle :
  DisplayAllStates (ZAligned E) <-> the source's (8.6.3) at every labelled (8.6.2) state pair and every
  window above the vanishing bound.  Forward: the per-pair bridge of batch 226 with the (8.10.5)
  threshold.  Backward: the labelled pairs include the (8.5.4) states (MM.FLM85Un.stateOfVL_eq_tmul with
  u' = MM.FLM85Un.fockWord), the display there gives the spanning grounded windows, hence the spanning
  eventual windows (MM.FLM86SL.spanningGrounded_iff_eventual), hence the grounded Res_{z_0} face at ALL
  states (MM.FLM810ASG.groundedZeroFace_of_spanningEventual), hence the display at every pair (the
  per-pair bridge, MM.FLM810ASM.corollary851_iff_zeroFace).
* CONSEQUENCE: the campaign's residual #1 and the spine's "single named next step" (8.6.3) are ONE
  statement, machine-checked both ways; the source's route (8.6.4)--(8.6.27), with the mode--field
  commutator (8.6.9)/(8.6.10) PROVED in batch 219-B and the per-step status table in
  MMFLM86SpineGap.lean, is available as a map.

EXACT RESIDUAL after batch 227 (content unchanged, now identified with the source): (1) the source's
(8.6.3) = DisplayAllStates (ZAligned E) = DisplayModeStep = CommutatorInsertion8625 E (honestIns8625 E);
(2) NegativeResidual; (3) the Fock named residuals; (4) the six boundary inputs.

Verification: tools/build.ps1 Definitions/MMFLM86SourceBridge.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 227 entry and NOTES section 124 appended; HANDOVER.md updated.
