MM.MM.FLM810ASA.crossBracket_eq_crossIterate_of_nonneg_of_grounded MMFLM810AssemblyAux.lean:245
MM.MM.FLM810ASM.negativeFaces_of_residual                  MMFLM810AssemblySlices.lean:100
MM.MM.FLM86M8625.residueMatching8625_iff_coeff_and_slot    MMFLM86Matching8625.lean:159
MM.MM.FLM86M8625.honestBlockCoeffJL_one_rankOne            MMFLM86Matching8625Aux.lean:261
MM.MM.FLM86NPCL.honestNegPairingCoeff_iff_atStates         MMFLM86NegPairingCoeffAll.lean:345
MM.MM.FLM86NPFS.fockStep_imp_oneMode                       MMFLM86NegPairingFockStep.lean:144
MM.MM.FLM86NPFS.faceAtFamily_lattice                       MMFLM86NegPairingFockStep.lean:160
MM.MM.FLM86NPFS.honestNegPairingCoeffAtStates_iff_fockStep MMFLM86NegPairingFockStep.lean:193
MM.MM.FLM86WSA.groundedModeStep_of_commutatorInsertion     MMFLM86WindowSyncAbsorbed.lean:264
MM.MM.FLM86WSA.stepCorrected_of_commutatorHalf             MMFLM86WindowSyncAbsorbed.lean:318
MM.MM.FLM86WSD.allStates_of_matching_and_groundedStep      MMFLM86WindowSyncDelivery.lean:110
