WitnessSystemCodes.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

Finite endpoint, partner, and label descriptions for selected witness systems.

abbrev OAI.TwoPointCorrelations.WitnessRelationSlot line 13
Source documentation
Two labels, a partner witness, and four bounded endpoints. Internal relations leave the unused entries arbitrary.
```
abbrev WitnessRelationSlot (n N : ℕ) (ι : Type*) :=
…
```
structure OAI.TwoPointCorrelations.WitnessSystemData line 18
Source documentation
The mode records the two internal and the two comparison alternatives. Every selected witness has only bounded numerical-index metadata.
```
structure WitnessSystemData (n N : ℕ) (ι : Type*) where
…
```
def OAI.TwoPointCorrelations.witnessSystemCode line 23
lemma OAI.TwoPointCorrelations.witnessSystemCode_injective line 28
instance OAI.TwoPointCorrelations.(instance at line 53) line 53
instance OAI.TwoPointCorrelations.(instance at line 56) line 56
lemma OAI.TwoPointCorrelations.card_witnessRelationSlot line 59
theorem OAI.TwoPointCorrelations.card_witnessSystemData_le line 66
Source documentation
A single optional-slot function records the chosen set as well as all its data, so no extra subset-count factor is needed.
```
theorem card_witnessSystemData_le (n N : ℕ) (ι : Type*) [Fintype ι] :
    Fintype.card (WitnessSystemData n N ι) ≤
      4 * (1 + Fintype.card ι ^ 2 * n * (N + 1) ^ 4) ^ n := by
…
```
Mentions: OAI.TwoPointCorrelations.WitnessSystemData