Batch 362-A (THE WINDOW REPAIR IS LANDED, WITH A COMPILED WITNESS: the windows of the prescription are genuine TRUNCATION POINTS -- the batch-361-A suspicion is discharged at the definitional level).

THE REPAIR (a definitional repair of the 344-A/345-A family, NOT a weakening).  Definitions/FLM861BookDefs.lean:
* IsNormalOrder X Y Z now asks, beside the cut sum at the window N, for the TWO TAILS at N to vanish: (forall i >= N, splitMinus X (-i-1) (Y (m+i) w) = 0) and (forall k >= N, Y (m-1-k) (splitPlus X k w) = 0);
* IsBaseField's rectangle now asks for the p-tail (forall p >= N, forall q, Em p (azPowD a q (Ep (p+m+q) w)) = 0) and the q-tail (forall q not in Icc (-N) N, forall p < N, the same = 0).
That is exactly the book's "the sums are finite on every vector": with the tails at N vanishing every larger window gives the same value, the LIMIT, which is what the (8.5.1) determinism needs.  In the honest case both IsBaseField conjuncts are provable with landed material (annihFam_killsAbove for the p-tail on the finite lattice-support set of q, the azPowD confinement for the rest), so the producer zAligned_isVertexOperator merely owes that tail bookkeeping -- which its header already named.  The three book-facing statements' TEXT is unchanged (byte-identical measure below); what changes is that their hypothesis IsVertexOperator is now the book's relation instead of a strictly weaker one.

THE COMPILED WITNESS (new Probe/B362-A_window.lean, EXIT=0, no sorry, namespace MM.B362A).  The pre-repair spelling is copied verbatim as MM.B362A.Old.IsNormalOrder; with the test families Xtest (the single mode -1, the identity) and Ytest (the single mode 0): old_holds shows the PRE-repair relation admits the ZERO family as :Xtest Ytest: (the witness window 0 cuts both sums to 0 and the old spelling asks nothing else), not_isNormalOrder_zero shows the REPAIRED relation admits NO window for it (for every NONZERO w: at N = 0 the first tail is already w != 0, and at every N >= 1 the cut sum is w while the claimed value is 0), and window_repair_is_strict combines them.  This is NOT a refutation of isVertexOperator_unique (no second solution of the whole prescription is exhibited): it is the compiled evidence that the pre-repair relation was strictly weaker than the book's, which upgrades the batch-361-A record from "reasoning only" to "compiled witness of the gap".

DOCS: the WINDOW DEFECT OF RECORD notes on the two definitions are replaced by WINDOW REPAIR notes; the SUSPECT mark on MM.FLM861Book.isVertexOperator_unique is replaced by its post-repair STATUS note (route unblocked; what is still owed is steps (i)--(iv) plus the producer); NOTES.md section 279 and HANDOVER.md sections 3 and 6 carry the record.

EVIDENCE: lake build FinalCheck EXIT=0 (9175 jobs) with the same NINE 'declaration uses sorry' warnings -- the repaired definitions broke NO consumer (the frozen statements, the bridge, the producer and the two refutation files all elaborate unchanged); lake env lean Probe/B362-A_window.lean EXIT=0; the three book-facing statements byte-identical (3 blocks, 0 mismatches); lake env lean Refuted/MMFLM861BookBridgeRefute.lean EXIT=0 and Refuted/MMFLM861BookFieldRefute.lean EXIT=0, both silent; forbidden_tokens on the touched files: admit=0 axiom=0 native_decide=0, sorry only where registered (this module's two pieces).
