FiniteSeedModel.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

def OAI.MatroidProphet.finiteSeedEncode line 9
Source documentation
A one-hot code retains the entire finite seed, including unused coordinates.
```
noncomputable def finiteSeedEncode (α : Type*) [Fintype α] (a : α) :
    Seed (Fintype.card α) := by
…
```
Mentions: OAI.MatroidProphet.Seed
def OAI.MatroidProphet.finiteSeedDecode line 15
Source documentation
Total decoding, with an arbitrary fallback on codes outside the encoder range.
```
noncomputable def finiteSeedDecode (α : Type*) [Fintype α] [Nonempty α] :
    Seed (Fintype.card α) → α :=
…
```
Mentions: OAI.MatroidProphet.Seed
def OAI.MatroidProphet.reindexOnlineSeed line 20
Source documentation
Change only the representation of the complete initial seed.
```
noncomputable def reindexOnlineSeed {n bits bits' : ℕ} (A : OnlineRule n bits)
    (f : Seed bits' → Seed bits) : OnlineRule n bits' where
…
```
Mentions: OAI.MatroidProphet.OnlineRule, OAI.MatroidProphet.Seed
def OAI.MatroidProphet.reindexHiddenSeed line 27
Source documentation
The sacrificed mask and every core decision use the same decoded seed.
```
noncomputable def reindexHiddenSeed {n bits bits' : ℕ} (A : HiddenRule n bits)
    (f : Seed bits' → Seed bits) : HiddenRule n bits' where
…
```
Mentions: OAI.MatroidProphet.HiddenRule, OAI.MatroidProphet.Seed