Model.lean`

32 declarations, 0 contain sorry, 0 declared as axioms

structure OAI.WLIdentification.Graph line 7
Also declared: ComparatorChallenges/WLIdentification.lean:7 (same declaration text).
def OAI.WLIdentification.Isomorphic line 13
Also declared: ComparatorChallenges/WLIdentification.lean:13 (same declaration text).
def OAI.WLIdentification.NeighborColor line 17
Source documentation
Colors retain their full history, and hence are shared between graphs.
Also declared: ComparatorChallenges/WLIdentification.lean:17 (same declaration text).
```
def NeighborColor : ℕ → Type
  | 0 => Unit
  | s + 1 => NeighborColor s × Multiset (NeighborColor s)
```
def OAI.WLIdentification.neighborColor line 21
Also declared: ComparatorChallenges/WLIdentification.lean:21 (same declaration text).
def OAI.WLIdentification.neighborHistogram line 26
Also declared: ComparatorChallenges/WLIdentification.lean:26 (same declaration text).
def OAI.WLIdentification.TupleColor line 29
Also declared: ComparatorChallenges/WLIdentification.lean:29 (same declaration text).

def OAI.WLIdentification.tupleColor line 34

Source documentation

Joint update: one multiset of whole replacement vectors, not independent marginals.

Also declared: ComparatorChallenges/WLIdentification.lean:34 (same declaration text).

def tupleColor (G : Graph) (k : ℕ) : (s : ℕ) → (Fin k → Fin G.order) → TupleColor k s
  | 0, v => (fun i j => decide (v i = v j), fun i j => G.edge (v i) (v j))
  | s + 1, v => (tupleColor G k s v,
      Finset.univ.val.map (fun z => fun i => tupleColor G k s (Function.update v i z)))

Mentions: OAI.WLIdentification.Graph, OAI.WLIdentification.TupleColor

def OAI.WLIdentification.tupleHistogram line 39
Also declared: ComparatorChallenges/WLIdentification.lean:39 (same declaration text).
def OAI.WLIdentification.Equivalent line 42
Also declared: ComparatorChallenges/WLIdentification.lean:42 (same declaration text).
def OAI.WLIdentification.Identifies line 47
Source documentation
There is no restriction to mates from a graph construction or to a selected order.
Also declared: ComparatorChallenges/WLIdentification.lean:47 (same declaration text).
```
def Identifies (k : ℕ) (G : Graph) : Prop :=
…
```
Mentions: OAI.WLIdentification.Graph
def OAI.WLIdentification.WLdim line 51
Source documentation
The infimum of the positive identifying dimensions; this set is nonempty for finite G.
Also declared: ComparatorChallenges/WLIdentification.lean:51 (same declaration text).
```
noncomputable def WLdim (G : Graph) : ℕ :=
…
```
Mentions: OAI.WLIdentification.Graph
abbrev OAI.WLIdentification.Word line 54
Also declared: ComparatorChallenges/WLIdentification.lean:54 (same declaration text).
abbrev OAI.WLIdentification.BinaryLanguage line 55
Also declared: ComparatorChallenges/WLIdentification.lean:55 (same declaration text).
def OAI.WLIdentification.binaryValue line 57
Also declared: ComparatorChallenges/WLIdentification.lean:57 (same declaration text).
def OAI.WLIdentification.matrixWord line 60
Also declared: ComparatorChallenges/WLIdentification.lean:60 (same declaration text).
def OAI.WLIdentification.inputWord line 64
Source documentation
Unary order header, row-major binary matrix, then most-significant-first binary k.
Also declared: ComparatorChallenges/WLIdentification.lean:64 (same declaration text).
```
def inputWord (G : Graph) (bits : Word) : Word :=
…
```
Mentions: OAI.WLIdentification.Graph, OAI.WLIdentification.Word
def OAI.WLIdentification.dimensionLanguage line 68
Source documentation
A malformed word is rejected: membership requires a valid nonempty simple matrix and k>0.
Also declared: ComparatorChallenges/WLIdentification.lean:68 (same declaration text).
```
def dimensionLanguage : BinaryLanguage :=
…
```
Mentions: OAI.WLIdentification.BinaryLanguage
inductive OAI.WLIdentification.Move line 76
Source comment
The deterministic local machine model is explicit; no oracle or arbitrary state-transition on whole inputs is included. Both alphabets are fixed finite types for each machine. Extra symbols and states allow arbitrary finite tables.
Also declared: ComparatorChallenges/WLIdentification.lean:76 (same declaration text).
```
inductive Move where
…
```
def OAI.WLIdentification.Move.displacement line 80
Also declared: ComparatorChallenges/WLIdentification.lean:80 (same declaration text).
structure OAI.WLIdentification.Machine line 85
Also declared: ComparatorChallenges/WLIdentification.lean:85 (same declaration text).
structure OAI.WLIdentification.Configuration line 91
Also declared: ComparatorChallenges/WLIdentification.lean:91 (same declaration text).
def OAI.WLIdentification.inputSymbol line 96
Also declared: ComparatorChallenges/WLIdentification.lean:96 (same declaration text).
def OAI.WLIdentification.initial line 99
Also declared: ComparatorChallenges/WLIdentification.lean:99 (same declaration text).
def OAI.WLIdentification.Halted line 104
Also declared: ComparatorChallenges/WLIdentification.lean:104 (same declaration text).
def OAI.WLIdentification.step line 108
Source documentation
One read/write/head-movement transition. A halted configuration is frozen.
Also declared: ComparatorChallenges/WLIdentification.lean:108 (same declaration text).
```
def step (M : Machine) (c : Configuration M) : Configuration M :=
…
```
Mentions: OAI.WLIdentification.Machine, OAI.WLIdentification.Configuration
def OAI.WLIdentification.run line 114
Also declared: ComparatorChallenges/WLIdentification.lean:114 (same declaration text).
def OAI.WLIdentification.Output line 118
Source documentation
Output is the binary word beginning at origin and ending at its first blank.
Also declared: ComparatorChallenges/WLIdentification.lean:118 (same declaration text).
```
def Output {M : Machine} (c : Configuration M) (w : Word) : Prop :=
…
```
Mentions: OAI.WLIdentification.Machine, OAI.WLIdentification.Configuration, OAI.WLIdentification.Word
def OAI.WLIdentification.DecidesWithin line 123
Source documentation
Uniform genuine executions on every bit word, including malformed graph words.
Also declared: ComparatorChallenges/WLIdentification.lean:123 (same declaration text).
```
def DecidesWithin (M : Machine) (L : BinaryLanguage) (bound : ℕ → ℕ) : Prop :=
…
```
Mentions: OAI.WLIdentification.Machine, OAI.WLIdentification.BinaryLanguage
def OAI.WLIdentification.InEXPTIME line 126
Also declared: ComparatorChallenges/WLIdentification.lean:126 (same declaration text).
def OAI.WLIdentification.ComputesWithin line 130
Also declared: ComparatorChallenges/WLIdentification.lean:130 (same declaration text).
def OAI.WLIdentification.PolytimeManyOne line 133
Also declared: ComparatorChallenges/WLIdentification.lean:133 (same declaration text).
def OAI.WLIdentification.EXPTIMEComplete line 137
Also declared: ComparatorChallenges/WLIdentification.lean:137 (same declaration text).