ChargedCoarseOracle.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

All initial-entry information used by a charged table body arrives through explicit requests. Flattening those requests gives an adaptive coarse oracle program whose shape is independent of coarse answers.

def OAI.EditApproximation.FiniteQuery.substitute line 14
theorem OAI.EditApproximation.FiniteQuery.substitute_cost line 18
theorem OAI.EditApproximation.FiniteQuery.substitute_value line 28

theorem OAI.EditApproximation.physicalGlobalQuery_refinement_initial_independent line 49

Source documentation

An internal refinement body never inspects a coarse seed function while building its local query. Its seed needs are explicit child reads.

theorem physicalGlobalQuery_refinement_initial_independent
    (left right : PhysicalEntry M J target.length → ℕ)
    (parent : PhysicalTableRequest M J target.length)
    (hi : ¬ parent.index ≤ T) (hd : parent.node.1.val < J)
    (hw : ¬ (physicalSourceInterval source.length parent.node).hi -
      (physicalSourceInterval source.length parent.node).lo ≤ 1) :
    physicalGlobalQuery source target N P F exponent H Q T S copies factor multiplier
      tau eta kappa delta group integer left parent =
    physicalGlobalQuery source target N P F exponent H Q T S copies factor multiplier
      tau eta kappa delta group integer right parent := by
…

Mentions: OAI.EditApproximation.PhysicalEntry, OAI.EditApproximation.PhysicalTableRequest, OAI.EditApproximation.physicalSourceInterval, OAI.EditApproximation.physicalGlobalQuery

theorem OAI.EditApproximation.chargedGlobalQuery_table_initial_independent line 65

Source documentation

Coarse answers enter the charged program only at coarse leaves.

theorem chargedGlobalQuery_table_initial_independent
    (left right : PhysicalEntry M J target.length → ℕ)
    (parent : {request : PhysicalTableRequest M J target.length // request.Bounded passes copies T S}) :
    chargedGlobalQuery source target N P F exponent H Q T S passes copies factor multiplier
      tau eta kappa delta group integer left (.inr parent) =
    chargedGlobalQuery source target N P F exponent H Q T S passes copies factor multiplier
      tau eta kappa delta group integer right (.inr parent) := by
…

Mentions: OAI.EditApproximation.PhysicalEntry, OAI.EditApproximation.PhysicalTableRequest, OAI.EditApproximation.chargedGlobalQuery

def OAI.EditApproximation.chargedCoarseQuery line 84
Source documentation
The flattened program receives each coarse answer from an explicit external read. The constant zero here is never used as a seed answer.
```
def chargedCoarseQuery (root : ChargedPhysicalRequest M J target.length passes copies T S) :
    FiniteQuery (PhysicalEntry M J target.length) :=
…
```
Mentions: OAI.EditApproximation.ChargedPhysicalRequest, OAI.EditApproximation.FiniteQuery, OAI.EditApproximation.PhysicalEntry
theorem OAI.EditApproximation.chargedCoarseQuery_value line 95