### MM.FLM88.  (133 hits)
   Definitions/MMFLM810Assembly.lean:251: `MM.FLM88.jacobiIdentity_zero_face_of_corollary851`, here in the iterate currency of the target. -/
   Definitions/MMFLM810Axioms.lean:17: repaired that by conjoining the landed `MM.FLM88.CrossWindow`; task W7 replaced that conjunct by the
   Definitions/MMFLM810Axioms.lean:138: | (8.10.8) | `JacobiAxiom` | `MM.FLM88.JacobiIdentity` -- the component form of Theorem 8.8.9 -- **together with** the f
   Definitions/MMFLM810Axioms.lean:162: windows (`jacobiAxiom_iff_deltaForm`, from the landed `MM.FLM88.jacobiIdentity_iff_delta` and the
   Definitions/MMFLM810Axioms.lean:182: (8.10.7) for `V_L`; (8.10.8) for `V_L` (the landed `MM.FLM88.JacobiIdentity` is *stated* there, not
   Definitions/MMFLM810Axioms.lean:183: proved, and `MM.FLM88.corollary851_iff_jacobiIdentity_zero_face` records that the whole route's open
   Definitions/MMFLM810Axioms.lean:345: the coefficient of each monomial in the formal variables is a finite sum".  `MM.FLM88.JacobiIdentity`
   Definitions/MMFLM810Axioms.lean:347: `MM.FLM88.JacobiDelta` is (8.8.29) read coefficientwise; the landed
### namespace FLM810NCFC  (1 hits)
   Definitions/MMFLM810NegCFaceClosed.lean:46: namespace FLM810NCFC
### namespace FLM810NCF  (3 hits)
   Definitions/MMFLM810NegCFace.lean:84: namespace FLM810NCF
   Definitions/MMFLM810NegCFaceClosed.lean:46: namespace FLM810NCFC
   Definitions/MMFLM810NegCFaceJ.lean:79: namespace FLM810NCFJ
### namespace FLM810ASM  (2 hits)
   Definitions/MMFLM810Assembly.lean:83: namespace FLM810ASM
   Definitions/MMFLM810AssemblySlices.lean:35: namespace FLM810ASM
### namespace FLM86M8625P  (3 hits)
   Definitions/MMFLM86Insertion8625Prove.lean:99: namespace FLM86M8625P
   Definitions/MMFLM86Insertion8625ProveAux.lean:79: namespace FLM86M8625P
   Definitions/MMFLM86Insertion8625ProveFalsify.lean:52: namespace FLM86M8625P
### theorem8102_of_matching_and_groundedStep  (10 hits)
   Definitions/MMFLM86WindowSyncAbsorbed.lean:133: #check @MM.FLM86WSD.theorem8102_of_matching_and_groundedStep
   Definitions/MMFLM86WindowSyncAbsorbed.lean:329: `theorem8102_of_matching_and_groundedStep` with residual #1 replaced by the honest commutator half of
   Definitions/MMFLM86WindowSyncAbsorbed.lean:343: theorem8102_of_matching_and_groundedStep (F := F) bL form hnd hs C h2 S hpd hW hfin hmatch
   Definitions/MMFLM86WindowSyncDelivery.lean:27: * allStates_of_matching_and_groundedStep and theorem8102_of_matching_and_groundedStep: batch 223-B's
   Definitions/MMFLM86WindowSyncDelivery.lean:35: `NegativeResidual`, the six boundary inputs of `theorem8102_of_matching_and_groundedStep`, Theorem
   Definitions/MMFLM86WindowSyncDelivery.lean:125: theorem theorem8102_of_matching_and_groundedStep
   Definitions/MMFLM86WindowSyncDelivery.lean:153: /-- info: 'MM.FLM86WSD.theorem8102_of_matching_and_groundedStep' depends on axioms: [propext, Classical.choice, Quot.sou
   Definitions/MMFLM86WindowSyncDelivery.lean:155: #print axioms MM.FLM86WSD.theorem8102_of_matching_and_groundedStep
### theorem8102_of_matching_and_commutatorHalf  (6 hits)
   Definitions/MMFLM86WindowSyncAbsorbed.lean:58: `theorem8102_of_matching_and_commutatorHalf`: the assembly's grounded `Res_{z_0}` face, the reduced
   Definitions/MMFLM86WindowSyncAbsorbed.lean:332: theorem theorem8102_of_matching_and_commutatorHalf
   Definitions/MMFLM86WindowSyncAbsorbed.lean:405: /-- info: 'MM.FLM86WSA.theorem8102_of_matching_and_commutatorHalf' depends on axioms: [propext, Classical.choice, Quot.s
   Definitions/MMFLM86WindowSyncAbsorbed.lean:407: #print axioms MM.FLM86WSA.theorem8102_of_matching_and_commutatorHalf
   HANDOVER.md:38: (`MM.FLM86WSA.theorem8102_of_matching_and_commutatorHalf`).
   ROADMAP.md:8216: NegativeResidual), theorem8102_of_matching_and_commutatorHalf (**FLM Theorem 8.10.2 on the display
### theorem8102_of_correctedResiduals  (10 hits)
   Definitions/MMFLM810BoundaryCorrected.lean:400: theorem theorem8102_of_correctedResiduals
   Definitions/MMFLM810BoundaryCorrected.lean:414: `theorem8102_of_correctedResiduals` by section 2's both-way normal-form theorem. -/
   Definitions/MMFLM810BoundaryCorrected.lean:424: theorem8102_of_correctedResiduals (F := F) bL form hnd hs C h2 S hpd hW hfin
   Definitions/MMFLM810BoundaryCorrected.lean:465: /-- info: 'MM.FLM810BC.theorem8102_of_correctedResiduals' depends on axioms: [propext, Classical.choice, Quot.sound] -/
   Definitions/MMFLM810BoundaryCorrected.lean:466: #guard_msgs in #print axioms MM.FLM810BC.theorem8102_of_correctedResiduals
   Definitions/MMFLM86Insertion8625Prove.lean:127: #check @MM.FLM810BC.theorem8102_of_correctedResiduals
   Definitions/MMFLM86Insertion8625Prove.lean:275: MM.FLM810BC.theorem8102_of_correctedResiduals with the package hypothesis built from the matching
   Definitions/MMFLM86Insertion8625Prove.lean:289: theorem8102_of_correctedResiduals (F := F) bL form hnd hs C h2 S hpd hW hfin
### ResidueMatching8625NegSecondSlot  (38 hits)
   Definitions/MMFLM810BoundaryCorrected.lean:48: MM.FLM86M8625.ResidueMatching8625NegSecondSlot E (the l >= 1 slot), strictly additional to l = 0
   Definitions/MMFLM810BoundaryCorrected.lean:115: only at the lattice generators) and ResidueMatching8625NegSecondSlot (open), and its Jacobi half
   Definitions/MMFLM810BoundaryCorrected.lean:166: #check @MM.FLM86M8625.ResidueMatching8625NegSecondSlot
   Definitions/MMFLM810BoundaryCorrected.lean:196: `HonestNegPairingCoeff` (at arbitrary `w`) and `ResidueMatching8625NegSecondSlot`;
   Definitions/MMFLM810BoundaryCorrected.lean:217: `MM.FLM86M8625.ResidueMatching8625NegSecondSlot` at `l >= 1`), the named residual list of
   Definitions/MMFLM810BoundaryCorrected.lean:222: ∧ ResidueMatching8625NegSecondSlot (F := F) bL form (C.toCentralExtension (F := F) h2)
   Definitions/MMFLM810BoundaryCorrected.lean:261: `HonestNegPairingCoeff /\ ResidueMatching8625NegSecondSlot`. -/
   Definitions/MMFLM810BoundaryCorrected.lean:266: ResidueMatching8625NegSecondSlot (F := F) bL form (C.toCentralExtension (F := F) h2) :=
### honestIns8625  (91 hits)
   Definitions/MMFLM86DisplayPair.lean:17: `MM.FLM86M8625.CommutatorInsertion8625 E (MM.FLM86M8625P.honestIns8625 E)` --- IS FLM's displayed
   Definitions/MMFLM86DisplayPair.lean:26: `CommutatorInsertion8625 E (honestIns8625 E)` (the inert labels dropped, both ways) --- so the
   Definitions/MMFLM86DisplayPair.lean:57: `DisplayAllStates (ZAligned E)` (equivalently `CommutatorInsertion8625 E (honestIns8625 E)`,
   Definitions/MMFLM86DisplayPair.lean:98: #check @MM.FLM86M8625P.honestIns8625
   Definitions/MMFLM86DisplayPair.lean:99: #check @MM.FLM86M8625P.honestIns8625_apply
   Definitions/MMFLM86DisplayPair.lean:134: ↔ CommutatorInsertion8625 (F := F) bL form E (honestIns8625 (F := F) bL form E) := by
   Definitions/MMFLM86DisplayPair.lean:141: rw [← honestIns8625_family (F := F) bL form E a b c r]
   Definitions/MMFLM86DisplayPair.lean:143: simpa only [corollary851Residue, honestIns8625] using h1
