PublishedInputReduction.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Discharging the compact-homotopy input

The conditional theorem is preserved. This specialization removes its homotopy hypothesis using the proved Fredholm-cycle homotopy construction. The odd coefficient group of a point is now proved by explicit Fredholm normalization; the circle, additivity, index and Kazhdan inputs remain.

theorem OAI.CoarseAssembly.compactFillingInput line 21
theorem OAI.CoarseAssembly.bounded_geometry_counterexample_of_point_odd_zero line 31
theorem OAI.CoarseAssembly.provedCompactFillingInput line 45
Source documentation
The complete compact-filling input is now a theorem.
```
theorem provedCompactFillingInput : PublishedCompactHomotopyInput :=
…
```

theorem OAI.CoarseAssembly.bounded_geometry_counterexample_from_circle_index_gap line 49

Source documentation

Main theorem after discharging compact homotopy invariance and the odd point coefficient.

theorem bounded_geometry_counterexample_from_circle_index_gap (circle : PublishedCircleInput)
    (hadd : CountableAdditivityInput CircleFamily) (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 ℚ) :=
…

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