RepresentationScheduleMatching.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

Raw occurrence accounting across all lifted parent residues

def OAI.LowSpaceSubsetSum.RepresentationScheduleData.lowMatchingUniverse line 18
theorem OAI.LowSpaceSubsetSum.RepresentationScheduleData.matchingUniverse_subset_low line 28
theorem OAI.LowSpaceSubsetSum.RepresentationScheduleData.matchingUniverses_disjoint line 46
theorem OAI.LowSpaceSubsetSum.RepresentationScheduleData.sum_matchingUniverse_card line 60
theorem OAI.LowSpaceSubsetSum.RepresentationScheduleData.unrestrictedChildCount_eq_zero line 75
Source documentation
Child stream membership is independent of the full parent-residue counter.
```
theorem unrestrictedChildCount_eq_zero (side : Fin 2) (z : ℕ) :
    (D.parentData side z).unrestrictedChildCount =
      (D.parentData side 0).unrestrictedChildCount := rfl
…
```
theorem OAI.LowSpaceSubsetSum.RepresentationSetup.schedule_lowMatchingUniverse_card line 88

theorem OAI.LowSpaceSubsetSum.RepresentationSetup.schedule_matchingVisits_sum_bound line 126

Source documentation

Full-residue iteration and prefix recomputation multiply the raw tuple resource charge only by the top-mask length.

theorem schedule_matchingVisits_sum_bound (B : ℕ) (side : Fin 2) :
    ∑ z : Fin q, ((R.scheduleData h r hn hlog q hq).parentData side z.val).matchingVisits 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