Batch 243-A ACCEPTED -- Theorem 8.8.9 (source-faithful) is ASSEMBLED (protocol (b)): the register now holds the two halves of (8.8.41)

Eliminated one open input and registered one sharper one, per the batch protocol.

* ELIMINATED: MM.FLM88T889S.theorem889_faithful (MM.FLM810ASM.FacesAtStates, Theorem 8.8.9 in the
  source-faithful face form) is no longer a `sorry`.  It is assembled from the two registered inputs
  through the landed slices: MM.FLM810ASM.faces_of_groundedZeroFace applied to the grounded display
  (MM.FLM810CCG.groundedZeroFace_evenCocycle, batch 242-A) and the negative residual
  (MM.FLM810NRA.negativeResidual_aligned, this batch).  The l > 0 slice is a theorem from the grounded
  face plus the landed (8.10.5) finiteness (MM.FLM810ASM.faceWindows_zAligned).
* REGISTERED (new file Definitions/MMFLM810NegativeResidualAligned.lean, MM.FLM810NRA):
  MM.FLM810NRA.negativeResidual_aligned -- the l < 0 faces of (8.8.41) at the honest field, off the
  landed generator chamber (MM.FLM810ASM.NegativeOnGenerators / negativeOnGenerators_zAligned, batch
  202).  This is the (8.6.25)/(8.6.27) matching's free-field half: the mode action on the
  normally-ordered blocks.  Also derived there: negativeFaces_aligned (the whole l < 0 slice, by the
  landed MM.FLM810ASM.negativeFaces_of_residual).  Guarded: [propext, sorryAx, Classical.choice,
  Quot.sound].
* The register now holds the two halves of (8.8.41): the grounded l = 0 face (the display; batch
  242-A's entry) and the l < 0 residual (this batch's entry).  Both are the section 8.6 engine: the
  former is its commutator/display output, the latter its Fock output (the mode action on the
  normally-ordered blocks, with batch 233's reindexing and batch 240-A's l-general window/coefficient
  layer already landed toward it).
* The form symmetry hs now threads through theorem889_faithful (the generator chamber needs it), and
  the 8.10.2 file's two call sites were updated accordingly; all footprints unchanged.
* Naming: the 8.8.9 file's prose was swept of campaign terms at the owner's instruction.

Build: the new module, the 8.8.9 file and the 8.10.2 file all --- OK ---; FinalCheck.lean GREEN;
HANDOVER.md section 1.1 records the elimination and the sharpened entry.
