### def DisplayModeStep
   MMFLM86DisplayPair.lean:210: def DisplayModeStep (Y : VL F L →ₗ[F] CoefFamily F (VL F L)) : Prop :=
### def DisplayAllStates
   MMFLM86DisplayPair.lean:126: def DisplayAllStates (Y : VL F L →ₗ[F] CoefFamily F (VL F L)) : Prop :=
### Corollary851SpanningEventualWindows
   MMFLM86SpanningLift.lean:115: def Corollary851SpanningEventualWindows
### def GroundedModeStepAtStates
   MMFLM86WindowSync.lean:136: def GroundedModeStepAtStates (Y : VL F L →ₗ[F] CoefFamily F (VL F L)) : Prop :=
### groundedModeStep_of_commutatorInsertion
   MMFLM86WindowSyncAbsorbed.lean:264: theorem groundedModeStep_of_commutatorInsertion (E : CentralExtension F L)
### def CommutatorInsertion8625
   MMFLM86Matching8625.lean:193: def CommutatorInsertion8625 (E : CentralExtension F L)
### honestIns8625
   MMFLM86Insertion8625ProveAux.lean:116: def honestIns8625 (E : CentralExtension F L) :
   MMFLM86Insertion8625ProveAux.lean:121: theorem honestIns8625_apply (E : CentralExtension F L) (a b : VL F L) (c : L) (r : Nat)
   MMFLM86Insertion8625ProveAux.lean:129: theorem honestIns8625_family (E : CentralExtension F L) (a b : VL F L) (c : L) (r : Nat) :
   MMFLM86Insertion8625ProveAux.lean:136: theorem honestIns8625_eq_zero_iff (E : CentralExtension F L) (a b : VL F L) (c : L) (r : Nat)
   MMFLM86Insertion8625ProveFalsify.lean:81: theorem honestIns8625_ne_zero (E : CentralExtension F L) (a b : L) :
### def JacobiAxiom
   MMFLM810Axioms.lean:355: def JacobiAxiom (Y : VertexOp F V) : Prop := ∀ u v : V, ∃ N : ℕ, JacobiIdentity Y.coeff u v N
   MMFLM810Axioms.lean:438: def JacobiAxiom (Y : VertexOp F V) : Prop :=
   MMFLM810JacobiNamedBridgeAux.lean:164: def JacobiAxiomUnconstrained (Y : VertexOp F V) : Prop :=
### def JacobiOnStateTargets
   MMFLM810RemainingReduction.lean:166: def JacobiOnStateTargets (bL : Module.Basis κ ℤ L)
### yFamOnGenerators_vertexOpOfField_Yaligned
   MMFLM810JacobiZeroFace.lean:128: theorem yFamOnGenerators_vertexOpOfField_Yaligned (E : CentralExtension F L) :
### crossBracket_eq_crossIterate_of_nonneg_of_grounded
   MMFLM810AssemblyAux.lean:245: theorem crossBracket_eq_crossIterate_of_nonneg_of_grounded (Y : M →ₗ[F] CoefFamily F M) (a b : M)
### negCFaceAligned_evenCocycle
   MMFLM810NegCFace.lean:467: theorem negCFaceAligned_evenCocycle (C : EvenCocycle L form) (h2 : (2 : F) ≠ 0)
   MMFLM810NegCFaceClosed.lean:84: theorem negCFaceAligned_evenCocycle (C : EvenCocycle L form) (h2 : (2 : F) ≠ 0)
   MMFLM86HarvestAllPairingsFaces.lean:241: theorem negCFaceAligned_evenCocycle_iff_below (C : EvenCocycle L form) (h2 : (2 : F) ≠ 0)
### groundedPairWindow_iff_aboveThreshold
   MMFLM86WindowSyncAbsorbed.lean:150: theorem groundedPairWindow_iff_aboveThreshold {Y : VL F L →ₗ[F] CoefFamily F (VL F L)}
### displayAtPair_zAligned_iff_groundedPairWindow
   MMFLM86DisplayPair.lean:175: theorem displayAtPair_zAligned_iff_groundedPairWindow (E : CentralExtension F L) (u v : VL F L) :
### displayAllStates_iff_groundedAllStates
   MMFLM86DisplayPair.lean:186: theorem displayAllStates_iff_groundedAllStates (E : CentralExtension F L) :
### jacobiAxiom_of_stateTargets
   MMFLM810RemainingReduction.lean:180: theorem jacobiAxiom_of_stateTargets (bL : Module.Basis κ ℤ L)
### def JacobiIdentity
   MMFLM810JacobiToBridge.lean:333: def JacobiIdentityStable (Y : V →ₗ[F] CoefFamily F V) (a b : V) : Prop :=
   MMFLM88Jacobi.lean:451: def JacobiIdentity (Y : M →ₗ[F] CoefFamily F M) (a b : M) (N : ℕ) : Prop :=
### def JacobiDelta
   MMFLM88Jacobi.lean:457: def JacobiDelta (Y : M →ₗ[F] CoefFamily F M) (a b : M) (N : ℕ) : Prop :=
### def FaithfulJacobi
   MMFLM810JacobiFaithful.lean:290: def FaithfulJacobi (Y : M →ₗ[F] CoefFamily F M) (a b : M) : Prop :=
   MMFLM810JacobiFaithful.lean:296: def FaithfulJacobiStable (Y : M →ₗ[F] CoefFamily F M) (a b : M) : Prop :=
### def Theorem8102
   MMFLM810Axioms.lean:796: def Theorem8102Conclusion (form : L →ₗ[ℤ] L →ₗ[ℤ] ℤ) (r : ℚ) : Prop :=
   MMFLM810Axioms.lean:825: def Theorem8102 (form : L →ₗ[ℤ] L →ₗ[ℤ] ℤ) (r : ℚ) : Prop :=
