OAI/RingTheory/DirectFiniteness/CandidateRelations.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.KaplanskyCounterexample.FiniteGeometry.GenericStep line 13
  2. structure OAI.KaplanskyCounterexample.FiniteGeometry.ExceptionalStep line 19
  3. abbrev OAI.KaplanskyCounterexample.FiniteGeometry.PolygonStep line 24
  4. def OAI.KaplanskyCounterexample.FiniteGeometry.PolygonStep.label line 28
  5. def OAI.KaplanskyCounterexample.FiniteGeometry.PolygonStep.bundle line 32
  6. def OAI.KaplanskyCounterexample.FiniteGeometry.PolygonStep.wcoord line 36
  7. def OAI.KaplanskyCounterexample.FiniteGeometry.PolygonStep.ecoord line 40
  8. def OAI.KaplanskyCounterexample.FiniteGeometry.PolygonStep.vector line 44
  9. lemma OAI.KaplanskyCounterexample.FiniteGeometry.PolygonStep.ecoord_nonzero line 49
  10. lemma OAI.KaplanskyCounterexample.FiniteGeometry.PolygonStep.vector_ne_zero line 55
  11. def OAI.KaplanskyCounterexample.FiniteGeometry.PolygonStep.blockLabel line 66
  12. def OAI.KaplanskyCounterexample.FiniteGeometry.PolygonStep.blockVector line 72
  13. lemma OAI.KaplanskyCounterexample.FiniteGeometry.PolygonStep.blockVector_mem line 78
  14. lemma OAI.KaplanskyCounterexample.FiniteGeometry.PolygonStep.sum_blocks line 89
  15. lemma OAI.KaplanskyCounterexample.FiniteGeometry.PolygonStep.filter_blocks_E line 94
  16. lemma OAI.KaplanskyCounterexample.FiniteGeometry.PolygonStep.filter_blocks_W line 104
  17. lemma OAI.KaplanskyCounterexample.FiniteGeometry.DirectionFrame.polygon_component_sums line 121
  18. lemma OAI.KaplanskyCounterexample.FiniteGeometry.DirectionFrame.generic_occurs_twice line 152

    Source documentation

    Every occurring generic label occurs precisely twice in a candidate with at most five steps. No exceptional-vector cancellation has been assumed.

    lemma generic_occurs_twice {k : ℕ} (s : Fin k → PolygonStep Q R E) (hk : k ≤ 5)
    (hz : ∑ i, (s i).vector F = 0)
    (hadj : ∀ i, (s i).label ≠ (s (finRotate k i)).label)
    (j : R × Q) (hj : ∃ i, (s i).label = .inl j) :
    (Finset.univ.filter (fun i => (s i).label = .inl j)).card = 2 := by
…

    Mentions: OAI.KaplanskyCounterexample.FiniteGeometry.PolygonStep