WitnessSystemDecoding.lean`

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

Decode bounded witness metadata into the actual interval or comparison relations.

structure OAI.TwoPointCorrelations.PackedPrimeRelation line 11
abbrev OAI.TwoPointCorrelations.WitnessSystemData.selected line 22
abbrev OAI.TwoPointCorrelations.WitnessSystemData.control line 23
abbrev OAI.TwoPointCorrelations.WitnessSystemData.partner line 24
abbrev OAI.TwoPointCorrelations.WitnessSystemData.left line 25
abbrev OAI.TwoPointCorrelations.WitnessSystemData.right line 26
abbrev OAI.TwoPointCorrelations.WitnessSystemData.departure line 27
abbrev OAI.TwoPointCorrelations.WitnessSystemData.partnerDeparture line 28
def OAI.TwoPointCorrelations.WitnessSystemData.relation line 32
Source documentation
Modes zero and one use internal intervals. Modes two and three use the earlier and later comparison, respectively.
```
def relation (d : WitnessSystemData n N ι) (main : LabeledPrimeWord ι)
    (word : Fin n → LabeledPrimeWord ι) (h : ℕ) (i : d.chosen) : PackedPrimeRelation ι :=
…
```
Mentions: OAI.TwoPointCorrelations.WitnessSystemData, OAI.TwoPointCorrelations.LabeledPrimeWord, OAI.TwoPointCorrelations.PackedPrimeRelation
def OAI.TwoPointCorrelations.WitnessSystemData.chosenOrder line 49
def OAI.TwoPointCorrelations.WitnessSystemData.Triangular line 55
Source documentation
This is a support property of the decoded expressions, independent of all numerical values assigned to the prime labels.
```
def Triangular (d : WitnessSystemData n N ι) (main : LabeledPrimeWord ι)
    (word : Fin n → LabeledPrimeWord ι) (h : ℕ) : Prop :=
…
```
Mentions: OAI.TwoPointCorrelations.WitnessSystemData, OAI.TwoPointCorrelations.LabeledPrimeWord
def OAI.TwoPointCorrelations.WitnessSystemData.Holds line 62
def OAI.TwoPointCorrelations.WitnessSystemData.toSystem line 66
lemma OAI.TwoPointCorrelations.WitnessSystemData.toSystem_size line 80
lemma OAI.TwoPointCorrelations.WitnessSystemData.toSystem_holds line 85