OAI/NumberTheory/Jacobsthal/Paths/RawBoxRationalWitness.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos970.NumberTheoryLean.RecentCountWitness.recent_count_witness line 17
  2. theorem OAI.Erdos970.NumberTheoryLean.CountWitnessReadout.selected_edge_singleton line 84
  3. theorem OAI.Erdos970.NumberTheoryLean.CountWitnessReadout.observed_node_bad_edge line 95
  4. theorem OAI.Erdos970.NumberTheoryLean.GeometricRecentWitness.geometric_recent_witness line 124
  5. theorem OAI.Erdos970.NumberTheoryLean.StructuredWitnessOutside.full_selection_coordinates line 180
  6. theorem OAI.Erdos970.NumberTheoryLean.StructuredWitnessOutside.structured_full_selection line 191
  7. def OAI.Erdos970.NumberTheoryLean.RawBoxRationalWitness.rawBoxList line 222
  8. theorem OAI.Erdos970.NumberTheoryLean.RawBoxRationalWitness.raw_box_list_card line 226
  9. theorem OAI.Erdos970.NumberTheoryLean.RawBoxRationalWitness.raw_box_witness line 235