OAI/Combinatorics/EditApproximation/Refinement/PhysicalQueryProgress.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

The dependency split for keys actually emitted by the adaptive local queries. Current-index edges descend in the physical tree; older reads decrease the table rank and never move to an ancestor.

  1. def OAI.EditApproximation.PhysicalTableRequest.DependencyProgress line 14
  2. theorem OAI.EditApproximation.PhysicalTableRequest.warmup_before_refinement_progress line 19
  3. theorem OAI.EditApproximation.PhysicalTableRequest.refinement_child_same_progress line 29
  4. theorem OAI.EditApproximation.PhysicalTableRequest.refinement_child_earlier_progress line 40
  5. theorem OAI.EditApproximation.PhysicalTableRequest.previous_pass_dependencyProgress line 48
  6. theorem OAI.EditApproximation.PhysicalTableRequest.rank_lt_iff_index_lt_of_pass line 54
  7. theorem OAI.EditApproximation.PhysicalTableRequest.rank_not_lt_iff_index_eq_of_pass line 61
  8. theorem OAI.EditApproximation.physicalRefinementWarmupRead_keys_progress line 70
  9. theorem OAI.EditApproximation.physicalRefinementDataRequest_keys_progress line 83
  10. theorem OAI.EditApproximation.physicalRefinementWarmupRead_keys_pass_copy line 122
  11. theorem OAI.EditApproximation.physicalRefinementDataRequest_keys_pass_copy line 133
  12. theorem OAI.EditApproximation.physicalWarmupRequestQuery_keys_progress line 170