sgl_clock_poly
DefinitionDefinition code
import Definitions.Def_sgl_power_uniform
import Definitions.Def_sgl_coeff
import Definitions.Def_sgl_seed
import Definitions.Def_sgl_tail
/-!
# The polynomial clock
Origin marker, seed, power, coefficient, tail: a clock of
`(N+1) + (κ+1)·(N+1)^d` marks over a blank with its head past them, the
inputs restored, and everything outside the seven roles untouched. `N`
bounds the delegate's total input length at every offset, so once `κ` and `d`
come from the delegate's polynomial bound the clock dominates its running
time — which is what the margin argument needs — and the tail keeps the size
conditions true at the low degrees the polynomial part cannot cover.
The power and coefficient machines have existentially quantified state
types, so the composite does too.
-/
namespace SipserGacsLautemann
variable {tapes : Nat}
/-- The state type of a machine, exposed for stepwise instance search: one
deep search over a fully nested composite fails, while one small search per
layer succeeds, because each layer sees the previous instance as a local
hypothesis rather than a subtree to recurse into. -/
@[reducible] def stateOf {S : Type} (_ : TypedMachine tapes S) : Type := S
set_option maxHeartbeats 4000000 in
set_option synthInstance.maxHeartbeats 4000000 in
set_option maxRecDepth 16000 in
/-- **The polynomial clock.** Roles: `idx 0‥2` the inputs, `idx 3` the seed,
`idx 4, 5` the ping-pong pair, `idx 6` the clock. -/
theorem clockPoly_exists (idx : Fin 7 → Fin tapes)
(hinj : Function.Injective idx) (κ d : Nat) :
∃ (S : Type) (_ : Fintype S) (M : TypedMachine tapes S),
∀ (T : Fin tapes → Tape) (x0 x1 x2 L0 L1 L2 R0 R1 R2 : List TapeSymbol),
(∀ c ∈ x0, c ≠ TapeSymbol.blank) →
(∀ c ∈ x1, c ≠ TapeSymbol.blank) →
(∀ c ∈ x2, c ≠ TapeSymbol.blank) →
T (idx 0) = cellsTape (TapeSymbol.blank :: L0)
(x0 ++ TapeSymbol.blank :: R0) →
T (idx 1) = cellsTape (TapeSymbol.blank :: L1)
(x1 ++ TapeSymbol.blank :: R1) →
T (idx 2) = cellsTape (TapeSymbol.blank :: L2)
(x2 ++ TapeSymbol.blank :: R2) →
T (idx 3) = cellsTape [] [] →
T (idx 4) = cellsTape [] [] →
T (idx 5) = cellsTape [] [] →
T (idx 6) = cellsTape [] [] →
∃ cost : Nat,
cost ≤ 110 * ((κ + 1) *
(x2.length + (x2.length + (x1.length + x0.length)) + 2)
^ (d + 1))
+ 30 * (x2.length + (x2.length + (x1.length + x0.length)) + 2)
+ 100 ∧
HaltsExactly M (M.startCfg T) cost true ∧
(((M.step^[cost]) (M.startCfg T)).tape) (idx 6) =
cellsTape (List.replicate
((x2.length + (x2.length + (x1.length + x0.length)) + 1)
+ (κ + 1) *
(x2.length + (x2.length + (x1.length + x0.length)) + 1)
^ d)
(TapeSymbol.bit true) ++ TapeSymbol.blank :: []) [] ∧
(((M.step^[cost]) (M.startCfg T)).tape) (idx 0) = T (idx 0) ∧
(((M.step^[cost]) (M.startCfg T)).tape) (idx 1) = T (idx 1) ∧
(((M.step^[cost]) (M.startCfg T)).tape) (idx 2) = T (idx 2) ∧
(∀ j, (∀ i : Fin 7, j ≠ idx i) →
(((M.step^[cost]) (M.startCfg T)).tape) j = T j) := by
classical
have hne : ∀ a b : Fin 7, a ≠ b → idx a ≠ idx b :=
fun a b hab h => hab (hinj h)
obtain ⟨SP, instP, MP, hMP⟩ := power_uniform (idx 3) (idx 4) (idx 5)
(hne 3 4 (by decide)) (hne 3 5 (by decide)) (hne 4 5 (by decide)) d
have hptc : pTape (idx 4) (idx 5) d ≠ idx 6 := by
rcases pTape_cases (idx 4) (idx 5) d with h | h <;> rw [h]
· exact hne 4 6 (by decide)
· exact hne 5 6 (by decide)
obtain ⟨SC, instC, MC, hMC⟩ := coeff_exists (pTape (idx 4) (idx 5) d)
(idx 6) hptc κ
letI := instP
letI := instC
refine ⟨_, ?_,
(prepTape (idx 6)).andThen fun _ =>
(seedSetup (idx 0) (idx 1) (idx 2) (idx 3)).andThen fun _ =>
MP.andThen fun _ =>
MC.andThen fun _ =>
tailSetup (idx 0) (idx 1) (idx 2) (idx 6),
?_⟩
· letI i5 : Fintype
(stateOf (tailSetup (idx 0) (idx 1) (idx 2) (idx 6))) :=
inferInstance
letI i4 : Fintype (stateOf (MC.andThen fun _ =>
tailSetup (idx 0) (idx 1) (idx 2) (idx 6))) := inferInstance
letI i3 : Fintype (stateOf (MP.andThen fun _ =>
MC.andThen fun _ =>
tailSetup (idx 0) (idx 1) (idx 2) (idx 6))) := inferInstance
letI iseed : Fintype
(stateOf (seedSetup (idx 0) (idx 1) (idx 2) (idx 3))) := inferInstance
letI i2 : Fintype
(stateOf ((seedSetup (idx 0) (idx 1) (idx 2) (idx 3)).andThen fun _ =>
MP.andThen fun _ =>
MC.andThen fun _ =>
tailSetup (idx 0) (idx 1) (idx 2) (idx 6))) := inferInstance
exact inferInstance
intro T x0 x1 x2 L0 L1 L2 R0 R1 R2 hn0 hn1 hn2 hx0 hx1 hx2 hsd ha hb hclk
set N := x2.length + (x2.length + (x1.length + x0.length)) with hN
obtain ⟨costP, hcostP, vP, hpP⟩ := hMP N
obtain ⟨vC, hpC⟩ := hMC
-- stage 0: the clock's origin marker
obtain ⟨g0, s0⟩ := prepTape_spec (idx 6) T [] hclk
set F0 := Function.update T (idx 6) (cellsTape [TapeSymbol.blank] [])
with hF0
have hF0v : ∀ j, j ≠ idx 6 → F0 j = T j := by
intro j hj
rw [hF0, Function.update_of_ne hj]
-- stage 1: the seed
obtain ⟨c1, hc1, g1, s1⟩ := seedSetup_spec (idx 0) (idx 1) (idx 2) (idx 3)
(hne 0 3 (by decide)) (hne 1 3 (by decide)) (hne 2 3 (by decide))
x0 x1 x2 L0 L1 L2 R0 R1 R2 F0 hn0 hn1 hn2
(by rw [hF0v _ (hne 0 6 (by decide))]; exact hx0)
(by rw [hF0v _ (hne 1 6 (by decide))]; exact hx1)
(by rw [hF0v _ (hne 2 6 (by decide))]; exact hx2)
(by rw [hF0v _ (hne 3 6 (by decide))]; exact hsd)
set F1 := Function.update F0 (idx 3)
(cellsTape [TapeSymbol.blank]
(List.replicate
(x2.length + (x2.length + (x1.length + (x0.length + 1))))
(TapeSymbol.bit true) ++ TapeSymbol.blank :: [])) with hF1
have hNN : x2.length + (x2.length + (x1.length + (x0.length + 1))) =
N + 1 := by omega
have hF1v : ∀ j, j ≠ idx 3 → j ≠ idx 6 → F1 j = T j := by
intro j hj3 hj6
rw [hF1, Function.update_of_ne hj3]
exact hF0v j hj6
have hF1sd : F1 (idx 3) = cellsTape (TapeSymbol.blank :: [])
(List.replicate (N + 1) (TapeSymbol.bit true) ++
TapeSymbol.blank :: []) := by
rw [hF1, Function.update_self, hNN]
-- stage 2: the power
obtain ⟨hg2, ⟨La, hFa⟩, ⟨Lb, hFb⟩, hFsd, hFo⟩ := hpP F1 [] []
hF1sd
(by rw [hF1v _ (hne 4 3 (by decide)) (hne 4 6 (by decide))]; exact ha)
(by rw [hF1v _ (hne 5 3 (by decide)) (hne 5 6 (by decide))]; exact hb)
set F2 := ((MP.step^[costP]) (MP.startCfg F1)).tape with hF2
have hF2v : ∀ j, j ≠ idx 3 → j ≠ idx 4 → j ≠ idx 5 → j ≠ idx 6 →
F2 j = T j := by
intro j hj3 hj4 hj5 hj6
rw [hFo j hj3 hj4 hj5]
exact hF1v j hj3 hj6
have hF2clk : F2 (idx 6) = cellsTape [TapeSymbol.blank] [] := by
rw [hFo _ (hne 6 3 (by decide)) (hne 6 4 (by decide))
(hne 6 5 (by decide)), hF1, Function.update_of_ne (hne 6 3 (by decide)),
hF0, Function.update_self]
-- stage 3: the coefficient
obtain ⟨costC, hcostC, hg3, hCs, hCclk, hCo⟩ := hpC F2 ((N + 1) ^ d) La
[TapeSymbol.blank] hFa hF2clk
set F3 := ((MC.step^[costC]) (MC.startCfg F2)).tape with hF3
have hjpt : ∀ j : Fin tapes, j ≠ idx 4 → j ≠ idx 5 →
j ≠ pTape (idx 4) (idx 5) d := by
intro j hj4 hj5
rcases pTape_cases (idx 4) (idx 5) d with h | h <;> rw [h]
· exact hj4
· exact hj5
have hF3v : ∀ j, j ≠ idx 3 → j ≠ idx 4 → j ≠ idx 5 → j ≠ idx 6 →
F3 j = T j := by
intro j hj3 hj4 hj5 hj6
rw [hCo j (hjpt j hj4 hj5) hj6]
exact hF2v j hj3 hj4 hj5 hj6
-- stage 4: the tail
obtain ⟨costT, hcT, g4, s4⟩ := tailSetup_spec (idx 0) (idx 1) (idx 2)
(idx 6) (hne 0 6 (by decide)) (hne 1 6 (by decide)) (hne 2 6 (by decide))
x0 x1 x2 L0 L1 L2 R0 R1 R2
(List.replicate ((κ + 1) * (N + 1) ^ d) (TapeSymbol.bit true) ++
[TapeSymbol.blank]) F3 hn0 hn1 hn2
(by rw [hF3v _ (hne 0 3 (by decide)) (hne 0 4 (by decide))
(hne 0 5 (by decide)) (hne 0 6 (by decide))]; exact hx0)
(by rw [hF3v _ (hne 1 3 (by decide)) (hne 1 4 (by decide))
(hne 1 5 (by decide)) (hne 1 6 (by decide))]; exact hx1)
(by rw [hF3v _ (hne 2 3 (by decide)) (hne 2 4 (by decide))
(hne 2 5 (by decide)) (hne 2 6 (by decide))]; exact hx2)
hCclk
-- the chain
have k4 := chainStepC hg3 rfl g4
have k3 := chainStepC hg2 rfl k4.1
have k2 := chainStepC g1 s1 k3.1
have k1 := chainStepC g0 s0 k2.1
have hIR : ∀ {S₁ S₂ : Type} (bb : Bool) (c : TypedConfiguration tapes S₂),
(TypedConfiguration.inRight (S₁ := S₁) bb c).tape = c.tape :=
fun _ _ => rfl
set E := (N + 2) ^ (d + 1) with hE
have hfin : ((((prepTape (idx 6)).andThen fun _ =>
(seedSetup (idx 0) (idx 1) (idx 2) (idx 3)).andThen fun _ =>
MP.andThen fun _ =>
MC.andThen fun _ =>
tailSetup (idx 0) (idx 1) (idx 2) (idx 6)).step^[
3 + 1 + (c1 + 1 + (costP + 1 + (costC + 1 + costT)))])
(((prepTape (idx 6)).andThen fun _ =>
(seedSetup (idx 0) (idx 1) (idx 2) (idx 3)).andThen fun _ =>
MP.andThen fun _ =>
MC.andThen fun _ =>
tailSetup (idx 0) (idx 1) (idx 2) (idx 6)).startCfg T)).tape =
Function.update F3 (idx 6)
(cellsTape (List.replicate
(x2.length + (x2.length + (x1.length + (x0.length + 1))))
(TapeSymbol.bit true) ++
(List.replicate ((κ + 1) * (N + 1) ^ d) (TapeSymbol.bit true) ++
[TapeSymbol.blank])) []) := by
rw [k1.2, hIR, k2.2, hIR, k3.2, hIR, k4.2, hIR]
exact s4
-- the arithmetic
have hℓE : (N + 1) ^ d ≤ E := by
rw [hE]
calc (N + 1) ^ d ≤ (N + 2) ^ d := Nat.pow_le_pow_left (by omega) d
_ ≤ (N + 2) ^ (d + 1) := Nat.pow_le_pow_right (by omega) (by omega)
have hE1 : 1 ≤ E := by
rw [hE]
exact Nat.one_le_pow _ _ (by omega)
have hcoeffle : (κ + 1) * (9 * (N + 1) ^ d + 11) ≤ (κ + 1) * (20 * E) :=
Nat.mul_le_mul_left (κ + 1) (by omega)
have hmulE : (κ + 1) * (20 * E) = 20 * ((κ + 1) * E) := by ring
have hEK : E ≤ (κ + 1) * E := Nat.le_mul_of_pos_left E (by omega)
refine ⟨_, by omega, k1.1, ?_, ?_, ?_, ?_, ?_⟩
· rw [hfin, Function.update_self, ← List.append_assoc,
← List.replicate_add, hNN]
· rw [hfin, Function.update_of_ne (hne 0 6 (by decide))]
exact hF3v _ (hne 0 3 (by decide)) (hne 0 4 (by decide))
(hne 0 5 (by decide)) (hne 0 6 (by decide))
· rw [hfin, Function.update_of_ne (hne 1 6 (by decide))]
exact hF3v _ (hne 1 3 (by decide)) (hne 1 4 (by decide))
(hne 1 5 (by decide)) (hne 1 6 (by decide))
· rw [hfin, Function.update_of_ne (hne 2 6 (by decide))]
exact hF3v _ (hne 2 3 (by decide)) (hne 2 4 (by decide))
(hne 2 5 (by decide)) (hne 2 6 (by decide))
· intro j hj
rw [hfin, Function.update_of_ne (hj 6)]
exact hF3v _ (hj 3) (hj 4) (hj 5) (hj 6)
end SipserGacsLautemann