UnconditionalConclusion.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

The unconditional bounded-geometry counterexample

The geometric construction, analytic assembly, integral spectral certificate and finite congruence generation are combined here.

theorem OAI.CoarseAssembly.provedKazhdanInput line 21

theorem OAI.CoarseAssembly.bounded_geometry_counterexample_unconditional line 26

Source documentation

The constructed ordinary coarse assembly map has an infinite-order kernel class and fails injectivity both integrally and rationally.

theorem bounded_geometry_counterexample_unconditional :
    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 ℚ) :=
…

Mentions: OAI.CoarseAssembly.VertexUnion, OAI.CoarseAssembly.UniformFiniteBalls, OAI.CoarseAssembly.constructedCoarseAssembly

theorem OAI.CoarseAssembly.bounded_geometry_graph_counterexample_unconditional line 38

Source documentation

The graph-family clauses of the main theorem, together with the full coarse-assembly conclusion for its concrete separated union.

Distinct definitions of this name: ComparatorChallenges/CoarseAssembly.lean:6629 (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