=== MMFLM810CreationIntertwine.lean
  124: Yzero_trunc
  155: YzeroField
  159: YzeroField_fam
  166: YzeroField_stateOfVL
  221: Yzero_modeVL_eq_actionFamily
  249: Yzero_modeVL_eq_actionFamily_nat
  273: Yzero_modeVL_iotaVL_eq_actionFamily
  288: Yzero_modeVL_neg_one_iotaVL_eq_actionFamily
  300: Yzero_modeVL_eq_actionFamily_modelBase
=== MMFLM810CurrentFieldComm.lean
  299: modeVL_YFam_add
=== MMFLM810DFoldAssembly.lean
  220: Yzero_sugawaraModeZero_modeVL
=== MMFLM810JacobiZeroFace.lean
  141: Yaligned_ne_Yzero_modelBaseField
=== MMFLM810NegOneChambersClose.lean
   66: YFam_mul_comm_of_cocycleCompatible
=== MMFLM810TheoremNoOrth.lean
  102: Yzero_baseRepaired_eq_Yaligned
=== MMFLM810TranslationBase.lean
   92: reflectFam_YFam_eq_zero_of_lt
  207: YFam_zero_label
  299: Yzero_baseRepaired_stateOfVL_singleton
=== MMFLM810TranslationCorrected.lean
  111: Yzero_iotaVL_eq_modelBase
  121: Yzero_modeVL_eq_actionFamily
=== MMFLM810TranslationDerivationState.lean
   74: Yzero_modeVL_iotaVL
   87: Yzero_modeVL_modeVL_iotaVL
  128: Yzero_LOf_conformalVectorZero_neg_one_stateOfVL
=== MMFLM810TranslationGeneral.lean
  392: Yzero_eq_actionFold_datumFactors
=== MMFLM810TranslationStateObstruction.lean
  132: Yzero_modelBase_modeVL_neg_one_iotaVL
=== MMFLM810ZeroModeL0Uncond.lean
   87: Yzero_spec
  100: Yzero_unique
=== MMFLM84LatticeField.lean
  720: YFam
  726: YFam_apply
  738: YFam_eq_convWith_assoc
  770: YFam_iotaVL
  799: YFam_iotaVL_eq_exp
  808: YFam_vacuumVL
  822: YFam_vacuumVL_eq_YCoeff
  870: YFam_eq_zero_of_gt
  997: rankOne_YFam_neg_two_ne_zero
 1018: rankOne_YFam_neg_two_eq_YCoeff
 1031: rankOne_YFam_zero_eq_zero
=== MMFLM84TwoVarProduct.lean
  407: YFam_eq_sum_mid_annih
  421: YFam_eq_sum_three_factor
=== MMFLM85BaseFieldAligned.lean
   85: genFam
   89: genFam_apply
   94: genFam_eq_reflectFam
  101: genFam_iotaVL
  108: genFam_iotaVL_eq_exp
  115: genFam_zero_label
  123: genFam_vacuumVL_eq_modelBase
  138: genFam_lower_truncation_vacuum
  149: YFam_eq_zero_of_nonneg_vacuum
  159: genFam_vacuum_creates
  167: genFam_lower_truncation_iotaVL
  175: genFam_iotaVL_pairing_eq
  185: genFam_eq_zero_of_lt
  203: genFam_lower_truncation_false
  216: genFam_lower_truncation_false_rankOne
  269: genFam_ne_modelBase
=== MMFLM85CanonicalField.lean
  263: YFam_pointer
=== MMFLM85FockStrict.lean
  578: not_bdd_YFam_of_functional
  604: not_bdd_YFam_of_ne_zero
  622: not_cfield_YFam_of_ne_zero
=== MMFLM85OneSidedProduct.lean
  108: coefVanishesAbove_YFam
=== MMFLM85PrescriptionCoeff.lean
  103: ZAligned_creationStep
=== MMFLM85PrescriptionCoeffLevel.lean
  103: shiftCoef_one_YFam
=== MMFLM86CoherentCreatedPosRankOne.lean
  232: YFam_rankOne_summand
=== MMFLM86CoherentField.lean
  215: ZAligned_eq_reflectFam_YzeroField
  226: YzeroField_creationExpVL_fam
=== MMFLM86CommIota.lean
   74: commutator_YFam_eq_twoVarField_sub_swap2
   99: commutator_YFam_eq_smul_twoVarField_of_nonneg
  111: commutator_YFam_eq_smul_mul_of_nonneg
  123: commutator_YFam_eq_sum_ratioCoeff_of_nonneg
  145: commutator_YFam_eq_zero_of_cocycle
  186: commutator_YFam_eq_zero_of_even
  251: not_YFamOnGenerators_and_corollary851_rankOne
  321: commutator_YFam_eq_eps_smul_of_pairing_neg_one
=== MMFLM86Contraction8612.lean
  328: YFam_eq_sum_three_factor_of_mem
=== MMFLM86Corollary851ModeStepAux.lean
  248: Yzero_modeVL_add
  261: Yzero_modeVL_smul
=== MMFLM86Corollary851ModeStepExistsAux.lean
  149: modeVL_YFam_add_ne
=== MMFLM86DerivDictionary.lean
  141: Yzero_modeVL_neg_one
  289: YzeroField_smul_fam
=== MMFLM86ExpProduct.lean
  148: Yzero_iotaVL_eq_modelBase
  158: Yzero_iotaVL_apply
  185: Yzero_iotaVL_mul_Yzero_iotaVL
  209: Yzero_iotaVL_apply_iotaVL
  229: Yzero_iotaVL_apply_iotaVL_eq_YFam
  253: commutatorFamily_Yzero_iotaVL
  275: commutatorFamily_Yzero_iotaVL_eq_c
=== MMFLM86FlatReassembly.lean
  221: genFam_iotaVL
=== MMFLM86IterateIota.lean
   68: YFamOnGenerators
=== MMFLM86MixedProduct.lean
  252: YFamBridge
=== MMFLM86ModeFieldCommAnnProveAux.lean
   74: Yzero_modeVL_fam
   93: Yzero_modeVL_window
=== MMFLM86ModeLawTwo.lean
  310: YzeroField_iotaVL
  318: YzeroField_anchorVL
  326: YzeroField_creationExpVL_one_anchor
  338: YzeroField_creationExpVL_one_iota_fam
=== MMFLM86NegPairingNonvacAnchor.lean
  117: creationExpVL_eq_YFam_vacuum
  138: creationExpVL_zero_eq_YFam_vacuum
=== MMFLM86ShiftedDeriv.lean
  165: shiftedCreationDerivation_YFam
=== MMFLM86ShiftedDerivation.lean
   55: YFamModeDerivation
   65: YFamShiftedDerivation
   76: shiftedCreationDerivation_iff_YFamShiftedDerivation
   90: YFamShiftedDerivation_of_modeDerivation
  120: YFamDerivationBase
=== MMFLM86ShiftedDerivationAux.lean
   90: Yaligned_eq_Yzero_baseRepaired
  112: ZAligned_iotaVL_eq_YFam
  119: ZAligned_iotaVL_eq_YFam_apply
  136: YFam_zero_neg_one_vacuum
=== MMFLM86TailContraction.lean
  327: hZeroVL_YFam_add
  437: modeVL_YFam_add_pos
  496: splitPlus_heisFamZero_YFam_add
=== MMFLM86YFamDerivationAux.lean
   90: YFamResidualAt
=== MMFLM86YFamProduct.lean
  113: YFam_mul_eq_twoVarField
  128: YFam_mul_YFam_iotaVL
  136: YFam_mul_YFam_iotaVL_eq_exp
  153: YFam_mul_apply_eq_sum_ratioCoeff
  165: YFam_mul_eq_sum_ratioCoeff
  181: YFam_mul_eq_convWith2_contrFam
  209: YFam_mul_YFam_iotaVL_eq_sum
  228: YFam_mul_eq_normOrdered2_of_form_eq_zero
  245: YFam_mul_rankOne_negTwo_vacuum
  263: YFam_mul_rankOne_negTwo_vacuum_ne_zero
=== MMFLM86YzeroIsYFam.lean
   87: Yzero_iotaVL_apply_iotaVL
  100: Yzero_iotaVL_vacuum_eq_reflectFam
  112: Yzero_iterateStateFamily_latticeState
  125: Yzero_iotaVL_zero_apply
  135: Yzero_iotaVL_zero_vacuum
  145: YFam_apply_zero_vacuum
  158: not_YFamOnGenerators_modelBaseField
=== MMFLM86ZLineInduction.lean
  589: zLineVal_zero_eq_genFam
  601: modeVL_genFam_apply
=== MMFLM86ZOneFockOne.lean
  443: modeVL_genFam_sub
=== MMFLMRepairNaming.lean
  340: YFamTwoSidedWindow
  351: not_YFamTwoSidedWindow_of_ne_zero
