Batch 228-A ACCEPTED -- the FOCK half of (8.6.25)/(8.6.27) is ONE one-mode step (the mode action on the blocks), and its lattice base is a THEOREM

Definitions/MMFLM86NegPairingFockStep.lean (218), added to FinalCheck.lean (acceptance green).

* FaceAtFamily E a b j m n D: the (8.6.25) face at one finite family of (8.5.4) states, with the support
  common to the family; honestNegPairingCoeffAtStates_iff_familyFaces identifies it with the ledger's
  HonestNegPairingCoeffAtStates definitionally.
* THE ONE-MODE STEP, NAMED: FockStep E -- the face at a family is inherited when a LIST of (8.5.4)
  creation modes is appended to every state of the family (the list form is what the (8.5.4) induction
  consumes, via List.take 1 / List.drop 1); its one-mode instance is fockStep_imp_oneMode.  This is the
  piece recorded as missing ("the mode action, i.e. its Fock second half"): the proof compares the two
  sides' recursions in the TEST vector -- the PROVED (8.6.9)/(8.6.10) mode--field commutator at the
  inserted state on the left (batch 219-B) against the mode action on the normal-ordered blocks
  blockOfShift = normOrdered2 on the right, with the coefficients compared by the landed
  MM.FLM86FB.flatBinomialExpansion (batch 221-A).
* THE BASE IS A THEOREM: faceAtFamily_lattice -- for a family all of whose states are lattice states the
  face holds with the union of the canonical windows canonWindow of the family as the common support
  (the landed generator window honestNegPairingCoeff_at_generators_window + the vanishing of a block
  outside its own canonical window + blockSum_subset).  So appending modes is the ONLY content left.
* HEADLINE (both ways, hs only): honestNegPairingCoeffAtStates_iff_fockStep :
  HonestNegPairingCoeffAtStates E <-> FockStep E.  Forward: a list-extension of (8.5.4) data is again
  (8.5.4) data, so the face supplies the support.  Backward: strong induction on the total number of
  oscillators sum_i #(D i).osc, peeling ONE mode from every state of the family per round; the base is
  faceAtFamily_lattice and each round is FockStep.
* CONSEQUENCE: the Fock half (residual #3) is a single one-mode step, exactly as batch 218 isolated the
  (8.6.9) content as ModeFieldCommAnnStep (proved in batch 219-B).  The lattice factor, the generator
  slice, the windows, the uniform-support bookkeeping and the (8.5.4) induction are out of the residual.

EXACT RESIDUAL after batch 228: (1) residual #1 = the source's (8.6.3) (batches 225--227); (2)
NegativeResidual; (3) FockStep E (the Fock half, = HonestNegPairingCoeffAtStates = HonestNegPairingCoeff);
(4) ResidueMatching8625NegSecondSlot; (5) the six boundary inputs.

Verification: tools/build.ps1 Definitions/MMFLM86NegPairingFockStep.lean OK; python
Probe/forbidden_tokens.py all zeros; python Probe/b222a_audit.py reports 0 refuted names consumed;
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 228
entry and NOTES section 125 appended; HANDOVER.md updated (header, section 0, the Fock row, the next
steps).
