ChargedRandomCoarseOracle.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

A fixed accepted source family leaves a nonanticipating coarse query: coarse values enter only when the corresponding leaf is requested.

theorem OAI.EditApproximation.physicalRandomGlobalQuery_refinement_initial_independent line 21

theorem OAI.EditApproximation.chargedRandomGlobalQuery_table_initial_independent line 35

Source documentation

Coarse answers enter the charged program only at coarse leaves.

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

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

def OAI.EditApproximation.chargedRandomCoarseQuery line 54
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.
```
noncomputable def chargedRandomCoarseQuery (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.chargedRandomCoarseQuery_value line 66