SourceAssembly.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

The actual hidden-vector performance theorem supplies the secretary bound. The finite coupling laws below are internal inputs; the final endpoint discharges them with the concrete source-prefix/table construction.

theorem OAI.MatroidProphet.SecretaryReplay.reconstructed_source_guarantee line 15

theorem OAI.MatroidProphet.SecretaryReplay.reconstructed_source_witness line 36

Source documentation

A concrete finite coupling completes the entire existential for one matroid, including pointwise feasibility even at null seeds and the full adversary clause.

theorem reconstructed_source_witness.{u} {n : ℕ} {Q : Type*}
    [Fintype Q] [MeasurableSpace Q] [MeasurableSingletonClass Q]
    (M : Matroid (Fin n)) (hE : M.E = Set.univ)
    (K : Q → Fin (n + 1))
    (decode : Q → Finset (Fin n) → Seed (mainSeedBits n))
    (νQ : Measure Q) [IsProbabilityMeasure νQ]
    (hproductLaw : (νQ.prod (Secretary.uniformArrivalLaw n)).map
      (fun z => decode z.1 (orderPrefix z.2 (K z.1).val)) = sourceSeedLaw n)
    (hproductMask : ∀ᵐ z ∂νQ.prod (Secretary.uniformArrivalLaw n),
      (completeHiddenRule M hE).mask (decode z.1 (orderPrefix z.2 (K z.1).val)) =
        orderPrefix z.2 (K z.1).val) :
    ∃ (q : ℕ) (ν : Measure (Fin q)), IsProbabilityMeasure ν ∧
…

Mentions: OAI.MatroidProphet.Seed, OAI.MatroidProphet.mainSeedBits, OAI.MatroidProphet.Secretary.uniformArrivalLaw, OAI.MatroidProphet.orderPrefix, OAI.MatroidProphet.sourceSeedLaw, OAI.MatroidProphet.completeHiddenRule