OAI/RingTheory/DirectFiniteness/PrescribedSearch.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.KaplanskyCounterexample.Prescription.Affine line 9
  2. abbrev OAI.KaplanskyCounterexample.Prescription.Pair line 10
  3. def OAI.KaplanskyCounterexample.Prescription.pairOrder line 15

    Source documentation

    Coordinate-lex order, then indicator order for points and lines, then indicator order for families, finally lexicographic order of the pair. Discarding the non-full-line candidates does not change relative order.

    @[instance_reducible] def pairOrder (h : Input) : LinearOrder (Pair h) :=
…

    Mentions: OAI.KaplanskyCounterexample.Prescription.Input, OAI.KaplanskyCounterexample.Prescription.Pair

  4. def OAI.KaplanskyCounterexample.Prescription.Test line 21
  5. def OAI.KaplanskyCounterexample.Prescription.Succeeds line 24
  6. lemma OAI.KaplanskyCounterexample.Prescription.succeeds217 line 26
  7. def OAI.KaplanskyCounterexample.Prescription.selectedH line 41

    Source documentation

    The exact least successful outer input, not the convenient existence bound 217.

    def selectedH : ℕ := Nat.find (show ∃ h, Succeeds h from ⟨217,succeeds217⟩)

    Mentions: OAI.KaplanskyCounterexample.Prescription.Succeeds, OAI.KaplanskyCounterexample.Prescription.succeeds217

  8. lemma OAI.KaplanskyCounterexample.Prescription.selectedH_spec line 42
  9. lemma OAI.KaplanskyCounterexample.Prescription.selectedH_le line 43
  10. lemma OAI.KaplanskyCounterexample.Prescription.selectedH_ge line 44
  11. lemma OAI.KaplanskyCounterexample.Prescription.selectedH_le217 line 45
  12. def OAI.KaplanskyCounterexample.Prescription.selectedInput line 47
  13. lemma OAI.KaplanskyCounterexample.Prescription.selectedInput_success line 48
  14. def OAI.KaplanskyCounterexample.Prescription.selectedPair line 51

    Source documentation

    The first successful pair in the literal finite lexicographic search.

    def selectedPair : Pair selectedInput :=
…

    Mentions: OAI.KaplanskyCounterexample.Prescription.Pair, OAI.KaplanskyCounterexample.Prescription.selectedInput

  15. lemma OAI.KaplanskyCounterexample.Prescription.selectedPair_spec line 55
  16. lemma OAI.KaplanskyCounterexample.Prescription.selectedPair_minimal line 58
  17. theorem OAI.KaplanskyCounterexample.Prescription.finite_search_terminates line 64

    Source documentation

    Formal termination certificate for both the outer loop and its finite inner loop.

    theorem finite_search_terminates :
    2 ≤ selectedH ∧ selectedH ≤ 217 ∧ Test selectedInput selectedPair ∧
      (∀ h, Succeeds h → selectedH ≤ h) ∧
      (∀ p, Test selectedInput p → @LE.le _ (pairOrder selectedInput).toLE selectedPair p) :=
…

    Mentions: OAI.KaplanskyCounterexample.Prescription.selectedH, OAI.KaplanskyCounterexample.Prescription.Test, OAI.KaplanskyCounterexample.Prescription.selectedInput, OAI.KaplanskyCounterexample.Prescription.selectedPair, OAI.KaplanskyCounterexample.Prescription.Succeeds, OAI.KaplanskyCounterexample.Prescription.pairOrder