Construction 2

Lax470956.Construction2 · concepts/Lax470956/Construction2.lean · lax-470956

proven

Loading review…

Natural Language Statement

Definition

The scheduling instance built from a $(3,4)$ formula. Each variable gets two machines, one for each truth value, and one job spanning a fixed window of length $25$ . Each clause gets three machines, and each of its three literal occurrences gets three jobs: a unit job whose deadline $2(k+1) + 8h$ records which occurrence $k$ of its variable it is and which literal $h$ of its clause, flanked by two jobs filling the rest of the window.

The window is what makes the construction work. A variable job overlaps every job of every occurrence of its variable, so a schedule that places all of them must put the variable job on one of the two machines of its variable, and that choice is the truth value. The bounded number of occurrences of a variable is what keeps the window, and with it every processing time, bounded by an absolute constant.

Concept map

9 concepts

100%

Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A

Evidence

This concept declares 8 statements. Each proof establishes one of them relative to its assumptions.

Lean source view on GitHub

1	import Lax470956.Exact34Encoding
2	import Lax470956.InstanceEncoding
3	import Lax759944.RamPolytime
4	import Mathlib.Data.Finset.Lattice.Fold
5
6	/-!
7	---
8	title: Construction 2
9	type: definition
10	---
11	The scheduling instance built from a $(3,4)$ formula. Each variable gets two
12	machines, one for each truth value, and one job spanning a fixed window of length $25$ .
13	Each clause gets three machines, and each of its three literal occurrences gets three
14	jobs: a unit job whose deadline $2(k+1) + 8h$ records which occurrence $k$ of its
15	variable it is and which literal $h$ of its clause, flanked by two jobs filling the rest
16	of the window.
17
18	The window is what makes the construction work. A variable job overlaps every job of
19	every occurrence of its variable, so a schedule that places all of them must put the
20	variable job on one of the two machines of its variable, and that choice is the truth
21	value. The bounded number of occurrences of a variable is what keeps the window, and
22	with it every processing time, bounded by an absolute constant.
23
24	# Formalization notes
25
26	The construction is a total function on words, so that the map it induces is defined
27	everywhere and the statements about it need no side condition. A word that is not a
28	well-formed formula still produces an instance, because the deadline is clamped to
29	$[2, 24]$ — exactly the range it already occupies when the appearance index is below
30	four and the literal index below three. The clamp is therefore invisible on well-formed
31	input, and it is what discharges the two standing conventions $0 < p$ and $p \le d$
32	without a hypothesis.
33
34	Jobs and machines are numbered rather than tagged. Job $v$ for $v < V$ belongs to
35	variable $v$ ; job $V + 9c + 3h + s$ belongs to occurrence $h$ of clause $c$ , in slot
36	$s$ — the literal job for $s = 0$ and its two wrappers for $s = 1, 2$ . Machine $2v$ is
37	the true machine of variable $v$ and $2v + 1$ its false machine; machine
38	$2V + 3c + t$ is the $t$ -th machine of clause $c$ . The numbering is part of the
39	construction because an instance is something a machine is handed, and a word presents
40	its jobs in an order.
41	-/
42
43	namespace Lax470956.Construction2
44
45	open Lax470956.Scheduling Lax470956.Exact34Encoding
46
47	variable (x : List ℕ)
48
49	/-- The number of variables the word declares. -/
50	abbrev nVar : ℕ := varCount x
51
52	/-- The number of clauses the word declares. -/
53	abbrev nCla : ℕ := clauseCount x
54
55	/-- One job per variable and nine per clause. -/
56	def nJobs : ℕ := nVar x + 9 * nCla x
57
58	/-- Two machines per variable and three per clause. -/
59	def nMach : ℕ := 2 * nVar x + 3 * nCla x
60
61	/-- The deadline of the literal job of occurrence `h` of clause `c`, clamped to the
62	range `[2, 24]` it already lies in on a well-formed word. -/
63	def dl (c h : ℕ) : ℕ := min 24 (max 2 (2 * (litApp x c h + 1) + 8 * h))
64
65	lemma dl_ge (c h : ℕ) : 2 ≤ dl x c h := by
66	simp only [dl]; omega
67
68	lemma dl_le (c h : ℕ) : dl x c h ≤ 24 := by
69	simp only [dl]; omega
70
71	/-- On a well-formed word the clamp is inactive: the deadline is the formula's own
72	`2(k+1) + 8h`. -/
73	lemma dl_eq_of_lt {c h : ℕ} (happ : litApp x c h < 4) (hh : h < 3) :
74	dl x c h = 2 * (litApp x c h + 1) + 8 * h := by
75	simp only [dl]; omega
76
77	variable {x}
78
79	/-- The clause of job index `i` counted from the first clause job. -/
80	def cOf (i : ℕ) : ℕ := i / 9
81
82	/-- The literal of job index `i` counted from the first clause job. -/
83	def hOf (i : ℕ) : ℕ := i % 9 / 3
84
85	/-- The slot of job index `i` counted from the first clause job. -/
86	def sOf (i : ℕ) : ℕ := i % 3
87
88	variable (x)
89
90	/-- The processing time of job `j`. -/
91	def procOf (j : ℕ) : ℕ :=
92	if j < nVar x then 25
93	else
94	match sOf (j - nVar x) with
95	\| 0 => 1
96	\| 1 => dl x (cOf (j - nVar x)) (hOf (j - nVar x)) - 1
97	\| _ => 25 - dl x (cOf (j - nVar x)) (hOf (j - nVar x))
98
99	/-- The deadline of job `j`. -/
100	def dueOf (j : ℕ) : ℕ :=
101	if j < nVar x then 25
102	else
103	match sOf (j - nVar x) with
104	\| 0 => dl x (cOf (j - nVar x)) (hOf (j - nVar x))
105	\| 1 => dl x (cOf (j - nVar x)) (hOf (j - nVar x)) - 1
106	\| _ => 25
107
108	/-- The machines eligible to run job `j`, as a list of machine numbers. -/
109	def eligOf (j : ℕ) : List ℕ :=
110	if j < nVar x then [2 * j, 2 * j + 1]
111	else
112	let i := j - nVar x
113	let base := 2 * nVar x + 3 * cOf i
114	match sOf i with
115	\| 0 => [base + 1, base + 2,
116	2 * litVar x (cOf i) (hOf i) + (if litSign x (cOf i) (hOf i) = 1 then 0 else 1)]
117	\| _ => [base, base + 1, base + 2]
118
119	lemma procOf_pos (j : ℕ) : 0 < procOf x j := by
120	unfold procOf
121	split
122	· omega
123	· have h1 := dl_ge x (cOf (j - nVar x)) (hOf (j - nVar x))
124	have h2 := dl_le x (cOf (j - nVar x)) (hOf (j - nVar x))
125	match hs : sOf (j - nVar x) with
126	\| 0 => simp
127	\| 1 => simp <;> omega
128	\| (k + 2) => simp <;> omega
129
130	lemma procOf_le_dueOf (j : ℕ) : procOf x j ≤ dueOf x j := by
131	unfold procOf dueOf
132	split
133	· omega
134	· have h1 := dl_ge x (cOf (j - nVar x)) (hOf (j - nVar x))
135	have h2 := dl_le x (cOf (j - nVar x)) (hOf (j - nVar x))
136	match hs : sOf (j - nVar x) with
137	\| 0 => simp <;> omega
138	\| 1 => simp
139	\| (k + 2) => simp <;> omega
140
141	lemma procOf_le_25 (j : ℕ) : procOf x j ≤ 25 := by
142	unfold procOf
143	split
144	· omega
145	· have h1 := dl_ge x (cOf (j - nVar x)) (hOf (j - nVar x))
146	have h2 := dl_le x (cOf (j - nVar x)) (hOf (j - nVar x))
147	match hs : sOf (j - nVar x) with
148	\| 0 => simp
149	\| 1 => simp <;> omega
150	\| (k + 2) => simp <;> omega
151
152	/-- Construction 2. The scheduling instance built from the word `x`. -/
153	def inst : Instance where
154	jobs := nJobs x
155	machines := nMach x
156	p j := procOf x j
157	d j := dueOf x j
158	w _ := 1
159	eligible j := Finset.univ.filter fun i : Fin (nMach x) => (i : ℕ) ∈ eligOf x j
160	p_pos j := procOf_pos x j
161	p_le_d j := procOf_le_dueOf x j
162
163	@[simp] lemma inst_jobs : (inst x).jobs = nJobs x := rfl
164	@[simp] lemma inst_machines : (inst x).machines = nMach x := rfl
165	@[simp] lemma inst_p (j : Fin (nJobs x)) : (inst x).p j = procOf x j := rfl
166	@[simp] lemma inst_d (j : Fin (nJobs x)) : (inst x).d j = dueOf x j := rfl
167
168
169	/-- Where job `j`'s block of eligible machines begins. -/
170	def offOf (j : ℕ) : ℕ :=
171	if j ≤ nVar x then 2 * j else 2 * nVar x + 3 * (j - nVar x)
172
173	/-- The processing-time block. -/
174	def procBlock : List ℕ := (List.range (nJobs x)).map (procOf x)
175
176	/-- The deadline block. -/
177	def dueBlock : List ℕ := (List.range (nJobs x)).map (dueOf x)
178
179	/-- The weight block: every job has weight one. -/
180	def wtBlock : List ℕ := List.replicate (nJobs x) 1
181
182	/-- The offset block, one entry per job and one more. -/
183	def offBlock : List ℕ := (List.range (nJobs x + 1)).map (offOf x)
184
185	/-- The target block: the eligible machines of each job in turn. -/
186	def tgtBlock : List ℕ := (List.range (nJobs x)).flatMap (eligOf x)
187
188	/-- The word Construction 2 emits. -/
189	def emit : List ℕ :=
190	[nJobs x, nMach x] ++ procBlock x ++ dueBlock x ++ wtBlock x ++ offBlock x ++ tgtBlock x
191
192	/-- The word a malformed input is sent to: one job, no machine, so its only job cannot
193	be scheduled. -/
194	def noWord : List ℕ := [1, 0, 1, 1, 1, 0, 0]
195
196	/-- Construction 2 as a total map on words. A word that is not a well-formed formula
197	is sent to a fixed instance that cannot schedule every job. A reduction is a function on
198	all words, and the machine that computes it has to decide which case it is in; making the
199	diversion part of the map rather than a side condition is what keeps the statement below
200	free of hypotheses.
201
202	The case split is on a proposition rather than on a decision procedure, so the map is
203	`noncomputable` in Lean. Nothing is lost: what has to be computable is the machine
204	program, and the statement that one computes this map is `reduce_computesInTime`. -/
205	noncomputable def reduce (x : List ℕ) : List ℕ :=
206	open Classical in
207	if Lax470956.Exact34Encoding.WellFormed x then emit x else noWord
208
209	/-- Every weight of the constructed instance is `1`. -/
210	axiom weights_one (x : List ℕ) (j : Fin (inst x).jobs) : (inst x).w j = 1
211
212	/-- Every processing time of the constructed instance is at most `25`. -/
213	axiom pmax_le (x : List ℕ) : (inst x).pmax ≤ 25
214
215	/-- Construction 2 is correct. A well-formed `(3,4)` formula is satisfiable
216	exactly when every job of the instance it builds can be scheduled. -/
217	axiom correct (x : List ℕ) (hwf : Lax470956.Exact34Encoding.WellFormed x) :
218	(∃ τ, Lax470956.Exact34Encoding.Satisfies x τ) ↔ (inst x).AllSchedulable
219
220	/-- The emitted word encodes the constructed instance. -/
221	axiom emit_encodes (x : List ℕ) (hwf : Lax470956.Exact34Encoding.WellFormed x) :
222	Lax470956.InstanceEncoding.EncodesInstance (emit x) (inst x)
223
224	/-- The reduction is correct. A word is a satisfiable `(3,4)` formula exactly
225	when the instance it is sent to can schedule every job. -/
226	axiom reduce_correct (x : List ℕ) :
227	x ∈ Lax470956.Exact34Encoding.Satisfiable ↔
228	∃ I, Lax470956.InstanceEncoding.EncodesInstance (reduce x) I ∧ I.AllSchedulable
229
230	/-- The reduction lands in the bounded slice. Every instance it emits has processing
231	times at most `25` and unit weights. -/
232	axiom reduce_slice (x : List ℕ) :
233	∃ I, Lax470956.InstanceEncoding.EncodesInstance (reduce x) I ∧
234	I.pmax ≤ 25 ∧ ∀ j, I.w j = 1
235
236	open Lax759944.RamPolytime in
237	/-- The reduction runs in polynomial time. One word RAM program computes the map on
238	every word — well-formed or not — within a polynomial number of instructions in the bit
239	size of its input.
240
241	This is the running-time half of the reduction, and it is the half the hardness
242	statements need, so it is stated in their currency: `Lax759944.RamPolytime` measures the
243	input by its bit size rather than by the number of entries, hands the machine the input
244	preceded by its length, and is proved in that submission to be interchangeable with
245	polynomial time on a Turing machine. The statement about the emitter alone,
246	`emit_computesInTime`, is the same claim in the archive's word-RAM currency and on
247	well-formed input only; it is the part of this one that does the work, and deciding
248	well-formedness is what the rest of it adds.
249
250	Deciding well-formedness is not a formality. The condition that distinct occurrences of
251	one variable carry distinct appearance indices is a disjointness condition on `3C`
252	pairs, and it is decidable in one pass only because the pairs live in a universe of size
253	`4V`: an occurrence is bucketed at `4v + k`, and a bucket claimed twice refutes it. -/
254	axiom reduce_ramPolytime : RamPolytime reduce
255
256	open Lax808846.Ram Lax808846.RamComputes Lax470956.ParameterizedComplexity in
257	/-- Construction 2 runs in linear time. One word RAM program and one constant `c`
258	such that, at every word length, on every well-formed formula whose entries fit, the
259	program halts within `c · (\|x\| + 1)` instructions having written `emit x`. -/
260	axiom emit_computesInTime :
261	∃ (prog : Program) (c : ℕ), ∀ w : ℕ,
262	ComputesInTime w prog
263	{y \| Lax470956.Exact34Encoding.WellFormed y ∧ Fits c w y}
264	emit (fun y => c * (y.length + 1))
265
266	end Lax470956.Construction2
267

Show ProofShow ProofShow ProofShow ProofShow ProofShow ProofShow ProofShow Proof

Formalization notes

The construction is a total function on words, so that the map it induces is defined everywhere and the statements about it need no side condition. A word that is not a well-formed formula still produces an instance, because the deadline is clamped to $[2, 24]$ — exactly the range it already occupies when the appearance index is below four and the literal index below three. The clamp is therefore invisible on well-formed input, and it is what discharges the two standing conventions $0 < p$ and $p \le d$ without a hypothesis.

Jobs and machines are numbered rather than tagged. Job $v$ for $v < V$ belongs to variable $v$ ; job $V + 9c + 3h + s$ belongs to occurrence $h$ of clause $c$ , in slot $s$ — the literal job for $s = 0$ and its two wrappers for $s = 1, 2$ . Machine $2v$ is the true machine of variable $v$ and $2v + 1$ its false machine; machine $2V + 3c + t$ is the $t$ -th machine of clause $c$ . The numbering is part of the construction because an instance is something a machine is handed, and a word presents its jobs in an order.

Builds on

Used by

none

From Mathlib

Mathlib.Data.Finset.Lattice.Fold

Discussion

Ask a question or add context. Endorsements and structured flags are kept in the review panel above.

Loading discussion…

Lax Lean Archive

Construction 2

Flags

Flag this concept

Natural Language Statement

Definition

1 `correct` proven

2 `emit_computesInTime` proven

3 `emit_encodes` proven

4 `pmax_le` proven

5 `reduce_correct` proven

6 `reduce_ramPolytime` proven

7 `reduce_slice` proven

8 `weights_one` proven

Lean source view on GitHub

Discussion

Settings