Batch 224-A ACCEPTED -- residual #1 SHARPENED: the (8.5.13) window synchronization IS the grounded one-mode step, and the (8.5.4) lattice corner is a THEOREM

Definitions/MMFLM86WindowSync.lean (348) + Definitions/MMFLM86WindowSyncDelivery.lean (159), both added to
FinalCheck.lean (acceptance green).

* GroundedPairWindow (a window at which C u v K holds AND the (8.5.24) iterate family already vanishes above
  it --- FLM (8.10.5) at that pair), GroundedLatticeCorner, and the sharpened residual
  GroundedModeStepAtStates: groundedness at a (8.5.4) pair is inherited by each of the pair's two
  one-creation-mode descendants, the step CONSUMING its own grounded input.
* groundedLatticeCorner_evenCocycle: the (8.5.4) lattice corner is a THEOREM at the even cocycle.  The
  (8.5.13) half is the landed corollary851_lattice_of_canonical_le with the PROVED
  MM.FLM86NTP.residueNegativeAligned_evenCocycle as its negative-pairing input; the vanishing half is
  (8.5.11) at the honest field (stateVanishesBelow_ZAligned) read through the (8.5.24) iterate.  So no
  negative-pairing hypothesis survives in the corner.
* HEADLINE (BOTH WAYS, UNCONDITIONAL): spanningEventual_zAligned_iff_groundedStep :
  Corollary851SpanningEventualWindows (ZAligned E) <-> GroundedModeStepAtStates (ZAligned E).  Forward: the
  one-mode successor of a (8.5.4) pair is again a (8.5.4) pair (stateOfVL_cons is rfl), so the residual
  applies directly.  Backward: the (8.5.4) list induction of the landed twin
  corollary851_spanningStates_exists_of_lattice_and_step, re-run in the grounded currency, each step
  consuming the grounded window its own induction hypothesis produced.  The cornered form
  spanningEventual_iff_groundedStep_of_corner is kept as the general statement.
* groundedStep_imp_windowFree: the honest one-way comparison with the window-free currency (the converse is
  the batch-223-A gap: a window below the (8.10.5) threshold cannot be raised, the machine-checked
  MM.FLM86SL.not_corollary851_succ_of_first_ne_zero).  groundedPairWindow_lattice_nonempty: the step's
  hypothesis is satisfiable (the corner), so the step is not about an empty hypothesis.
* the delivery is RE-HUNG on the sharpened spelling (composition of landed theorems only):
  groundedZeroFace_of_groundedStep (the assembly's grounded Res_{z_0} face),
  stepCorrected_of_groundedStep (EvenCocycleJacobiStepCorrected from the grounded step + NegativeResidual),
  allStates_of_matching_and_groundedStep, and theorem8102_of_matching_and_groundedStep (FLM Theorem 8.10.2
  with the window hypothesis replaced by the grounded one-mode step; the Fock matching conjunct
  ResidueMatching8625 and the six boundary inputs pass through unchanged).
* EXACT RESIDUAL after batch 224: residual #1 is exactly the (8.6.23)/(8.6.24) cross contraction at the
  descendant pair --- equivalently, by batch 223-B, the honest commutator half of the (8.6.25)/(8.6.27)
  matching; then NegativeResidual, the Fock named residuals and the six boundary inputs.

Verification: tools/build.ps1 Definitions/MMFLM86WindowSync.lean Definitions/MMFLM86WindowSyncDelivery.lean
OK; python Probe/forbidden_tokens.py on both files reports sorry=0 admit=0 axiom=0 native_decide=0;
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 224
entry and NOTES section 121 appended.
