Batch 360-A (FLM (8.5.1) SPLIT BY CLAUSE (b'): the battlefield's rigidity_of_hY is PROVED from UNIQUENESS + the PRODUCER, and the exponential-determinism core is landed).

Target: the battlefield's ONE registered piece MM.FLM861Book.rigidity_of_hY.  MEASUREMENT: it is the conjunction of two INDEPENDENT statements --- UNIQUENESS (the prescription determines the field, no honest field needed) and EXISTENCE (the honest field satisfies it = the producer, items 1+2 of FLM861BookProducer.lean's header) --- so the batch is the clause-(b') split with a COMPILED reassembly.

NEW MODULE Definitions/MMFLM861BookUniqueness.lean (namespace MM.FLM861Book), placed BETWEEN Definitions/FLM861BookDefs.lean and Definitions/FLM861BookTransport.lean: the import direction is load-bearing (the battlefield must consume it, so it cannot import the producer, which is downstream of the statement file).

MOVED there verbatim from Definitions/FLM861BookProducer.lean (proofs unchanged, namespace now MM.FLM861Book, which the producer opens so its remaining proofs and the two refutation files are untouched): modeVL_ofL_eq, creationVL_ofL_eq, rat_smul_eq, isEminus_creationExpVL, isEplus_annihFam (the producer's guards for them are deleted).

PROVED there (guarded, [propext, Classical.choice, Quot.sound]): isEminus_unique / isEplus_unique (the two (8.4.17) recurrences are triangular; m+1 != 0 and j+1 != 0 in characteristic zero, so each has at most one solution); isEminus_eq_creationExpVL / isEplus_eq_annihFam (hence the exponentials of ANY solution ARE the honest creationExpVL / annihFam, which is what lets the (8.4.17) triple product be read with the honest operators); annihFam_killsAbove (E^+ kills every fixed vector from a bound on, from the landed MM.FLM84CM.locallyFiniteCoef_annihFam via locallyFiniteCoef_iff_finiteSupport and Set.Finite.bddAbove --- the window stability of the triple product).

REGISTERED there (the split pieces): isVertexOperator_unique (UNIQUENESS) and zAligned_isVertexOperator (EXISTENCE = the producer).  Definitions/FLM861BookTransport.lean's rigidity_of_hY is now the compiled two-liner isVertexOperator_unique ... (zAligned_isVertexOperator ...) and the battlefield carries NO sorry; its header and TODO are rewritten accordingly.

Four-question test: (1) the entry MM.FLM861Book.rigidity_of_hY is PROVED and its two halves are registered in the new module (clause (b'): one hole becomes two strictly smaller, genuinely different ones --- determinism vs existence --- and the battlefield's own ledger goes to ZERO); (2) the old statement is PROVED in Lean from the new declarations (compiled one-liner; its footprint is unchanged, [propext, sorryAx, Classical.choice, Quot.sound], inherited); (3) no new declaration is deletable (the two uniqueness lemmas are what the ..._eq_... corollaries cite, those are the route into the uniqueness, annihFam_killsAbove is the window stability it consumes, and the moved instances are what the corollaries compare against); (4) the new module is reached from FinalCheck.lean through MMFLM861BookUniqueness -> FLM861BookTransport -> FLM861Book (EXIT=0), and its two pieces are guarded locally and in the gate.

Evidence: lake build Definitions.FLM861Book EXIT=0 (3511 jobs); lake build Definitions.FLM861BookProducer EXIT=0 (3512 jobs); lake build Definitions.FLM861BookProducer Definitions.FLM889Book Definitions.FLM8102Book FinalCheck EXIT=0 (9175 jobs) with NINE 'declaration uses sorry' warnings, TWO of them in this cone (the two pieces; Transport has none); lake env lean Refuted/MMFLM861BookBridgeRefute.lean EXIT=0 and Refuted/MMFLM861BookFieldRefute.lean EXIT=0, both SILENT (every #guard_msgs matched); Probe/forbidden_tokens.py on the touched files: admit=0 axiom=0 native_decide=0, sorry only where registered (the new module 2, FLM889Book 1, FLM8102Book 2, the two 8.6.25/8.6.27 halves, #2, moonshine); the three book-facing statements byte-identical (3 blocks, 0 mismatches).

Next for this line: (a) isVertexOperator_unique --- its docstring names the exact remaining pieces (the q-window confinement of azPowD, the two truncation facts of IsNormalOrder via MM.FLM85Ac.modeVL_exists_eq_zero / Factor.bound_spec, and the spanning of V_L by stateOf D); (b) zAligned_isVertexOperator --- the producer's rectangle window against MM.FLM84LF.YFam and its IsFold half at the book's h-valued StateDatum.  Records: NOTES.md section 277; HANDOVER.md sections 0 and 6.
