Batch 237-A ACCEPTED -- correction of record: the batch-229 Theorem 8.8.9 statement was VACUOUS; the hole is restated in the source-faithful form; residual #2 is supplied by it (registered holes 5 -> 4)

Definitions/MMFLM88Theorem889Stated.lean:

* MM.FLM88.JacobiIdentity Y a b N is the plain equality forall l m n, crossBracket Y a b N l m n =
  crossIterate Y a b N l m n (MMFLM88Jacobi.lean:451--452), with NO window conjuncts, and the landed
  MM.FLM810JBAux.jacobiIdentity_zero_window proves it at N = 0 for EVERY field (the campaign recorded
  this degeneracy at MMFLM810JacobiToBridge.lean:329--332).  Hence the batch-229 statement
  `forall u v, exists N, JacobiIdentity ... N` was provable with N := 0: its registered `sorry` was
  SPURIOUS, and the five declarations stated in that uniform currency (theorem889_jacobi,
  theorem889_delta, remark8811_res_z0, remark8811_res_z1, remark8812_res_z2) asserted nothing.
* the SOURCE-FAITHFUL statement is added as the file's ONLY hole: `theorem889_faithful`, i.e. the
  landed MM.FLM810ASM.FacesAtStates at the boundary field (per monomial AND per element windows, both
  sides terminated and equal -- the source's own reading of the (8.10.8) sentence, quoted at
  MMFLM810Axioms.lean:343--349).  Its l = 0 face is Corollary 8.5.1 (8.5.13) and its l < 0 slice is
  residual #2;
* theorem889_jacobi is now PROVED (by N = 0) and its docstring marks the currency as degenerate; the
  other four uniform declarations are PROVED, so their guards now print [propext, Classical.choice,
  Quot.sound] while theorem889_faithful's guard prints sorryAx.  The engine link
  theorem861_of_theorem889 is unaffected (it takes the FACE at a window K with 1 <= K).

Definitions/MMFLM810Theorem8102Stated.lean: no hole of its own for residual #2 any more --
negativeResidual_evenCocycle is the one-line projection
`fun u v l _ _ m n D => MM.FLM88T889S.theorem889_faithful ... u v l m n D` (FacesAtStates |->
NegativeFaces |-> NegativeResidual, both definitional per MMFLM810Assembly.lean:104/150/177); its
footprint still carries sorryAx through the 8.8.9 hole (guard unchanged), and the header/table say so.

Registered holes after this commit: FOUR, not five -- (1) the (8.4.25) cross contraction
(MM.FLM810T861S.crossContraction_evenCocycle); (2) residual #2 = Theorem 8.8.9 in the source-faithful
form (MM.FLM88T889S.theorem889_faithful), registered ONCE (it used to be counted twice and the 8.8.9
copy was the empty uniform form); (3) FockStep (#3); (4) ResidueMatching8625NegSecondSlot (#4); the six
boundary inputs remain parameters.  #3/#4 are NOT fillable from 8.8.9: the book proves 8.8.9 by
repeating Theorem 8.6.1's proof, which computes the iterate side via (8.6.25)/(8.6.27), so they are
UPSTREAM of 8.8.9, and #2 is the item expected to consume #3 (HANDOVER.md section 6 item 3).

Both files build `--- OK ---`; FinalCheck.lean GREEN; Probe/forbidden_tokens.py reads sorry=1 (8.8.9
file, the faithful hole) and sorry=2 (8.10.2 file, #3/#4), all other counts zero.  README.md (the two
map rows), HANDOVER.md (the hole count, the 8.10.2 row, section 1 row 2), ROADMAP.md (#2) and NOTES.md
(section 137) updated.
