Model.lean`

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

structure OAI.MatchingFPRAS.GraphInput line 8
Source documentation
Each unordered edge is represented once, by increasing endpoints.
Also declared: ComparatorChallenges/MatchingFPRAS.lean:8 (same declaration text).
```
structure GraphInput where
…
```
def OAI.MatchingFPRAS.Perfect line 14
Source documentation
Exactly one selected edge is incident to every vertex.
Also declared: ComparatorChallenges/MatchingFPRAS.lean:14 (same declaration text).
```
def Perfect (G : GraphInput) (M : Finset (Fin G.n × Fin G.n)) : Prop :=
…
```
Mentions: OAI.MatchingFPRAS.GraphInput
def OAI.MatchingFPRAS.perfectMatchings line 17
Also declared: ComparatorChallenges/MatchingFPRAS.lean:17 (same declaration text).
def OAI.MatchingFPRAS.Z line 23
Source documentation
The exact unweighted count, including the empty graph.
Also declared: ComparatorChallenges/MatchingFPRAS.lean:23 (same declaration text).
```
noncomputable def Z (G : GraphInput) : ℕ := (perfectMatchings G).card
```
Mentions: OAI.MatchingFPRAS.GraphInput, OAI.MatchingFPRAS.perfectMatchings
abbrev OAI.MatchingFPRAS.Symbol line 25
Also declared: ComparatorChallenges/ContingencyTables.lean:7 (same declaration text), ComparatorChallenges/MatchingFPRAS.lean:25 (same declaration text).
def OAI.MatchingFPRAS.encodeNat line 28
Source documentation
Binary numeral followed by a delimiter. Tape blank is 0; bits use 1 and 2.
Also declared: ComparatorChallenges/ContingencyTables.lean:10 (same declaration text), ComparatorChallenges/MatchingFPRAS.lean:28 (same declaration text).
```
def encodeNat (n : ℕ) : List Symbol :=
…
```
Mentions: OAI.MatchingFPRAS.Symbol
def OAI.MatchingFPRAS.encodeInt line 31
Also declared: ComparatorChallenges/ContingencyTables.lean:13 (same declaration text), ComparatorChallenges/MatchingFPRAS.lean:31 (same declaration text).
def OAI.MatchingFPRAS.encodeRat line 35
Source documentation
A rational encoded by its reduced numerator and positive denominator.
Also declared: ComparatorChallenges/ContingencyTables.lean:17 (same declaration text), ComparatorChallenges/MatchingFPRAS.lean:35 (same declaration text).
```
def encodeRat (q : ℚ) : List Symbol := encodeInt q.num ++ encodeNat q.den
```
Mentions: OAI.MatchingFPRAS.Symbol, OAI.MatchingFPRAS.encodeInt, OAI.MatchingFPRAS.encodeNat
def OAI.MatchingFPRAS.encodeInput line 38
Source documentation
Explicit sparse graph encoding, then the two rational parameters.
Also declared: ComparatorChallenges/MatchingFPRAS.lean:38 (same declaration text).
```
def encodeInput (G : GraphInput) (ε δ : ℚ) : List Symbol :=
…
```
Mentions: OAI.MatchingFPRAS.GraphInput, OAI.MatchingFPRAS.Symbol
structure OAI.MatchingFPRAS.RandomMachine line 45
Source documentation
A uniform randomized Post-Turing machine: a single finite transition table.
Also declared: ComparatorChallenges/ContingencyTables.lean:20 (same declaration text), ComparatorChallenges/MatchingFPRAS.lean:45 (same declaration text).
```
structure RandomMachine where
…
```
structure OAI.MatchingFPRAS.Configuration line 50
Also declared: ComparatorChallenges/ContingencyTables.lean:25 (same declaration text), ComparatorChallenges/MatchingFPRAS.lean:50 (same declaration text).
def OAI.MatchingFPRAS.tick line 56
Source documentation
A halted configuration is absorbing. Each nonhalting tick is exactly one write or one move, or the detection of halt.
Also declared: ComparatorChallenges/ContingencyTables.lean:31 (same declaration text), ComparatorChallenges/MatchingFPRAS.lean:56 (same declaration text).
```
def tick (A : RandomMachine) (c : Configuration A) (bit : Bool) : Configuration A :=
…
```
Mentions: OAI.MatchingFPRAS.RandomMachine, OAI.MatchingFPRAS.Configuration
def OAI.MatchingFPRAS.initial line 66
Also declared: ComparatorChallenges/ContingencyTables.lean:41 (same declaration text), ComparatorChallenges/MatchingFPRAS.lean:66 (same declaration text).
def OAI.MatchingFPRAS.run line 70
Source documentation
Bounded execution on a finite prefix of the random tape.
Also declared: ComparatorChallenges/ContingencyTables.lean:45 (same declaration text), ComparatorChallenges/MatchingFPRAS.lean:70 (same declaration text).
```
def run (A : RandomMachine) (input : List Symbol) {t : ℕ}
    (bits : Fin t → Bool) : Configuration A :=
…
```
Mentions: OAI.MatchingFPRAS.RandomMachine, OAI.MatchingFPRAS.Symbol, OAI.MatchingFPRAS.Configuration
def OAI.MatchingFPRAS.Outputs line 74
Also declared: ComparatorChallenges/ContingencyTables.lean:49 (same declaration text), ComparatorChallenges/MatchingFPRAS.lean:74 (same declaration text).
def OAI.MatchingFPRAS.timeBound line 81
Source documentation
A fixed-degree polynomial in input bits, ε⁻¹, and log δ⁻¹. Natural ceilings and binary ceiling-log change this bound only by constants.
Also declared: ComparatorChallenges/MatchingFPRAS.lean:81 (same declaration text).
```
def timeBound (C d : ℕ) (G : GraphInput) (ε δ : ℚ) : ℕ :=
…
```
Mentions: OAI.MatchingFPRAS.GraphInput
def OAI.MatchingFPRAS.goodTapes line 84
Also declared: ComparatorChallenges/MatchingFPRAS.lean:84 (same declaration text).
def OAI.MatchingFPRAS.MainStatement line 94
Source documentation
A uniform approximation scheme using independent fair bits. All tapes halt within the fixed polynomial bound and return a nonnegative rational. A zero count always produces encoded zero.
Also declared: ComparatorChallenges/MatchingFPRAS.lean:94 (same declaration text).
```
def MainStatement : Prop :=
…
```