TripleKernelModel.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

Concrete one-label conditional kernel for the secretary reconstruction. The boolean records membership in the sacrificed observation mask, not branch choice. The three coordinates are the original H, D, C coins; the T coin is not sacrificed.

abbrev OAI.MatroidProphet.Secretary.MaskTriple line 13
def OAI.MatroidProphet.Secretary.tripleRevealed line 16
Source documentation
Whether at least one of the three observation coins is set.
```
def tripleRevealed (x : MaskTriple) : Bool := x.1 || x.2.1 || x.2.2
```
Mentions: OAI.MatroidProphet.Secretary.MaskTriple
def OAI.MatroidProphet.Secretary.tripleWeight line 19
Source documentation
The independent H,D,C law at one label, retaining the thinning parameter.
```
noncomputable def tripleWeight (t : ℝ) (x : MaskTriple) : ℝ :=
…
```
Mentions: OAI.MatroidProphet.Secretary.MaskTriple
def OAI.MatroidProphet.Secretary.mainRevealRate line 24
Source documentation
Probability that a label is sacrificed in the main branch.
```
noncomputable def mainRevealRate : ℝ := 5 / 8 + 3 * thinningRate / 8
```
Mentions: OAI.MatroidProphet.thinningRate
def OAI.MatroidProphet.Secretary.conditionalTripleWeight line 28
Source documentation
The source specifies all seven nonzero triple masses divided by the reveal rate. Outside the observation set the triple is deterministically zero.
```
noncomputable def conditionalTripleWeight (revealed : Bool) (x : MaskTriple) : ℝ :=
…
```
Mentions: OAI.MatroidProphet.Secretary.MaskTriple
def OAI.MatroidProphet.Secretary.revealBitWeight line 34
Source documentation
Probability of a prescribed observation-mask membership bit.
```
noncomputable def revealBitWeight (revealed : Bool) : ℝ :=
…
```