Model.lean`

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

def OAI.DirectedFeedback.natBits line 8
Source documentation
Unary self-delimiting natural numbers. Outputs are explicit, not succinct.
Also declared: ComparatorChallenges/DirectedFeedback.lean:8 (same declaration text).
```
def natBits (n : ℕ) : List Bool := List.replicate n true ++ [false]
```
def OAI.DirectedFeedback.pairBits line 11
Source documentation
The explicit framing used for an input and its NP certificate.
Also declared: ComparatorChallenges/DirectedFeedback.lean:11 (same declaration text).
```
def pairBits (p : List Bool × List Bool) : List Bool :=
…
```
def OAI.DirectedFeedback.FiniteAlphabet line 16
Source documentation
Finitely many stacks and control states are already part of FinTM2. This additionally excludes infinite stack alphabets.
Also declared: ComparatorChallenges/DirectedFeedback.lean:16 (same declaration text).
```
def FiniteAlphabet (M : Turing.FinTM2) : Prop := ∀ k, Finite (M.Γ k)
```
structure OAI.DirectedFeedback.NPVerifier line 20
Source documentation
Polynomially bounded certificates checked by an actual deterministic finite-alphabet machine, on the explicitly encoded input/certificate pair.
Also declared: ComparatorChallenges/DirectedFeedback.lean:20 (same declaration text).
```
structure NPVerifier where
…
```
def OAI.DirectedFeedback.NPVerifier.Accepts line 26
Also declared: ComparatorChallenges/DirectedFeedback.lean:26 (same declaration text).
def OAI.DirectedFeedback.InNP line 31
Source documentation
NP is defined independently of SAT or any hardness assertion.
Also declared: ComparatorChallenges/DirectedFeedback.lean:31 (same declaration text).
```
def InNP (language : List Bool → Prop) : Prop :=
…
```
structure OAI.DirectedFeedback.Digraph line 36
Source documentation
Finite loopless digraph. Opposite arcs are permitted. Every arc is listed explicitly. No symmetric closure or undirected-cycle convention is used.
Also declared: ComparatorChallenges/DirectedFeedback.lean:36 (same declaration text).
```
structure Digraph where
…
```
def OAI.DirectedFeedback.Digraph.IsCycle line 47
Source documentation
An actual simple directed cycle of positive length. A cyclic enumeration of r + 1 distinct vertices supplies every successive arc, including the closing arc. A 2-cycle is allowed; looplessness rules out length 1.
Also declared: ComparatorChallenges/DirectedFeedback.lean:47 (same declaration text).
```
def IsCycle (G : Digraph) {r : ℕ} (c : Fin (r + 1) → Fin G.n) : Prop :=
…
```
Mentions: OAI.DirectedFeedback.Digraph
def OAI.DirectedFeedback.Digraph.Feedback line 51
Source documentation
A feedback set intersects EVERY actual directed cycle.
Also declared: ComparatorChallenges/DirectedFeedback.lean:51 (same declaration text).
```
def Feedback (G : Digraph) (F : Finset (Fin G.n)) : Prop :=
…
```
Mentions: OAI.DirectedFeedback.Digraph
def OAI.DirectedFeedback.Digraph.dfvs line 56
Source documentation
Minimum number of vertices of a feedback set. No weights or auxiliary cost oracle appear in this definition.
Also declared: ComparatorChallenges/DirectedFeedback.lean:56 (same declaration text).
```
noncomputable def dfvs (G : Digraph) : ℕ := by
…
```
Mentions: OAI.DirectedFeedback.Digraph
def OAI.DirectedFeedback.Digraph.bits line 64
Source documentation
Full explicit vertex and arc serialization, including isolated vertices.
Also declared: ComparatorChallenges/DirectedFeedback.lean:64 (same declaration text).
```
def bits (G : Digraph) : List Bool :=
…
```
Mentions: OAI.DirectedFeedback.Digraph
structure OAI.DirectedFeedback.GapInstance line 71
Source documentation
Output includes a strictly positive integer threshold.
Also declared: ComparatorChallenges/DirectedFeedback.lean:71 (same declaration text).
```
structure GapInstance where
…
```
def OAI.DirectedFeedback.GapInstance.bits line 76
Also declared: ComparatorChallenges/DirectedFeedback.lean:76 (same declaration text).
structure OAI.DirectedFeedback.GapReduction line 81
Source documentation
A strict YES/NO gap reduction implemented by a finite-alphabet machine with polynomial runtime in the raw input bit length.
Also declared: ComparatorChallenges/DirectedFeedback.lean:81 (same declaration text).
```
structure GapReduction (A : ℝ) (language : List Bool → Prop) where
…
```
def OAI.DirectedFeedback.MainStatement line 92
Source documentation
Constant-factor directed feedback vertex set hardness for all NP languages.
Also declared: ComparatorChallenges/DirectedFeedback.lean:92 (same declaration text).
```
def MainStatement : Prop :=
…
```