### crossBracket_eq_crossIterate_of_nonneg_of_grounded  (7)
   Definitions/MMFLM810Assembly.lean:317: · refine FLM810ASA.crossBracket_eq_crossIterate_of_nonneg_of_grounded (F := F)
   Definitions/MMFLM810AssemblyAux.lean:245: theorem crossBracket_eq_crossIterate_of_nonneg_of_grounded (Y : M →ₗ[F] CoefFamily F M) (a b : M)
   Definitions/MMFLM810AssemblyAux.lean:382: /-- info: 'MM.FLM810ASA.crossBracket_eq_crossIterate_of_nonneg_of_grounded' depends on axioms: [propext,
   Definitions/MMFLM810AssemblyAux.lean:385: #guard_msgs in #print axioms MM.FLM810ASA.crossBracket_eq_crossIterate_of_nonneg_of_grounded
   Definitions/MMFLM86WindowSyncDelivery.lean:83: MM.FLM810ASM.crossBracket_eq_crossIterate_of_nonneg_of_grounded.  Composition: the step IS the
   HANDOVER.md:68: of (8.8.41) are PROVED not residual (`crossBracket_eq_crossIterate_of_nonneg_of_grounded`).
   HANDOVER.md:94: | (8.8.41) `l >= 0` faces, every state/pairing | `MM.FLM810ASM.crossBracket_eq_crossIterate_of_nonneg_of_grounded` |
### namespace FLM810ASA  (1)
   Definitions/MMFLM810AssemblyAux.lean:69: namespace FLM810ASA
### namespace FLM810ASM  (2)
   Definitions/MMFLM810Assembly.lean:83: namespace FLM810ASM
   Definitions/MMFLM810AssemblySlices.lean:35: namespace FLM810ASM
### negCFaceAligned_evenCocycle  (17)
   Definitions/MMFLM810Assembly.lean:35: The second row of the last line is batch 202's `MM.FLM810NCFC.negCFaceAligned_evenCocycle`: every
   Definitions/MMFLM810Assembly.lean:161: batch-202 theorem `MM.FLM810NCFC.negCFaceAligned_evenCocycle` covers, in the currency of the target.
   Definitions/MMFLM810AssemblySlices.lean:53: generators with `0 <= <a,b>` --- the composition `MM.FLM810NCFC.negCFaceAligned_evenCocycle` of the
   Definitions/MMFLM810AssemblySlices.lean:67: exact FLM810NCFC.negCFaceAligned_evenCocycle (F := F) bL form C h2 hs hc a b hab m n
   Definitions/MMFLM810NegCFace.lean:63: (`negCFaceAligned_evenCocycle`, `negCBinomMomentAligned_of_negCFaceAligned`).
   Definitions/MMFLM810NegCFace.lean:467: theorem negCFaceAligned_evenCocycle (C : EvenCocycle L form) (h2 : (2 : F) ≠ 0)
   Definitions/MMFLM810NegCFace.lean:539: negCFaceAligned_evenCocycle (F := F) bL form C h2 hs hc⟩
   Definitions/MMFLM810NegCFace.lean:572: /-- info: 'MM.FLM810NCF.negCFaceAligned_evenCocycle' depends on axioms: [propext, Classical.choice, Quot.sound] -/
   Definitions/MMFLM810NegCFace.lean:573: #guard_msgs in #print axioms MM.FLM810NCF.negCFaceAligned_evenCocycle
   Definitions/MMFLM810NegCFaceClosed.lean:84: theorem negCFaceAligned_evenCocycle (C : EvenCocycle L form) (h2 : (2 : F) ≠ 0)
### MM.FLM810NCFC.negCFaceAligned  (6)
   Definitions/MMFLM810Assembly.lean:35: The second row of the last line is batch 202's `MM.FLM810NCFC.negCFaceAligned_evenCocycle`: every
   Definitions/MMFLM810Assembly.lean:161: batch-202 theorem `MM.FLM810NCFC.negCFaceAligned_evenCocycle` covers, in the currency of the target.
   Definitions/MMFLM810AssemblySlices.lean:53: generators with `0 <= <a,b>` --- the composition `MM.FLM810NCFC.negCFaceAligned_evenCocycle` of the
   Definitions/MMFLM810NegCFaceClosed.lean:104: /-- info: 'MM.FLM810NCFC.negCFaceAligned_evenCocycle' depends on axioms: [propext, Classical.choice, Quot.sound] -/
   Definitions/MMFLM810NegCFaceClosed.lean:106: #print axioms MM.FLM810NCFC.negCFaceAligned_evenCocycle
   HANDOVER.md:95: | (8.8.41) `l = -c`, generator `0 <= <a,b>` chamber | `MM.FLM810NCFC.negCFaceAligned_evenCocycle` |
