ComparatorChallenges/CoarseAssembly.lean

GitHub source file

Explanation legend Lean4 Domain Explanation Language (L4DEL)

L4DEL explanations are a separate layer. They do not change the Lean source. Intuition is explanatory prose; numbered items are a reading path; sources link the wording back to evidence.

L4DEL
Lean4 Domain Explanation Language

Credit: OpenAI's pinned repository says an unreleased internal model produced the manuscripts and supporting proof artifacts. The collection builds on the mathematics community's accumulated problems, results, language, and formal libraries; each manuscript's BibTeX and bibliography are the authority for individual scholarly credit.

Project sources: Pinned openai/math documentation, Pinned formalization catalogue

199 declarations, 1 contain sorry, 0 declared as axioms

A bounded-geometry counterexample to coarse Novikov

The concrete graph union has an infinite-order class killed by its ordinary reduced coarse assembly map, including after rationalization.

  1. def OAI.CoarseAssembly.blockLinear line 31

    Also declared: OAI/Topology/CoarseAssembly/Definitions.lean:31 (same declaration text).

  2. def OAI.CoarseAssembly.blockOperator line 40

    Also declared: OAI/Topology/CoarseAssembly/Definitions.lean:40 (same declaration text).

  3. def OAI.CoarseAssembly.blockIsometry line 63

    Also declared: OAI/Topology/CoarseAssembly/Definitions.lean:63 (same declaration text).

  4. def OAI.CoarseAssembly.flattenVector line 96

    Also declared: OAI/Topology/CoarseAssembly/Definitions.lean:96 (same declaration text).

  5. def OAI.CoarseAssembly.rowVector line 128

    Also declared: OAI/Topology/CoarseAssembly/Definitions.lean:128 (same declaration text).

  6. def OAI.CoarseAssembly.unflattenVector line 144

    Also declared: OAI/Topology/CoarseAssembly/Definitions.lean:144 (same declaration text).

  7. def OAI.CoarseAssembly.flattenEquiv line 168

    Also declared: OAI/Topology/CoarseAssembly/Definitions.lean:168 (same declaration text).

  8. def OAI.CoarseAssembly.operatorConjugation line 262

    Also declared: OAI/Topology/CoarseAssembly/Definitions.lean:262 (same declaration text).

  9. def OAI.CoarseAssembly.operatorConjugationHom line 265

    Also declared: OAI/Topology/CoarseAssembly/Definitions.lean:265 (same declaration text).

  10. abbrev OAI.CoarseAssembly.Congruence.ArithmeticGroup line 302

    Also declared: OAI/Topology/CoarseAssembly/Definitions.lean:302 (same declaration text).

  11. abbrev OAI.CoarseAssembly.Congruence.Quotient line 304

    Also declared: OAI/Topology/CoarseAssembly/Definitions.lean:304 (same declaration text).

  12. def OAI.CoarseAssembly.Congruence.reduce line 306

    Also declared: OAI/Topology/CoarseAssembly/Definitions.lean:306 (same declaration text).

  13. def OAI.CoarseAssembly.Congruence.diagonal line 309

    Also declared: OAI/Topology/CoarseAssembly/Definitions.lean:309 (same declaration text).

  14. def OAI.CoarseAssembly.Congruence.holonomy line 313

    Also declared: OAI/Topology/CoarseAssembly/Definitions.lean:313 (same declaration text).

  15. def OAI.CoarseAssembly.Congruence.residueMap line 324

    Also declared: OAI/Topology/CoarseAssembly/Definitions.lean:324 (same declaration text).

  16. def OAI.CoarseAssembly.Congruence.quotientMap line 327

    Also declared: OAI/Topology/CoarseAssembly/Definitions.lean:327 (same declaration text).

  17. def OAI.CoarseAssembly.flattenOperator line 345

    Also declared: OAI/Topology/CoarseAssembly/Definitions.lean:345 (same declaration text).

  18. def OAI.CoarseAssembly.discreteGraphMetric line 366

    Also declared: OAI/Topology/CoarseAssembly/Definitions.lean:366 (same declaration text).

  19. def OAI.CoarseAssembly.connectedGraphMetric line 381

    Also declared: OAI/Topology/CoarseAssembly/Definitions.lean:381 (same declaration text).

  20. def OAI.CoarseAssembly.graphMetricOrDiscrete line 393

    Also declared: OAI/Topology/CoarseAssembly/Definitions.lean:393 (same declaration text).

  21. def OAI.CoarseAssembly.separatedDist line 411

    Also declared: OAI/Topology/CoarseAssembly/Definitions.lean:411 (same declaration text).

  22. def OAI.CoarseAssembly.separatedMetric line 415

    Also declared: OAI/Topology/CoarseAssembly/Definitions.lean:415 (same declaration text).

  23. abbrev OAI.CoarseAssembly.DiscreteRoe.Module line 595

    Also declared: OAI/Topology/CoarseAssembly/Definitions.lean:595 (same declaration text).

  24. abbrev OAI.CoarseAssembly.DiscreteRoe.Operator line 597

    Also declared: OAI/Topology/CoarseAssembly/Definitions.lean:597 (same declaration text).

  25. def OAI.CoarseAssembly.DiscreteRoe.insert line 600

    Also declared: OAI/Topology/CoarseAssembly/Definitions.lean:600 (same declaration text).

  26. def OAI.CoarseAssembly.DiscreteRoe.coordinate line 603

    Also declared: OAI/Topology/CoarseAssembly/Definitions.lean:603 (same declaration text).

  27. def OAI.CoarseAssembly.DiscreteRoe.entry line 606

    Also declared: OAI/Topology/CoarseAssembly/Definitions.lean:606 (same declaration text).

  28. def OAI.CoarseAssembly.DiscreteRoe.CompactEntries line 609

    Also declared: OAI/Topology/CoarseAssembly/Definitions.lean:609 (same declaration text).

  29. def OAI.CoarseAssembly.DiscreteRoe.PropagationLE line 620

    Also declared: OAI/Topology/CoarseAssembly/Definitions.lean:620 (same declaration text).

  30. def OAI.CoarseAssembly.DiscreteRoe.Generator line 623

    Also declared: OAI/Topology/CoarseAssembly/Definitions.lean:623 (same declaration text).

  31. def OAI.CoarseAssembly.DiscreteRoe.algebra line 626

    Also declared: OAI/Topology/CoarseAssembly/Definitions.lean:626 (same declaration text).

  32. instance OAI.CoarseAssembly.DiscreteRoe.(instance at line 629) line 629
  33. def OAI.CoarseAssembly.DiscreteRoe.MapsToRoe line 664

    Also declared: OAI/Topology/CoarseAssembly/Definitions.lean:664 (same declaration text).

  34. def OAI.CoarseAssembly.DiscreteRoe.conjugationHom line 668

    Also declared: OAI/Topology/CoarseAssembly/Definitions.lean:668 (same declaration text).

  35. def OAI.CoarseAssembly.UniformFiniteBalls line 692

    Also declared: OAI/Topology/CoarseAssembly/Definitions.lean:692 (same declaration text).

  36. abbrev OAI.CoarseAssembly.LatticeVertex line 711

    Also declared: OAI/Topology/CoarseAssembly/Definitions.lean:711 (same declaration text).

  37. def OAI.CoarseAssembly.latticeRadius line 713

    Also declared: OAI/Topology/CoarseAssembly/Definitions.lean:713 (same declaration text).

  38. def OAI.CoarseAssembly.triangularGraph line 716

    Also declared: OAI/Topology/CoarseAssembly/Definitions.lean:716 (same declaration text).

  39. def OAI.CoarseAssembly.Disc line 722

    Also declared: OAI/Topology/CoarseAssembly/Definitions.lean:722 (same declaration text).

  40. instance OAI.CoarseAssembly.(instance at line 724) line 724
  41. def OAI.CoarseAssembly.discGraph line 737

    Also declared: OAI/Topology/CoarseAssembly/Definitions.lean:737 (same declaration text).

  42. def OAI.CoarseAssembly.discDepth line 742

    Also declared: OAI/Topology/CoarseAssembly/Definitions.lean:742 (same declaration text).

  43. def OAI.CoarseAssembly.latticeCharge line 752

    Also declared: OAI/Topology/CoarseAssembly/Definitions.lean:752 (same declaration text).

  44. def OAI.CoarseAssembly.Congruence.chosenHolonomyUnit line 786

    Also declared: OAI/Topology/CoarseAssembly/Definitions.lean:786 (same declaration text).

  45. def OAI.CoarseAssembly.symmetricMoves line 843

    Also declared: OAI/Topology/CoarseAssembly/Definitions.lean:843 (same declaration text).

  46. abbrev OAI.CoarseAssembly.FiberVertex line 846

    Also declared: OAI/Topology/CoarseAssembly/Definitions.lean:846 (same declaration text).

  47. instance OAI.CoarseAssembly.(instance at line 848) line 848
  48. def OAI.CoarseAssembly.fiberCoordinate line 850

    Also declared: OAI/Topology/CoarseAssembly/Definitions.lean:850 (same declaration text).

  49. def OAI.CoarseAssembly.fiberCharge line 853

    Also declared: OAI/Topology/CoarseAssembly/Definitions.lean:853 (same declaration text).

  50. def OAI.CoarseAssembly.LiftStep line 856

    Also declared: OAI/Topology/CoarseAssembly/Definitions.lean:856 (same declaration text).

  51. def OAI.CoarseAssembly.fiberedGraph line 864

    Also declared: OAI/Topology/CoarseAssembly/Definitions.lean:864 (same declaration text).

  52. def OAI.CoarseAssembly.discBoundaryBase line 921

    Also declared: OAI/Topology/CoarseAssembly/Definitions.lean:921 (same declaration text).

  53. def OAI.CoarseAssembly.fiberBoundaryBase line 926

    Also declared: OAI/Topology/CoarseAssembly/Definitions.lean:926 (same declaration text).

  54. abbrev OAI.CoarseAssembly.BaseUnion line 940

    Also declared: OAI/Topology/CoarseAssembly/Definitions.lean:940 (same declaration text).

  55. abbrev OAI.CoarseAssembly.BaseFiber line 942

    Also declared: OAI/Topology/CoarseAssembly/Definitions.lean:942 (same declaration text).

  56. abbrev OAI.CoarseAssembly.VertexUnion line 944

    Also declared: OAI/Topology/CoarseAssembly/Definitions.lean:944 (same declaration text).

  57. instance OAI.CoarseAssembly.baseUnionDecidableEq line 946

    Also declared: OAI/Topology/CoarseAssembly/Definitions.lean:946 (same declaration text).

  58. instance OAI.CoarseAssembly.vertexUnionDecidableEq line 948

    Also declared: OAI/Topology/CoarseAssembly/Definitions.lean:948 (same declaration text).

  59. def OAI.CoarseAssembly.componentMetric line 951

    Also declared: OAI/Topology/CoarseAssembly/Definitions.lean:951 (same declaration text).

  60. def OAI.CoarseAssembly.componentUnionMetric line 955

    Also declared: OAI/Topology/CoarseAssembly/Definitions.lean:955 (same declaration text).

  61. def OAI.CoarseAssembly.vertexUnionMetric line 960

    Also declared: OAI/Topology/CoarseAssembly/Definitions.lean:960 (same declaration text).

  62. def OAI.CoarseAssembly.positiveElementaryMove line 978

    Also declared: OAI/Topology/CoarseAssembly/Definitions.lean:978 (same declaration text).

  63. def OAI.CoarseAssembly.elementaryMoves line 981

    Also declared: OAI/Topology/CoarseAssembly/Definitions.lean:981 (same declaration text).

  64. abbrev OAI.CoarseAssembly.AmpleSpace line 985

    Also declared: OAI/Topology/CoarseAssembly/Definitions.lean:985 (same declaration text).

  65. structure OAI.CoarseAssembly.Analytic.HilbertSpace line 1000

    Also declared: OAI/Topology/CoarseAssembly/Definitions.lean:1000 (same declaration text).

  66. instance OAI.CoarseAssembly.Analytic.(instance at line 1010) line 1010
  67. abbrev OAI.CoarseAssembly.Analytic.End line 1012

    Also declared: OAI/Topology/CoarseAssembly/Definitions.lean:1012 (same declaration text).

  68. structure OAI.CoarseAssembly.Analytic.OddCycle line 1016

    Also declared: OAI/Topology/CoarseAssembly/Definitions.lean:1016 (same declaration text).

  69. def OAI.CoarseAssembly.Analytic.OddCycle.Degenerate line 1031

    Also declared: OAI/Topology/CoarseAssembly/Definitions.lean:1031 (same declaration text).

  70. def OAI.CoarseAssembly.Analytic.OddCycle.precomp line 1036

    Also declared: OAI/Topology/CoarseAssembly/Definitions.lean:1036 (same declaration text).

  71. structure OAI.CoarseAssembly.Analytic.OddCycle.UnitaryEquivalent line 1044

    Also declared: OAI/Topology/CoarseAssembly/Definitions.lean:1044 (same declaration text).

  72. def OAI.CoarseAssembly.Analytic.OddCycle.UnitaryEquivalent.precomp line 1050

    Also declared: OAI/Topology/CoarseAssembly/Definitions.lean:1050 (same declaration text).

  73. structure OAI.CoarseAssembly.Analytic.OddCycle.IsDirectSum line 1056

    Also declared: OAI/Topology/CoarseAssembly/Definitions.lean:1056 (same declaration text).

  74. def OAI.CoarseAssembly.Analytic.OddCycle.IsDirectSum.precomp line 1068

    Also declared: OAI/Topology/CoarseAssembly/Definitions.lean:1068 (same declaration text).

  75. abbrev OAI.CoarseAssembly.Analytic.Interval line 1079

    Also declared: OAI/Topology/CoarseAssembly/Definitions.lean:1079 (same declaration text).

  76. def OAI.CoarseAssembly.Analytic.start line 1081

    Also declared: OAI/Topology/CoarseAssembly/Definitions.lean:1081 (same declaration text).

  77. def OAI.CoarseAssembly.Analytic.finish line 1083

    Also declared: OAI/Topology/CoarseAssembly/Definitions.lean:1083 (same declaration text).

  78. structure OAI.CoarseAssembly.Analytic.OddHomotopy line 1085

    Also declared: OAI/Topology/CoarseAssembly/Definitions.lean:1085 (same declaration text).

  79. def OAI.CoarseAssembly.Analytic.OddHomotopy.eval line 1100

    Also declared: OAI/Topology/CoarseAssembly/Definitions.lean:1100 (same declaration text).

  80. def OAI.CoarseAssembly.Analytic.OddHomotopy.precomp line 1108

    Also declared: OAI/Topology/CoarseAssembly/Definitions.lean:1108 (same declaration text).

  81. inductive OAI.CoarseAssembly.Analytic.CycleRelation line 1135

    Also declared: OAI/Topology/CoarseAssembly/Definitions.lean:1135 (same declaration text).

  82. def OAI.CoarseAssembly.Analytic.relations line 1145

    Also declared: OAI/Topology/CoarseAssembly/Definitions.lean:1145 (same declaration text).

  83. abbrev OAI.CoarseAssembly.Analytic.OddK line 1148

    Also declared: OAI/Topology/CoarseAssembly/Definitions.lean:1148 (same declaration text).

  84. def OAI.CoarseAssembly.Analytic.cycleClass line 1150

    Also declared: OAI/Topology/CoarseAssembly/Definitions.lean:1150 (same declaration text).

  85. def OAI.CoarseAssembly.Analytic.precompFree line 1157

    Also declared: OAI/Topology/CoarseAssembly/Definitions.lean:1157 (same declaration text).

  86. def OAI.CoarseAssembly.Analytic.precomp line 1160

    Also declared: OAI/Topology/CoarseAssembly/Definitions.lean:1160 (same declaration text).

  87. def OAI.CoarseAssembly.Analytic.OddCycle.compactPerturb line 1242

    Also declared: OAI/Topology/CoarseAssembly/Definitions.lean:1242 (same declaration text).

  88. def OAI.CoarseAssembly.Analytic.OddCycle.localCompactPerturb line 1337

    Also declared: OAI/Topology/CoarseAssembly/Definitions.lean:1337 (same declaration text).

  89. def OAI.CoarseAssembly.Analytic.symmetricCutDown line 1408

    Also declared: OAI/Topology/CoarseAssembly/Definitions.lean:1408 (same declaration text).

  90. def OAI.CoarseAssembly.Analytic.OddCycle.scalarRestriction line 1424

    Also declared: OAI/Topology/CoarseAssembly/Definitions.lean:1424 (same declaration text).

  91. def OAI.CoarseAssembly.Analytic.representedCorrection line 1440

    Also declared: OAI/Topology/CoarseAssembly/Definitions.lean:1440 (same declaration text).

  92. def OAI.CoarseAssembly.Analytic.OddCycle.cutDown line 1443

    Also declared: OAI/Topology/CoarseAssembly/Definitions.lean:1443 (same declaration text).

  93. def OAI.CoarseAssembly.Analytic.completedRepresentation line 1605

    Also declared: OAI/Topology/CoarseAssembly/Definitions.lean:1605 (same declaration text).

  94. def OAI.CoarseAssembly.Analytic.OddCycle.characterExtension line 1661

    Also declared: OAI/Topology/CoarseAssembly/Definitions.lean:1661 (same declaration text).

  95. abbrev OAI.CoarseAssembly.Analytic.LocallyFiniteK1 line 1716

    Also declared: OAI/Topology/CoarseAssembly/Definitions.lean:1716 (same declaration text).

  96. def OAI.CoarseAssembly.Analytic.pullback line 1718

    Also declared: OAI/Topology/CoarseAssembly/Definitions.lean:1718 (same declaration text).

  97. def OAI.CoarseAssembly.Analytic.pushforward line 1722

    Also declared: OAI/Topology/CoarseAssembly/Definitions.lean:1722 (same declaration text).

  98. structure OAI.CoarseAssembly.Analytic.Coarsening line 1725

    Also declared: OAI/Topology/CoarseAssembly/Definitions.lean:1725 (same declaration text).

  99. def OAI.CoarseAssembly.Analytic.Coarsening.map line 1737

    Also declared: OAI/Topology/CoarseAssembly/Definitions.lean:1737 (same declaration text).

  100. abbrev OAI.CoarseAssembly.Analytic.Coarsening.Homology line 1741

    Also declared: OAI/Topology/CoarseAssembly/Definitions.lean:1741 (same declaration text).

  101. structure OAI.CoarseAssembly.Rips.Point line 1761

    Also declared: OAI/Topology/CoarseAssembly/Definitions.lean:1761 (same declaration text).

  102. def OAI.CoarseAssembly.Rips.coordinates line 1769

    Also declared: OAI/Topology/CoarseAssembly/Definitions.lean:1769 (same declaration text).

  103. instance OAI.CoarseAssembly.Rips.(instance at line 1771) line 1771
  104. instance OAI.CoarseAssembly.Rips.(instance at line 1774) line 1774
  105. def OAI.CoarseAssembly.Rips.coarsen line 1787

    Also declared: OAI/Topology/CoarseAssembly/Definitions.lean:1787 (same declaration text).

  106. def OAI.CoarseAssembly.Rips.inclusion line 1793

    Also declared: OAI/Topology/CoarseAssembly/Definitions.lean:1793 (same declaration text).

  107. def OAI.CoarseAssembly.Rips.coarsening line 1866

    Also declared: OAI/Topology/CoarseAssembly/Definitions.lean:1866 (same declaration text).

  108. abbrev OAI.CoarseAssembly.Rips.KX1 line 1897

    Also declared: OAI/Topology/CoarseAssembly/Definitions.lean:1897 (same declaration text).

  109. def OAI.CoarseAssembly.Rips.vertex line 1916

    Also declared: OAI/Topology/CoarseAssembly/Definitions.lean:1916 (same declaration text).

  110. instance OAI.CoarseAssembly.Rips.(instance at line 1945) line 1945
  111. def OAI.CoarseAssembly.Analytic.zeroExtension line 2062

    Also declared: OAI/Topology/CoarseAssembly/Definitions.lean:2062 (same declaration text).

  112. def OAI.CoarseAssembly.Analytic.zeroExtensionHom line 2085

    Also declared: OAI/Topology/CoarseAssembly/Definitions.lean:2085 (same declaration text).

  113. def OAI.CoarseAssembly.Analytic.cayleyDenominator line 2174

    Also declared: OAI/Topology/CoarseAssembly/Definitions.lean:2174 (same declaration text).

  114. def OAI.CoarseAssembly.Analytic.cayleyUnitary line 2192

    Also declared: OAI/Topology/CoarseAssembly/Definitions.lean:2192 (same declaration text).

  115. def OAI.CoarseAssembly.Analytic.rationalBoundaryUnitary line 2233

    Also declared: OAI/Topology/CoarseAssembly/Definitions.lean:2233 (same declaration text).

  116. def OAI.CoarseAssembly.Analytic.boundedTransform line 2251

    Also declared: OAI/Topology/CoarseAssembly/Definitions.lean:2251 (same declaration text).

  117. def OAI.CoarseAssembly.Analytic.OddCycle.bounded line 2276

    Also declared: OAI/Topology/CoarseAssembly/Definitions.lean:2276 (same declaration text).

  118. def OAI.CoarseAssembly.Analytic.OddCycle.unitalSelfAdjoint line 2482

    Also declared: OAI/Topology/CoarseAssembly/Definitions.lean:2482 (same declaration text).

  119. def OAI.CoarseAssembly.Analytic.OddCycle.regularize line 2597

    Also declared: OAI/Topology/CoarseAssembly/Definitions.lean:2597 (same declaration text).

  120. def OAI.CoarseAssembly.Rips.sqrtCoordinate line 2734

    Also declared: OAI/Topology/CoarseAssembly/Definitions.lean:2734 (same declaration text).

  121. def OAI.CoarseAssembly.DiscreteRoe.partitionMap line 2766

    Also declared: OAI/Topology/CoarseAssembly/Definitions.lean:2766 (same declaration text).

  122. def OAI.CoarseAssembly.DiscreteRoe.partitionIsometry line 2769

    Also declared: OAI/Topology/CoarseAssembly/Definitions.lean:2769 (same declaration text).

  123. def OAI.CoarseAssembly.DiscreteRoe.constantBlock line 2823

    Also declared: OAI/Topology/CoarseAssembly/Definitions.lean:2823 (same declaration text).

  124. def OAI.CoarseAssembly.DiscreteRoe.partitionCompression line 2826

    Also declared: OAI/Topology/CoarseAssembly/Definitions.lean:2826 (same declaration text).

  125. def OAI.CoarseAssembly.isometricExtension line 2845

    Also declared: OAI/Topology/CoarseAssembly/Definitions.lean:2845 (same declaration text).

  126. def OAI.CoarseAssembly.DiscreteRoe.algebraicRoe line 2874

    Also declared: OAI/Topology/CoarseAssembly/Definitions.lean:2874 (same declaration text).

  127. def OAI.CoarseAssembly.DiscreteRoe.RoeMultiplier line 3154

    Also declared: OAI/Topology/CoarseAssembly/Definitions.lean:3154 (same declaration text).

  128. def OAI.CoarseAssembly.DiscreteRoe.roeIdealizer line 3158

    Also declared: OAI/Topology/CoarseAssembly/Definitions.lean:3158 (same declaration text).

  129. def OAI.CoarseAssembly.DiscreteRoe.localizedSpatialOperator line 3204

    Also declared: OAI/Topology/CoarseAssembly/Definitions.lean:3204 (same declaration text).

  130. def OAI.CoarseAssembly.Rips.representedSqrt line 3225

    Also declared: OAI/Topology/CoarseAssembly/Definitions.lean:3225 (same declaration text).

  131. def OAI.CoarseAssembly.Rips.ripsSpatialOperator line 3228

    Also declared: OAI/Topology/CoarseAssembly/Definitions.lean:3228 (same declaration text).

  132. def OAI.CoarseAssembly.extendedFunction line 3294

    Also declared: OAI/Topology/CoarseAssembly/Definitions.lean:3294 (same declaration text).

  133. def OAI.CoarseAssembly.inclusionVector line 3297

    Also declared: OAI/Topology/CoarseAssembly/Definitions.lean:3297 (same declaration text).

  134. def OAI.CoarseAssembly.inclusionIsometry line 3340

    Also declared: OAI/Topology/CoarseAssembly/Definitions.lean:3340 (same declaration text).

  135. def OAI.CoarseAssembly.Analytic.ampleIsometry line 3430

    Also declared: OAI/Topology/CoarseAssembly/Definitions.lean:3430 (same declaration text).

  136. def OAI.CoarseAssembly.DiscreteRoe.coefficientIsometry line 3478

    Also declared: OAI/Topology/CoarseAssembly/Definitions.lean:3478 (same declaration text).

  137. def OAI.CoarseAssembly.DiscreteRoe.coefficientExtension line 3483

    Also declared: OAI/Topology/CoarseAssembly/Definitions.lean:3483 (same declaration text).

  138. def OAI.CoarseAssembly.DiscreteRoe.diagonalFamily line 3502

    Also declared: OAI/Topology/CoarseAssembly/Definitions.lean:3502 (same declaration text).

  139. def OAI.CoarseAssembly.Rips.mapPoint line 3526

    Also declared: OAI/Topology/CoarseAssembly/Definitions.lean:3526 (same declaration text).

  140. def OAI.CoarseAssembly.Rips.unmapPoint line 3542

    Also declared: OAI/Topology/CoarseAssembly/Definitions.lean:3542 (same declaration text).

  141. def OAI.CoarseAssembly.separatedComponent line 3571

    Also declared: OAI/Topology/CoarseAssembly/Definitions.lean:3571 (same declaration text).

  142. abbrev OAI.CoarseAssembly.TopologicalK1.InvertibleMatrix line 3590

    Also declared: OAI/Topology/CoarseAssembly/Definitions.lean:3590 (same declaration text).

  143. abbrev OAI.CoarseAssembly.TopologicalK1.StableGL line 3592

    Also declared: OAI/Topology/CoarseAssembly/Definitions.lean:3592 (same declaration text).

  144. def OAI.CoarseAssembly.TopologicalK1.IsStabilization line 3594

    Also declared: OAI/Topology/CoarseAssembly/Definitions.lean:3594 (same declaration text).

  145. inductive OAI.CoarseAssembly.TopologicalK1.Relation line 3599

    Also declared: OAI/Topology/CoarseAssembly/Definitions.lean:3599 (same declaration text).

  146. def OAI.CoarseAssembly.TopologicalK1.relations line 3608

    Also declared: OAI/Topology/CoarseAssembly/Definitions.lean:3608 (same declaration text).

  147. abbrev OAI.CoarseAssembly.TopologicalK1.Group line 3611

    Also declared: OAI/Topology/CoarseAssembly/Definitions.lean:3611 (same declaration text).

  148. def OAI.CoarseAssembly.TopologicalK1.matrixClass line 3613

    Also declared: OAI/Topology/CoarseAssembly/Definitions.lean:3613 (same declaration text).

  149. def OAI.CoarseAssembly.TopologicalK1.mapGL line 3620

    Also declared: OAI/Topology/CoarseAssembly/Definitions.lean:3620 (same declaration text).

  150. def OAI.CoarseAssembly.TopologicalK1.mapFree line 3623

    Also declared: OAI/Topology/CoarseAssembly/Definitions.lean:3623 (same declaration text).

  151. def OAI.CoarseAssembly.TopologicalK1.map line 3626

    Also declared: OAI/Topology/CoarseAssembly/Definitions.lean:3626 (same declaration text).

  152. def OAI.CoarseAssembly.OperatorKTheory.scalarMap line 3742

    Also declared: OAI/Topology/CoarseAssembly/Definitions.lean:3742 (same declaration text).

  153. abbrev OAI.CoarseAssembly.OperatorKTheory.K1 line 3745

    Also declared: OAI/Topology/CoarseAssembly/Definitions.lean:3745 (same declaration text).

  154. def OAI.CoarseAssembly.OperatorKTheory.unitizationMap line 3751

    Also declared: OAI/Topology/CoarseAssembly/Definitions.lean:3751 (same declaration text).

  155. def OAI.CoarseAssembly.OperatorKTheory.map line 3755

    Also declared: OAI/Topology/CoarseAssembly/Definitions.lean:3755 (same declaration text).

  156. def OAI.CoarseAssembly.OperatorKTheory.relativePart line 3801

    Also declared: OAI/Topology/CoarseAssembly/Definitions.lean:3801 (same declaration text).

  157. def OAI.CoarseAssembly.OperatorKTheory.relativeUnitary line 3803

    Also declared: OAI/Topology/CoarseAssembly/Definitions.lean:3803 (same declaration text).

  158. def OAI.CoarseAssembly.OperatorKTheory.relativeMatrix line 3842

    Also declared: OAI/Topology/CoarseAssembly/Definitions.lean:3842 (same declaration text).

  159. def OAI.CoarseAssembly.OperatorKTheory.relativeClass line 3848

    Also declared: OAI/Topology/CoarseAssembly/Definitions.lean:3848 (same declaration text).

  160. def OAI.CoarseAssembly.DiscreteRoe.multiplierAlgebra line 3914

    Also declared: OAI/Topology/CoarseAssembly/Definitions.lean:3914 (same declaration text).

  161. instance OAI.CoarseAssembly.DiscreteRoe.(instance at line 3935) line 3935
  162. def OAI.CoarseAssembly.DiscreteRoe.multiplierRoeIdeal line 3965

    Also declared: OAI/Topology/CoarseAssembly/Definitions.lean:3965 (same declaration text).

  163. def OAI.CoarseAssembly.DiscreteRoe.multiplierBoundaryUnitary line 3973

    Also declared: OAI/Topology/CoarseAssembly/Definitions.lean:3973 (same declaration text).

  164. def OAI.CoarseAssembly.DiscreteRoe.multiplierBoundaryClass line 3978

    Also declared: OAI/Topology/CoarseAssembly/Definitions.lean:3978 (same declaration text).

  165. def OAI.CoarseAssembly.DiscreteRoe.separatedFamilyMultiplier line 4108

    Also declared: OAI/Topology/CoarseAssembly/Definitions.lean:4108 (same declaration text).

  166. def OAI.CoarseAssembly.DiscreteRoe.separatedFamilyBoundary line 4460

    Source comment

    The self-contained construction includes its support proofs.

    Also declared: OAI/Topology/CoarseAssembly/Definitions.lean:4460 (same declaration text).

    def separatedFamilyBoundary (hself : ∀ i, IsSelfAdjoint (A i))
    (hsq : ∀ i, IsCompactOperator ((A i * A i - (1 : OAI.CoarseAssembly.DiscreteRoe.Operator (V i) H)).toFun)) :
    letI := OAI.CoarseAssembly.separatedMetric o
…

    Mentions: OAI.CoarseAssembly.DiscreteRoe.Operator, OAI.CoarseAssembly.separatedMetric

  167. def OAI.CoarseAssembly.DiscreteRoe.partitionConjugate line 4878

    Also declared: OAI/Topology/CoarseAssembly/Definitions.lean:4878 (same declaration text).

  168. def OAI.CoarseAssembly.Analytic.localizedOperator line 4919

    Also declared: OAI/Topology/CoarseAssembly/Definitions.lean:4919 (same declaration text).

  169. def OAI.CoarseAssembly.Analytic.localizedCycle line 4922

    Also declared: OAI/Topology/CoarseAssembly/Definitions.lean:4922 (same declaration text).

  170. def OAI.CoarseAssembly.Rips.ampleRipsOperator line 4987

    Also declared: OAI/Topology/CoarseAssembly/Definitions.lean:4987 (same declaration text).

  171. def OAI.CoarseAssembly.Rips.ampleRipsFamilyBoundary line 4995

    Source comment

    The self-contained construction includes its support proofs.

    Also declared: OAI/Topology/CoarseAssembly/Definitions.lean:4995 (same declaration text).

    def ampleRipsFamilyBoundary (o : ∀ i, V i) (r : ℝ) (hr : 0 ≤ r)
    (c : ∀ i, OAI.CoarseAssembly.Analytic.OddCycle C(OAI.CoarseAssembly.Rips.Point (V i) r, ℂ)) (hπ : ∀ i, (c i).representation 1 = 1)
    (hF : ∀ i, IsSelfAdjoint (c i).operator)
    (C : ℝ) (hC : 0 ≤ C) (hnorm : ∀ i, ‖(c i).operator‖ ≤ C) :
    letI := OAI.CoarseAssembly.separatedMetric o
…

    Mentions: OAI.CoarseAssembly.Analytic.OddCycle, OAI.CoarseAssembly.Rips.Point, OAI.CoarseAssembly.separatedMetric

  172. def OAI.CoarseAssembly.DiscreteRoe.inclusionHom line 5312

    Source comment

    The self-contained construction includes its support proofs.

    Also declared: OAI/Topology/CoarseAssembly/Definitions.lean:5312 (same declaration text).

    def inclusionHom (e : X ↪ Y) (he : ∀ x y, dist (e x) (e y) ≤ dist x y) :
    OAI.CoarseAssembly.DiscreteRoe.algebra (X := X) (H := H) →⋆ₙₐ[ℂ] OAI.CoarseAssembly.DiscreteRoe.algebra (X := Y) (H := H) := by
…

    Mentions: OAI.CoarseAssembly.DiscreteRoe.algebra

  173. structure OAI.CoarseAssembly.Rips.ControlledCycleFamily line 5456

    Also declared: OAI/Topology/CoarseAssembly/Definitions.lean:5456 (same declaration text).

  174. def OAI.CoarseAssembly.Rips.ControlledCycleFamily.boundary line 5466

    Also declared: OAI/Topology/CoarseAssembly/Definitions.lean:5466 (same declaration text).

  175. def OAI.CoarseAssembly.Rips.regularizedFamily line 5491

    Also declared: OAI/Topology/CoarseAssembly/Definitions.lean:5491 (same declaration text).

  176. def OAI.CoarseAssembly.Rips.analyticFamilyIndexFree line 5762

    Also declared: OAI/Topology/CoarseAssembly/Definitions.lean:5762 (same declaration text).

  177. def OAI.CoarseAssembly.Rips.analyticFamilyIndex line 5772

    Also declared: OAI/Topology/CoarseAssembly/Definitions.lean:5772 (same declaration text).

  178. def OAI.CoarseAssembly.separatedRipsMap line 5803

    Also declared: OAI/Topology/CoarseAssembly/Definitions.lean:5803 (same declaration text).

  179. def OAI.CoarseAssembly.separatedRipsEmbedding line 5845

    Also declared: OAI/Topology/CoarseAssembly/Definitions.lean:5845 (same declaration text).

  180. def OAI.CoarseAssembly.Analytic.compactFunctionLift line 5901

    Also declared: OAI/Topology/CoarseAssembly/Definitions.lean:5901 (same declaration text).

  181. def OAI.CoarseAssembly.Rips.lateRipsFunctionHom line 5928

    Also declared: OAI/Topology/CoarseAssembly/Definitions.lean:5928 (same declaration text).

  182. def OAI.CoarseAssembly.Rips.ripsPointCharacter line 6093

    Also declared: OAI/Topology/CoarseAssembly/Definitions.lean:6093 (same declaration text).

  183. def OAI.CoarseAssembly.Rips.separatedRipsIndex line 6097

    Also declared: OAI/Topology/CoarseAssembly/Definitions.lean:6097 (same declaration text).

  184. structure OAI.CoarseAssembly.Analytic.CoarseningMorphism line 6180

    Also declared: OAI/Topology/CoarseAssembly/Definitions.lean:6180 (same declaration text).

  185. structure OAI.CoarseAssembly.Analytic.CompatibleIndexFamily line 6186

    Also declared: OAI/Topology/CoarseAssembly/Definitions.lean:6186 (same declaration text).

  186. def OAI.CoarseAssembly.Analytic.CompatibleIndexFamily.assembly line 6197

    Also declared: OAI/Topology/CoarseAssembly/Definitions.lean:6197 (same declaration text).

  187. def OAI.CoarseAssembly.Rips.separatedIndexFamily line 6219

    Also declared: OAI/Topology/CoarseAssembly/Definitions.lean:6219 (same declaration text).

  188. def OAI.CoarseAssembly.Analytic.CompatibleIndexFamily.transport line 6249

    Also declared: OAI/Topology/CoarseAssembly/Definitions.lean:6249 (same declaration text).

  189. def OAI.CoarseAssembly.Rips.embeddingMap line 6313

    Also declared: OAI/Topology/CoarseAssembly/Definitions.lean:6313 (same declaration text).

  190. def OAI.CoarseAssembly.Rips.embeddingCoarsening line 6452

    Also declared: OAI/Topology/CoarseAssembly/Definitions.lean:6452 (same declaration text).

  191. def OAI.CoarseAssembly.TotalRoe line 6489

    Also declared: OAI/Topology/CoarseAssembly/Definitions.lean:6489 (same declaration text).

  192. instance OAI.CoarseAssembly.(instance at line 6491) line 6491
  193. abbrev OAI.CoarseAssembly.FiberedUnion line 6510

    Also declared: OAI/Topology/CoarseAssembly/Definitions.lean:6510 (same declaration text).

  194. def OAI.CoarseAssembly.totalToFiber line 6533

    Also declared: OAI/Topology/CoarseAssembly/Definitions.lean:6533 (same declaration text).

  195. def OAI.CoarseAssembly.totalToFiberCoarsening line 6536

    Also declared: OAI/Topology/CoarseAssembly/Definitions.lean:6536 (same declaration text).

  196. def OAI.CoarseAssembly.fiberReindexRoeHom line 6569

    Also declared: OAI/Topology/CoarseAssembly/Definitions.lean:6569 (same declaration text).

  197. def OAI.CoarseAssembly.constructedTotalIndex line 6591

    Also declared: OAI/Topology/CoarseAssembly/Definitions.lean:6591 (same declaration text).

  198. def OAI.CoarseAssembly.constructedCoarseAssembly line 6610

    Also declared: OAI/Topology/CoarseAssembly/Definitions.lean:6610 (same declaration text).

  199. theorem OAI.CoarseAssembly.bounded_geometry_graph_counterexample_unconditional Challenge statement: Failure of rational injectivity for maximal coarse assembly sorry line 6629

    L4DEL explanation

    The coarse Novikov conjecture predicts rational injectivity of the ordinary coarse assembly map for uniformly discrete spaces of bounded geometry. The formalization constructs a counterexample from a coarse disjoint union of finite connected graphs with uniformly bounded degree. Its degree-one coarse $K$-homology contains an infinite-order class whose image under ordinary coarse assembly into the reduced locally compact Roe algebra vanishes. The class remains nonzero after tensoring with $\mathbb Q$, so rational injectivity fails.

    1. This is an exact comparator target linked by the pinned repository's formalization note for this result.
    2. The repository's comparator configuration selects OAI.Topology.CoarseAssembly as the released solution module checked against this declaration.

    Sources and attribution: Pinned Lean source (fd4aeeb2ee4f)

    Distinct definitions of this name: OAI/Topology/CoarseAssembly/UnconditionalConclusion.lean:38 (same statement text; different proof or body). Qualify references as OAI.CoarseAssembly.bounded_geometry_graph_counterexample_unconditional@path.

    theorem bounded_geometry_graph_counterexample_unconditional :
    (∀ j, Finite (FiberVertex j) ∧
      (fiberedGraph elementaryMoves chosenHolonomyUnit j).Connected) ∧
    (∃ D : ℕ, ∀ j (x : FiberVertex j),
      Nat.card {y // (fiberedGraph elementaryMoves chosenHolonomyUnit j).Adj x y} ≤ D) ∧
    ProperSpace VertexUnion ∧ UniformFiniteBalls VertexUnion ∧
      (∀ x y : VertexUnion, x ≠ y → 1 ≤ dist x y) ∧
      ∃ α : KX1 VertexUnion,
        (∀ n : ℤ, n ≠ 0 → n • α ≠ 0) ∧ constructedCoarseAssembly α = 0 ∧
        (1 : ℚ) ⊗ₜ[ℤ] α ≠ 0 ∧
        ¬ Function.Injective constructedCoarseAssembly ∧
        ¬ Function.Injective (constructedCoarseAssembly.toIntLinearMap.lTensor ℚ) := by
…

    Mentions: OAI.CoarseAssembly.FiberVertex, OAI.CoarseAssembly.fiberedGraph, OAI.CoarseAssembly.elementaryMoves, OAI.CoarseAssembly.VertexUnion, OAI.CoarseAssembly.UniformFiniteBalls, OAI.CoarseAssembly.constructedCoarseAssembly