RepresentationScheduleQueries.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Concrete child-stream and reader-query budgets for the full schedule

theorem OAI.LowSpaceSubsetSum.RepresentationParentData.pair_outputUniverse_empty line 17

theorem OAI.LowSpaceSubsetSum.RepresentationSetup.schedule_unrestrictedChildCount line 43

Source documentation

Exact identification with the four raw child counts used in the resource event, including both complementary residues.

theorem schedule_unrestrictedChildCount :
    ((R.scheduleData h r hn hlog q hq).parentData 0 0).unrestrictedChildCount +
      ((R.scheduleData h r hn hlog q hq).parentData 1 0).unrestrictedChildCount =
        RepresentationMoments.G (prefixModulus_pos h.2 1) (prefixModulus_pos h.2 2)
          (R.signedWeights h.1.1.1)
          (R.rawLeaf h.1.1.1 h.1.1.2 h.1.2
            (R.allocatedBackground h.1.1.1 h.1.1.2 hn hlog) 0)
          (R.rawLeaf h.1.1.1 h.1.1.2 h.1.2
            (R.allocatedBackground h.1.1.1 h.1.1.2 hn hlog) 1)
          (R.signedTarget h.1.1.1) r := by
…

Mentions: OAI.LowSpaceSubsetSum.RepresentationMoments.G, OAI.LowSpaceSubsetSum.prefixModulus_pos

theorem OAI.LowSpaceSubsetSum.RepresentationSetup.schedule_child_resource line 79
theorem OAI.LowSpaceSubsetSum.RepresentationSetup.schedule_matching_resource line 87

theorem OAI.LowSpaceSubsetSum.RepresentationSetup.schedule_queryVisits_sum_bound line 97

Source documentation

Reader queries over all prefixes in a side of the full residue loop.

theorem schedule_queryVisits_sum_bound (B : ℕ) (side : Fin 2) :
    ∑ z : Fin q, ((R.scheduleData h r hn hlog q hq).parentData side z.val).queryVisits B
      (R.scheduleData h r hn hlog q hq).topOrder MaskRestriction.empty ≤
      (6 * ((R.scheduleData h r hn hlog q hq).parentData side 0).unrestrictedChildCount + 2) *
        (∑ z : Fin q, ((R.scheduleData h r hn hlog q hq).parentData side z.val).taskStarts B
          (R.scheduleData h r hn hlog q hq).topOrder MaskRestriction.empty) +
        (mixerSize n + 1) * ((R.scheduleData h r hn hlog q hq).lowMatchingUniverse side).card := by
…

Mentions: OAI.LowSpaceSubsetSum.MaskRestriction.empty, OAI.LowSpaceSubsetSum.mixerSize