SourceSeedConditionalSupport.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Strict support for the actual finite conditional reconstruction. Every advertised branch/mask fiber has positive source mass, so the zero-fiber fallback is never used for these concrete kernels. The conditional law is supported exactly on its fiber, not on the whole source space; this does not remove the secretary replay's every-seed mismatch guard.

Source: sections/secretary.tex, lines 68--78, SHA256 3554fe0f7296782edf63cc7f1305c377e7a7b9d8f8948b9510ea4ad02a702d63.

theorem OAI.MatroidProphet.SourceSeedSupport.coupling_fiberMass_pos line 21
theorem OAI.MatroidProphet.SourceSeedSupport.couplingKernel_singleton_pos_iff line 44
Source documentation
Each complete source seed has positive conditional mass exactly in its advertised branch/mask fiber, including unused source coordinates.
```
theorem couplingKernel_singleton_pos_iff {n : ℕ} (M : Matroid (Fin n))
    (hE : M.E = Set.univ) (b : SourceObservation n) (r : Seed (mainSeedBits n)) :
    0 < couplingKernel M hE b {r} ↔ couplingObservation M hE r = b := by
…
```
Mentions: OAI.MatroidProphet.Seed, OAI.MatroidProphet.mainSeedBits