SourceSeedSupport.lean`

19 declarations, 0 contain sorry, 0 declared as axioms

Full support of the actual source seed

All four masks and both coins remain in the source law, including coordinates unused in the selected branch. Strictly positive atom masses justify finite conditional reconstruction on every realizable observation fiber. No nonempty label or positive-rank assumption is made.

Source: sections/secretary.tex, conditional reconstruction paragraph (lines 65–81), SHA256 3554fe0f7296782edf63cc7f1305c377e7a7b9d8f8948b9510ea4ad02a702d63. These are supporting positivity obligations, not the secretary endpoint or a replacement for the joint-law and prefix-only online-rule constructions.

lemma OAI.MatroidProphet.SourceSeedSupport.bitsWeight_pos line 23
lemma OAI.MatroidProphet.SourceSeedSupport.bernoulliSeedLaw_singleton_pos line 32
lemma OAI.MatroidProphet.SourceSeedSupport.maskCoinLaw_singleton_pos line 39
lemma OAI.MatroidProphet.SourceSeedSupport.prod_singleton_pos line 43
lemma OAI.MatroidProphet.SourceSeedSupport.mainBlockLaw_singleton_pos line 51
lemma OAI.MatroidProphet.SourceSeedSupport.encodeMainSeed_surjective line 67
Source documentation
The block encoding retains every bit; it is onto even for an empty ground set.
```
lemma encodeMainSeed_surjective (n : ℕ) :
    Function.Surjective (@encodeMainSeed n) := by
…
```
Mentions: OAI.MatroidProphet.encodeMainSeed
lemma OAI.MatroidProphet.SourceSeedSupport.mainSeedLaw_singleton_pos line 85
lemma OAI.MatroidProphet.SourceSeedSupport.sourceCoinProbability_pos line 97
lemma OAI.MatroidProphet.SourceSeedSupport.sourceCoinProbability_lt_one line 101
theorem OAI.MatroidProphet.SourceSeedSupport.sourceSeedLaw_singleton_pos line 106
Source documentation
Every complete source seed has positive mass, with no exceptional labels or ranks.
```
theorem sourceSeedLaw_singleton_pos (n : ℕ) (r : Seed (mainSeedBits n)) :
    0 < sourceSeedLaw n {r} :=
…
```
Mentions: OAI.MatroidProphet.Seed, OAI.MatroidProphet.mainSeedBits, OAI.MatroidProphet.sourceSeedLaw
theorem OAI.MatroidProphet.SourceSeedSupport.sourceSeedLaw_fiber_pos_iff line 113
Source documentation
A source observation fiber has positive probability exactly when it is realizable. The observation may keep branch, mask, and any additional seed coordinates.
```
theorem sourceSeedLaw_fiber_pos_iff (n : ℕ) {β : Type*}
    (f : Seed (mainSeedBits n) → β) (b : β) :
    0 < sourceSeedLaw n {r | f r = b} ↔ ∃ r, f r = b := by
…
```
Mentions: OAI.MatroidProphet.Seed, OAI.MatroidProphet.mainSeedBits, OAI.MatroidProphet.sourceSeedLaw
theorem OAI.MatroidProphet.SourceSeedSupport.sourceSeedLaw_fiber_toReal_pos line 134
Source documentation
Real-valued finite conditional-kernel denominators are strictly positive.
```
theorem sourceSeedLaw_fiber_toReal_pos (n : ℕ) {β : Type*}
    (f : Seed (mainSeedBits n) → β) (r : Seed (mainSeedBits n)) :
    0 < (sourceSeedLaw n {s | f s = f r}).toReal := by
…
```
Mentions: OAI.MatroidProphet.Seed, OAI.MatroidProphet.mainSeedBits, OAI.MatroidProphet.sourceSeedLaw
theorem OAI.MatroidProphet.SourceSeedSupport.exists_mainMasks_mainBranch line 142
Source documentation
Every assignment of all four masks, parity, and branch is realized by a seed.
```
theorem exists_mainMasks_mainBranch {n : ℕ} (d : MainMasks n) (j : Bool) :
    ∃ r : Seed (mainSeedBits n), mainMasks r = d ∧ mainBranch r = j := by
…
```
Mentions: OAI.MatroidProphet.MainMasks, OAI.MatroidProphet.Seed, OAI.MatroidProphet.mainSeedBits, OAI.MatroidProphet.mainMasks, OAI.MatroidProphet.mainBranch
theorem OAI.MatroidProphet.SourceSeedSupport.sourceSeedLaw_masks_branch_pos line 155
Source documentation
The entire mask/coin assignment has positive mass, including either unused branch.
```
theorem sourceSeedLaw_masks_branch_pos {n : ℕ} (d : MainMasks n) (j : Bool) :
    0 < sourceSeedLaw n {r | mainMasks r = d ∧ mainBranch r = j} := by
…
```
Mentions: OAI.MatroidProphet.MainMasks, OAI.MatroidProphet.sourceSeedLaw, OAI.MatroidProphet.mainMasks, OAI.MatroidProphet.mainBranch
theorem OAI.MatroidProphet.SourceSeedSupport.sourceSeedLaw_branch_mask_pos line 166
Source documentation
Both source branches admit every sacrificed-mask fiber with positive mass.
```
theorem sourceSeedLaw_branch_mask_pos (n : ℕ) (j : Bool) (P : Finset (Fin n)) :
    0 < sourceSeedLaw n {r | mainBranch r = j ∧
      (if mainBranch r then (mainMasks r).H ∪ (mainMasks r).D ∪ (mainMasks r).C
        else (mainMasks r).H) = P} := by
…
```
Mentions: OAI.MatroidProphet.sourceSeedLaw, OAI.MatroidProphet.mainBranch, OAI.MatroidProphet.mainMasks
theorem OAI.MatroidProphet.SourceSeedSupport.sourceSeedLaw_actual_branch_mask_pos line 178
Source documentation
The positivity statement for the actual algorithmic sacrificed mask, rather than a surrogate observation map.
```
theorem sourceSeedLaw_actual_branch_mask_pos {n : ℕ} (M : Matroid (Fin n))
    (hE : M.E = Set.univ) (j : Bool) (P : Finset (Fin n)) :
    0 < sourceSeedLaw n {r | mainBranch r = j ∧ (completeHiddenRule M hE).mask r = P} := by
…
```
Mentions: OAI.MatroidProphet.sourceSeedLaw, OAI.MatroidProphet.mainBranch, OAI.MatroidProphet.completeHiddenRule
theorem OAI.MatroidProphet.SourceSeedSupport.mainMasks_mainBranch_injective line 185
Source documentation
The four masks, parity, and branch determine every original seed coordinate.
```
theorem mainMasks_mainBranch_injective (n : ℕ) :
    Function.Injective (fun r : Seed (mainSeedBits n) => (mainMasks r, mainBranch r)) := by
…
```
Mentions: OAI.MatroidProphet.Seed, OAI.MatroidProphet.mainSeedBits, OAI.MatroidProphet.mainMasks, OAI.MatroidProphet.mainBranch
theorem OAI.MatroidProphet.SourceSeedSupport.source_statistic_factors line 223
Source documentation
Every statistic of the complete source seed can be written using all masks and coins.
```
theorem source_statistic_factors {n : ℕ} {β : Type*}
    (f : Seed (mainSeedBits n) → β) :
    ∃ g : MainMasks n → Bool → β, ∀ r, g (mainMasks r) (mainBranch r) = f r := by
…
```
Mentions: OAI.MatroidProphet.Seed, OAI.MatroidProphet.mainSeedBits, OAI.MatroidProphet.MainMasks, OAI.MatroidProphet.mainMasks, OAI.MatroidProphet.mainBranch
theorem OAI.MatroidProphet.SourceSeedSupport.sourceSeedLaw_ae_iff line 239
Source documentation
Since there are no null source atoms, almost-sure seed properties are pointwise.
```
theorem sourceSeedLaw_ae_iff (n : ℕ) (P : Seed (mainSeedBits n) → Prop) :
    (∀ᵐ r ∂sourceSeedLaw n, P r) ↔ ∀ r, P r := by
…
```
Mentions: OAI.MatroidProphet.Seed, OAI.MatroidProphet.mainSeedBits, OAI.MatroidProphet.sourceSeedLaw