ChargedRandomGlobalQuery.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

The coarse seed, recursive table values, and random scalar sources are all requested through the memo program. Inactive refinement branches use the existing explicit coarse/median seed queries.

theorem OAI.EditApproximation.chargedRandomGlobalQuery_value line 32

Source documentation

Composition with the local source-provider correctness theorem.

 theorem chargedRandomGlobalQuery_value
    (hbody : ∀ parent,
      (physicalRandomBoundedQuery source target N P F exponent H Q T S passes copies factor multiplier
        tau eta kappa delta readGroup readInteger initial parent).value
        (Sum.elim sourceAnswer (fun child => localRequestValue source target N P F exponent H Q T S copies
          factor multiplier tau eta kappa delta group integer initial child.val.val)) =
      localRequestValue source target N P F exponent H Q T S copies factor multiplier
        tau eta kappa delta group integer initial parent.val)
    (request : ChargedPhysicalRequest M J target.length 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 initial request).value
      (Sum.elim sourceAnswer (fun child => chargedRequestValue source target N P F exponent H Q T S
…

Mentions: OAI.EditApproximation.physicalRandomBoundedQuery, OAI.EditApproximation.localRequestValue, OAI.EditApproximation.ChargedPhysicalRequest, OAI.EditApproximation.chargedRandomGlobalQuery, OAI.EditApproximation.chargedRequestValue