QueryChargedSeedSpace.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.EditApproximation.chargedPhysicalCodeAllocation_le_work line 13
Source documentation
Scalar cells of the actual coarse/table address construction.
```
theorem chargedPhysicalCodeAllocation_le_work {M J n passes copies T S : ℕ}
    (request : ChargedPhysicalRequest M J n passes copies T S) :
    chargedPhysicalCodeAllocation request ≤ (chargedPhysicalCodeWithWork request).2 := by
…
```
Mentions: OAI.EditApproximation.ChargedPhysicalRequest, OAI.EditApproximation.chargedPhysicalCodeAllocation, OAI.EditApproximation.chargedPhysicalCodeWithWork
def OAI.EditApproximation.queryChargedReadHeap line 35
def OAI.EditApproximation.queryChargedSeedAtHeap line 41