OAI/Topology/CoarseAssembly/BoundaryConclusion.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

The boundary class in the reduced coarse assembly kernel

The filling and detector refer to the same explicitly parametrized family. Those maps combine with the two stated published assembly naturality equations.

  1. def OAI.CoarseAssembly.counterexampleClass line 32
  2. theorem OAI.CoarseAssembly.boundaryLoopClass_base_zero line 36
  3. theorem OAI.CoarseAssembly.counterexampleClass_image line 45
  4. theorem OAI.CoarseAssembly.counterexampleClass_infinite_order line 68
  5. theorem OAI.CoarseAssembly.counterexampleClass_index_zero line 76
  6. theorem OAI.CoarseAssembly.bounded_geometry_counterexample line 86

    Source documentation

    The manuscript's bounded-geometry rational counterexample, conditional only on the precisely cited published analytic inputs.

    theorem bounded_geometry_counterexample (circle : PublishedCircleInput)
    (hadd : CountableAdditivityInput CircleFamily)
    (homotopy : PublishedCompactHomotopyInput) (hfill : CountableAdditivityInput FilledDisc)
    (index : PublishedBoundaryAssemblyInput) (hgap : PublishedKazhdanInput) :
    ProperSpace VertexUnion ∧ UniformFiniteBalls VertexUnion ∧
      (∀ x y : VertexUnion, x ≠ y → 1 ≤ dist x y) ∧
      ∃ α : KX1 VertexUnion,
        (∀ n : ℤ, n ≠ 0 → n • α ≠ 0) ∧ index.total.assembly α = 0 ∧
        (1 : ℚ) ⊗ₜ[ℤ] α ≠ 0 ∧
        ¬ Function.Injective index.total.assembly ∧
        ¬ Function.Injective (index.total.assembly.toIntLinearMap.lTensor ℚ) := by
…

    Mentions: OAI.CoarseAssembly.PublishedCircleInput, OAI.CoarseAssembly.CircleFamily, OAI.CoarseAssembly.FilledDisc, OAI.CoarseAssembly.PublishedBoundaryAssemblyInput, OAI.CoarseAssembly.PublishedKazhdanInput, OAI.CoarseAssembly.VertexUnion, OAI.CoarseAssembly.UniformFiniteBalls