MaskLaw.lean`

13 declarations, 0 contain sorry, 0 declared as axioms

Exact branch/sacrificed-mask marginal of the complete source law.

This marginal is taken after integrating all source coins, including test, parity and unused coins. It is not a product-law assertion conditional on the entire secretary seed.

Pinned source: sections/secretary.tex, lines 41--52 and 68--78, SHA256 3554fe0f7296782edf63cc7f1305c377e7a7b9d8f8948b9510ea4ad02a702d63. These are supporting obligations of cor:secretary, not the complete endpoint.

lemma OAI.MatroidProphet.Secretary.branchRate_pos line 21
lemma OAI.MatroidProphet.Secretary.branchRate_lt_one line 24
lemma OAI.MatroidProphet.Secretary.branchRate_main line 27
lemma OAI.MatroidProphet.Secretary.sourceMask_eq_completeHiddenRule line 31
lemma OAI.MatroidProphet.Secretary.triple_mask_expectation line 36
theorem OAI.MatroidProphet.Secretary.integral_branch_sourceMask line 57
Source documentation
Joint branch/mask law. All unused source coins are integrated, not discarded from the information available to the adversary.
```
theorem integral_branch_sourceMask {n : ℕ} (j : Bool) (f : Finset (Fin n) → ℝ) :
    (∫ r, (if mainBranch r = j then f (sourceMask r) else 0) ∂sourceSeedLaw n) =
      (1 / 2 : ℝ) * bitsExpectation (fun _ : Fin n => branchRate j) univ f := by
…
```
Mentions: OAI.MatroidProphet.mainBranch, OAI.MatroidProphet.Secretary.sourceMask, OAI.MatroidProphet.sourceSeedLaw, OAI.MatroidProphet.bitsExpectation, OAI.MatroidProphet.Secretary.branchRate
lemma OAI.MatroidProphet.Secretary.integral_sourceMask_atom line 83
Source documentation
Every branch/mask fiber has its explicit positive Bernoulli product mass.
```
lemma integral_sourceMask_atom {n : ℕ} (j : Bool) (P : Finset (Fin n)) :
    (∫ r, (if mainBranch r = j ∧ sourceMask r = P then (1 : ℝ) else 0)
      ∂sourceSeedLaw n) =
      (1 / 2 : ℝ) * bitsWeight (fun _ : Fin n => branchRate j) univ P := by
…
```
Mentions: OAI.MatroidProphet.mainBranch, OAI.MatroidProphet.Secretary.sourceMask, OAI.MatroidProphet.sourceSeedLaw, OAI.MatroidProphet.bitsWeight, OAI.MatroidProphet.Secretary.branchRate
lemma OAI.MatroidProphet.Secretary.bitsWeight_branchRate_pos line 91
lemma OAI.MatroidProphet.Secretary.sourceMask_atom_real line 100
lemma OAI.MatroidProphet.Secretary.sourceMask_atom line 108
lemma OAI.MatroidProphet.Secretary.sourceMask_atom_pos line 113
theorem OAI.MatroidProphet.Secretary.completeHiddenRule_joint_atom line 120
Source documentation
The same atom identity stated directly for the source algorithm's actual branch-tagged observation; this is the finite conditional-kernel interface.
```
theorem completeHiddenRule_joint_atom {n : ℕ} (M : Matroid (Fin n))
    (hE : M.E = Set.univ) (j : Bool) (P : Finset (Fin n)) :
    sourceSeedLaw n {r | (mainBranch r, (completeHiddenRule M hE).mask r) = (j, P)} =
      ENNReal.ofReal ((1 / 2 : ℝ) * bitsWeight (fun _ : Fin n => branchRate j) univ P) := by
…
```
Mentions: OAI.MatroidProphet.sourceSeedLaw, OAI.MatroidProphet.mainBranch, OAI.MatroidProphet.completeHiddenRule, OAI.MatroidProphet.bitsWeight, OAI.MatroidProphet.Secretary.branchRate
theorem OAI.MatroidProphet.Secretary.completeHiddenRule_joint_atom_pos line 127