=== Definitions/MMFLM88Jacobi.lean
=== Definitions/MMFLM810Assembly.lean
  326: /-- info: 'MM.FLM810ASM.NegativeOnGenerators' depends on axioms: [propext, Classical.choice, Quot.sound] -/
  327: #guard_msgs in #print axioms MM.FLM810ASM.NegativeOnGenerators
  329: /-- info: 'MM.FLM810ASM.FacesAtStates' depends on axioms: [propext, Classical.choice, Quot.sound] -/
  330: #guard_msgs in #print axioms MM.FLM810ASM.FacesAtStates
  332: /-- info: 'MM.FLM810ASM.FaceWindows' depends on axioms: [propext, Classical.choice, Quot.sound] -/
  333: #guard_msgs in #print axioms MM.FLM810ASM.FaceWindows
  335: /-- info: 'MM.FLM810ASM.ZeroFaces' depends on axioms: [propext, Classical.choice, Quot.sound] -/
  336: #guard_msgs in #print axioms MM.FLM810ASM.ZeroFaces
  338: /-- info: 'MM.FLM810ASM.PositiveFaces' depends on axioms: [propext, Classical.choice, Quot.sound] -/
  339: #guard_msgs in #print axioms MM.FLM810ASM.PositiveFaces
  341: /-- info: 'MM.FLM810ASM.NegativeFaces' depends on axioms: [propext, Classical.choice, Quot.sound] -/
  342: #guard_msgs in #print axioms MM.FLM810ASM.NegativeFaces
  344: /-- info: 'MM.FLM810ASM.NegativeResidual' depends on axioms: [propext, Classical.choice, Quot.sound] -/
  345: #guard_msgs in #print axioms MM.FLM810ASM.NegativeResidual
  347: /-- info: 'MM.FLM810ASM.GroundedZeroFace' depends on axioms: [propext, Classical.choice, Quot.sound] -/
  348: #guard_msgs in #print axioms MM.FLM810ASM.GroundedZeroFace
  350: /-- info: 'MM.FLM810ASM.jacobiEvenCocycle_iff_faces' depends on axioms: [propext, Classical.choice, Quot.sound] -/
  351: #guard_msgs in #print axioms MM.FLM810ASM.jacobiEvenCocycle_iff_faces
  353: /-- info: 'MM.FLM810ASM.faces_iff_split' depends on axioms: [propext, Classical.choice, Quot.sound] -/
  354: #guard_msgs in #print axioms MM.FLM810ASM.faces_iff_split
  356: /-- info: 'MM.FLM810ASM.faceWindows_zAligned' depends on axioms: [propext, Classical.choice, Quot.sound] -/
  357: #guard_msgs in #print axioms MM.FLM810ASM.faceWindows_zAligned
  359: /-- info: 'MM.FLM810ASM.corollary851_iff_zeroFace' depends on axioms: [propext, Classical.choice, Quot.sound] -/
  360: #guard_msgs in #print axioms MM.FLM810ASM.corollary851_iff_zeroFace
  362: /-- info: 'MM.FLM810ASM.zeroFaces_of_groundedZeroFace' depends on axioms: [propext, Classical.choice, Quot.sound] -/
  363: #guard_msgs in #print axioms MM.FLM810ASM.zeroFaces_of_groundedZeroFace
  365: /-- info: 'MM.FLM810ASM.positiveFaces_of_groundedZeroFace' depends on axioms: [propext, Classical.choice, Quot.sound] -/
  366: #guard_msgs in #print axioms MM.FLM810ASM.positiveFaces_of_groundedZeroFace
=== Definitions/MMFLM810AssemblyGrounded.lean
  157: /-- info: 'MM.FLM810ASG.iterateOf_eq_zero_of_mem_span' depends on axioms: [propext, Classical.choice, Quot.sound] -/
  158: #guard_msgs in #print axioms MM.FLM810ASG.iterateOf_eq_zero_of_mem_span
  160: /-- info: 'MM.FLM810ASG.groundedZeroFace_of_spanningEventual' depends on axioms: [propext, Classical.choice, Quot.sound] -/
  161: #guard_msgs in #print axioms MM.FLM810ASG.groundedZeroFace_of_spanningEventual
  163: /-- info: 'MM.FLM810ASG.stepCorrected_of_spanningEventual' depends on axioms: [propext, Classical.choice, Quot.sound] -/
  164: #guard_msgs in #print axioms MM.FLM810ASG.stepCorrected_of_spanningEventual
=== Definitions/MMFLM86DisplayVOASplit.lean
  301: Every message below is the **measured** printed form from the build of this file; `#guard_msgs` fails
  306: /-- info: 'MM.FLM86DVS.UniformBracketWindow' depends on axioms: [propext, Classical.choice, Quot.sound] -/
  307: #guard_msgs in
  310: /-- info: 'MM.FLM86DVS.uniformBracketWindow_of_weight' depends on axioms: [propext, Classical.choice, Quot.sound] -/
  311: #guard_msgs in
  314: /-- info: 'MM.FLM86DVS.uniformBracketWindow_of_grading' depends on axioms: [propext, Classical.choice, Quot.sound] -/
  315: #guard_msgs in
  318: /-- info: 'MM.FLM86DVS.residue863_of_faithfulJacobi' depends on axioms: [propext, Classical.choice, Quot.sound] -/
  319: #guard_msgs in
  322: /-- info: 'MM.FLM86DVS.display863_of_faithfulJacobi_at' depends on axioms: [propext, Classical.choice, Quot.sound] -/
  323: #guard_msgs in
  326: /-- info: 'MM.FLM86DVS.display863_of_faithfulJacobi' depends on axioms: [propext, Classical.choice, Quot.sound] -/
  327: #guard_msgs in
  330: /-- info: 'MM.FLM86DVS.display863_fixed_window' depends on axioms: [propext, Classical.choice, Quot.sound] -/
  331: #guard_msgs in
  334: /-- info: 'MM.FLM86DVS.display863_of_voa_self' depends on axioms: [propext, Classical.choice, Quot.sound] -/
  335: #guard_msgs in
  338: /-- info: 'MM.FLM86DVS.display863_of_voa' depends on axioms: [propext, Classical.choice, Quot.sound] -/
  339: #guard_msgs in
  342: /-- info: 'MM.FLM86DVS.display863_of_remainingFields' depends on axioms: [propext, Classical.choice, Quot.sound] -/
  343: #guard_msgs in
=== Definitions/MMFLM810AssemblyAux.lean
  361: /-- info: 'MM.FLM810ASA.crossTerm_apply' depends on axioms: [propext, Classical.choice, Quot.sound] -/
  362: #guard_msgs in #print axioms MM.FLM810ASA.crossTerm_apply
  364: /-- info: 'MM.FLM810ASA.crossTermSwap_apply' depends on axioms: [propext, Classical.choice, Quot.sound] -/
  365: #guard_msgs in #print axioms MM.FLM810ASA.crossTermSwap_apply
  367: /-- info: 'MM.FLM810ASA.sum_crossTerm_eq_range_of_nonneg' depends on axioms: [propext, Classical.choice, Quot.sound] -/
  368: #guard_msgs in #print axioms MM.FLM810ASA.sum_crossTerm_eq_range_of_nonneg
  370: /-- info: 'MM.FLM810ASA.sum_crossTermSwap_eq_range_of_nonneg' depends on axioms: [propext, Classical.choice, Quot.sound] -/
  371: #guard_msgs in #print axioms MM.FLM810ASA.sum_crossTermSwap_eq_range_of_nonneg
  373: /-- info: 'MM.FLM810ASA.sum_crossTermSwap_eq_smul_sum' depends on axioms: [propext, Classical.choice, Quot.sound] -/
  374: #guard_msgs in #print axioms MM.FLM810ASA.sum_crossTermSwap_eq_smul_sum
  376: /-- info: 'MM.FLM810ASA.crossBracket_eq_sum_commutator_of_nonneg' depends on axioms: [propext, Classical.choice, Quot.sound] -/
  377: #guard_msgs in #print axioms MM.FLM810ASA.crossBracket_eq_sum_commutator_of_nonneg
  379: /-- info: 'MM.FLM810ASA.sum_deltaExpCoeff_mul_binomCoeff' depends on axioms: [propext, Classical.choice, Quot.sound] -/
  380: #guard_msgs in #print axioms MM.FLM810ASA.sum_deltaExpCoeff_mul_binomCoeff
  382: /-- info: 'MM.FLM810ASA.crossBracket_eq_crossIterate_of_nonneg_of_grounded' depends on axioms: [propext,
  385: #guard_msgs in #print axioms MM.FLM810ASA.crossBracket_eq_crossIterate_of_nonneg_of_grounded
=== Definitions/MMFLM810NegCFaceClosed.lean
   92: /-- info: 'MM.FLM810NCFC.zLine_all' depends on axioms: [propext, Classical.choice, Quot.sound] -/
   93: #guard_msgs in
   96: /-- info: 'MM.FLM810NCFC.negCBinomMomentAligned_all' depends on axioms: [propext, Classical.choice, Quot.sound] -/
   97: #guard_msgs in
  100: /-- info: 'MM.FLM810NCFC.negCBinomMomentAlignedAt_all' depends on axioms: [propext, Classical.choice, Quot.sound] -/
  101: #guard_msgs in
  104: /-- info: 'MM.FLM810NCFC.negCFaceAligned_evenCocycle' depends on axioms: [propext, Classical.choice, Quot.sound] -/
  105: #guard_msgs in
