PhysicalDependencyRank.lean`

27 declarations, 0 contain sorry, 0 declared as axioms

Concrete table requests and their dependency order. A single table index identifies the end of warmup with refinement time zero. Copy labels remain part of a request but do not reset its dependency rank.

theorem OAI.EditApproximation.PhysicalTableRequest.refinement_zero_eq_warmup line 32
def OAI.EditApproximation.PhysicalTableRequest.changeCopy line 37
theorem OAI.EditApproximation.PhysicalTableRequest.rank_changeCopy line 40
theorem OAI.EditApproximation.PhysicalTableRequest.remainingDepth_changeCopy line 43
theorem OAI.EditApproximation.PhysicalTableRequest.warmup_rank line 46
theorem OAI.EditApproximation.PhysicalTableRequest.refinement_rank line 50
theorem OAI.EditApproximation.PhysicalTableRequest.remainingDepth_le_of_no_ancestor line 54
theorem OAI.EditApproximation.PhysicalTableRequest.remainingDepth_lt_of_descendant line 59
theorem OAI.EditApproximation.PhysicalTableRequest.sameIndexChild_progress line 68
theorem OAI.EditApproximation.PhysicalTableRequest.rank_lt_same_pass line 78

theorem OAI.EditApproximation.PhysicalTableRequest.warmup_previous_child_progress line 87

Source documentation

A warmup predecessor lies at the physical child and at the preceding unified table index.

theorem warmup_previous_child_progress (pass copy T S j : ℕ)
    (node : PhysicalNode M J) (hbelow : node.1.val < J) (i : Fin M)
    (state previousState : TargetInterval ny) (hj : 0 < j) :
    (warmup pass copy (physicalChild node hbelow i) (j - 1) previousState).remainingDepth <
        (warmup pass copy node j state).remainingDepth ∧
      rank T S (warmup pass copy (physicalChild node hbelow i) (j - 1) previousState) <
        rank T S (warmup pass copy node j state) := by
…

Mentions: OAI.EditApproximation.PhysicalNode, OAI.EditApproximation.TargetInterval, OAI.EditApproximation.PhysicalTableRequest.warmup, OAI.EditApproximation.physicalChild, OAI.EditApproximation.PhysicalTableRequest.remainingDepth, OAI.EditApproximation.PhysicalTableRequest.rank

theorem OAI.EditApproximation.PhysicalTableRequest.refinement_history_progress line 103

Source documentation

Old refinement values and all optimistic-history values have strictly smaller rank, even if their copy label changes.

theorem refinement_history_progress (pass copy previousCopy T S t s : ℕ)
    (node previousNode : PhysicalNode M J) (state previousState : TargetInterval ny)
    (hnode : node.1.val ≤ previousNode.1.val) (hs : s < t) :
    (refinement pass previousCopy previousNode T s previousState).remainingDepth ≤
        (refinement pass copy node T t state).remainingDepth ∧
      rank T S (refinement pass previousCopy previousNode T s previousState) <
        rank T S (refinement pass copy node T t state) := by
…

Mentions: OAI.EditApproximation.PhysicalNode, OAI.EditApproximation.TargetInterval, OAI.EditApproximation.PhysicalTableRequest.refinement, OAI.EditApproximation.PhysicalTableRequest.remainingDepth, OAI.EditApproximation.PhysicalTableRequest.rank

theorem OAI.EditApproximation.PhysicalTableRequest.refinement_history_child_progress line 115
theorem OAI.EditApproximation.PhysicalTableRequest.rank_lt_previous_pass line 132
Source documentation
A previous pass can request any of its warmup/refinement indices. The added one in the pass stride makes its last index strictly earlier than the next pass's first index.
```
theorem rank_lt_previous_pass (T S : ℕ) (first second : PhysicalTableRequest M J ny)
    (hpass : second.pass < first.pass) (hindex : second.index ≤ T + S) :
    rank T S second < rank T S first := by
…
```
Mentions: OAI.EditApproximation.PhysicalTableRequest, OAI.EditApproximation.PhysicalTableRequest.rank
theorem OAI.EditApproximation.PhysicalTableRequest.previous_pass_progress line 141
theorem OAI.EditApproximation.PhysicalTableRequest.rank_lt_pass_bound line 148
theorem OAI.EditApproximation.PhysicalTableRequest.warmup_index_bound line 156
theorem OAI.EditApproximation.PhysicalTableRequest.refinement_index_bound line 162
theorem OAI.EditApproximation.PhysicalTableRequest.warmup_bounded line 168
theorem OAI.EditApproximation.PhysicalTableRequest.refinement_bounded line 174
theorem OAI.EditApproximation.PhysicalTableRequest.bounded_changeCopy line 180
theorem OAI.EditApproximation.PhysicalTableRequest.bounded_sameIndexChild line 185
theorem OAI.EditApproximation.PhysicalTableRequest.bounded_of_earlier_same_pass line 190
theorem OAI.EditApproximation.PhysicalTableRequest.bounded_of_previous_pass line 196
def OAI.EditApproximation.PhysicalTableRequest.boundedTuple line 204
Source documentation
Bounded requests have an explicit finite coordinate representation; the copy coordinate is retained even though the progress rank ignores it.
```
def boundedTuple (passes copies T S : ℕ)
    (request : {r : PhysicalTableRequest M J ny // Bounded passes copies T S r}) :
    Fin passes × Fin copies × PhysicalNode M J × Fin (T + S + 1) × TargetInterval ny :=
…
```
Mentions: OAI.EditApproximation.PhysicalTableRequest, OAI.EditApproximation.PhysicalTableRequest.Bounded, OAI.EditApproximation.PhysicalNode, OAI.EditApproximation.TargetInterval
theorem OAI.EditApproximation.PhysicalTableRequest.boundedTuple_injective line 210
instance OAI.EditApproximation.PhysicalTableRequest.boundedRequestFinite line 233