### namespace FLM86NTP  (2)
   Definitions/MMFLM86NegThreeProve.lean:66: namespace FLM86NTP
   Definitions/MMFLM86NegThreeProveAux.lean:85: namespace FLM86NTP
### negThreeExpandedResidualAligned_evenCocycle  (12)
   Definitions/MMFLM810BoundaryCorrected.lean:59: | NegThreeExpandedResidualAligned E (FLM (8.5.13) at <a,b> <= -3, expanded) | MM.FLM86NTP.negThreeExpandedResi
   Definitions/MMFLM810BoundaryCorrected.lean:160: #check @MM.FLM86NTP.negThreeExpandedResidualAligned_evenCocycle
   Definitions/MMFLM810BoundaryCorrected.lean:298: FLM86NTP.negThreeExpandedResidualAligned_evenCocycle (F := F) bL form C h2 hs,
   Definitions/MMFLM810BoundaryCorrected.lean:320: FLM86NTP.negThreeExpandedResidualAligned_evenCocycle (F := F) bL form C h2 hs,
   Definitions/MMFLM810BoundaryReduced.lean:58: | `NegThreeExpandedResidualAligned E` | `MM.FLM86NTP.negThreeExpandedResidualAligned_evenCocycle` (batch 204-A
### residueNegativeAligned_evenCocycle  (64)
   Definitions/MMFLM810BoundaryCorrected.lean:76: the landed lattice corner (MM.FLM86NTP.residueNegativeAligned_evenCocycle) gives the (8.5.4)
   Definitions/MMFLM810BoundaryCorrected.lean:161: #check @MM.FLM86NTP.residueNegativeAligned_evenCocycle
   Definitions/MMFLM810BoundaryCorrected.lean:360: `MM.FLM86NTP.residueNegativeAligned_evenCocycle` (batch 204-A) turns it into the (8.5.4)-states
   Definitions/MMFLM810BoundaryCorrected.lean:372: FLM86NTP.residueNegativeAligned_evenCocycle (F := F) bL form C h2 hs
   Definitions/MMFLM810HonestAudit.lean:54: | `MM.FLM810TE.residueNegativeAligned_evenCocycle_of_residuals` | package hypothesis FALSE | the `iff` form be
### spanningGrounded_iff_eventual  (13)
   Definitions/MMFLM810AssemblyGrounded.lean:18: (`MM.FLM86SL.spanningGrounded_iff_eventual`, both ways).  This file performs the remaining bookkeeping:
   Definitions/MMFLM810AssemblyGrounded.lean:107: have hgr := (spanningGrounded_iff_eventual (F := F) bL form
   Definitions/MMFLM86Insertion8625ProveAux.lean:218: spanningGrounded_iff_eventual).  Forward: a grounded window is raised to every larger window by
   Definitions/MMFLM86SourceBridge.lean:44: (`MM.FLM86SL.spanningGrounded_iff_eventual`), hence the grounded `Res_{z_0}` face at all states
   Definitions/MMFLM86SourceBridge.lean:178: spanning eventual windows (`MM.FLM86SL.spanningGrounded_iff_eventual`), hence the grounded `Res_{z_0}`
### def spanningGrounded  (0)
### namespace FLM86SL  (2)
   Definitions/MMFLM86Slice.lean:101: namespace FLM86SL
   Definitions/MMFLM86SpanningLift.lean:95: namespace FLM86SL
### namespace FLM86WS  (3)
   Definitions/MMFLM86WindowSync.lean:82: namespace FLM86WS
   Definitions/MMFLM86WindowSyncAbsorbed.lean:100: namespace FLM86WSA
   Definitions/MMFLM86WindowSyncDelivery.lean:54: namespace FLM86WSD
### namespace FLM86DP  (1)
   Definitions/MMFLM86DisplayPair.lean:79: namespace FLM86DP
### namespace FLM86TDA  (1)
   Definitions/MMFLM86TheoremDisplay.lean:22: namespace FLM86TDA
### namespace FLM86SB  (1)
   Definitions/MMFLM86SourceBridge.lean:75: namespace FLM86SB
### namespace FLM810ASG  (1)
   Definitions/MMFLM810AssemblyGrounded.lean:50: namespace FLM810ASG
### namespace FLM810RR  (1)
   Definitions/MMFLM810RemainingReduction.lean:30: namespace FLM810RR
### namespace FLM810JZF  (1)
   Definitions/MMFLM810JacobiZeroFace.lean:99: namespace FLM810JZF
### namespace FLM810T861A  (1)
   Definitions/MMFLM810Theorem861Aligned.lean:112: namespace FLM810T861A
