Main.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.LittleFinitistic.Main.algebra_finite line 12
Source documentation
The fixed algebra and every actual witness are finite dimensional over ℂ.
```
theorem algebra_finite : FiniteDimensional ℂ A := inferInstance
```
theorem OAI.LittleFinitistic.Main.test_finite line 14
theorem OAI.LittleFinitistic.Main.projective_dimension_bounds line 19
Source documentation
For the one fixed finite-dimensional complex algebra constructed in the manuscript, every positive m has the actual finite module N_m with the stated finite projective-dimension bounds.
```
theorem projective_dimension_bounds (m : ℕ) [NeZero m] :
    ((2*m-2 : ℕ) : WithBot ℕ∞) ≤ projectiveDimension (testModule m) ∧
      projectiveDimension (testModule m) < ⊤ := by
…
```
theorem OAI.LittleFinitistic.Main.infinite_littleFinitisticDimension line 27
Source documentation
The actual constructed algebra has infinite little finitistic dimension.
```
theorem infinite_littleFinitisticDimension : littleFinitisticDimension A = ⊤ := by
…
```

theorem OAI.LittleFinitistic.Main.counterexample line 36

Source documentation

Main theorem, with finite dimensionality of the one fixed A explicit and with actual finitely generated witness modules for every positive m.

theorem counterexample : FiniteDimensional ℂ A ∧ littleFinitisticDimension A = ⊤ ∧
    ∀ m : ℕ, 0 < m → ∃ N : ModuleCat.{0} A, Module.Finite A N ∧
      ((2*m-2 : ℕ) : WithBot ℕ∞) ≤ projectiveDimension N ∧ projectiveDimension N < ⊤ := by
…

theorem OAI.LittleFinitistic.Main.exists_counterexample line 44
Distinct definitions of this name: ComparatorChallenges/LittleFinitistic.lean:23 (same statement text; different proof or body). Qualify references as OAI.LittleFinitistic.Main.exists_counterexample@path.