Exact and bounded iteration of the numerical schedule #
The division-by-four transition agrees with the entropy formula up to the scheduled depth. A semiconjugacy transfers this fact to the string program. Complete iteration uses an explicit bound on every encoded state, supplied by the finite width theorem for the scheduled specialization.
theorem
Algebraic.Cutwidth.Extractor.Internal.scheduledBlockStateStep_iterate
(initial h Q E : ℕ)
{i : ℕ}
(level : i ≤ h)
:
(scheduledBlockStateStep E)^[i] (initial, recursiveBlockEntropy h Q 0) = (recursiveBlockWidth initial h Q E i, recursiveBlockEntropy h Q i)
theorem
Algebraic.Cutwidth.Extractor.Internal.scheduledBlockStateStepEval_encode
(E : ℕ)
(state : ℕ × ℕ)
:
scheduledBlockStateStepEval (encodeScheduledBlockState E state) = encodeScheduledBlockState E (scheduledBlockStateStep E state)
theorem
Algebraic.Cutwidth.Extractor.Internal.scheduledBlockStateStepEval_iterate
(E : ℕ)
(state : ℕ × ℕ)
(i : ℕ)
:
scheduledBlockStateStepEval^[i] (encodeScheduledBlockState E state) = encodeScheduledBlockState E ((scheduledBlockStateStep E)^[i] state)
theorem
Algebraic.Cutwidth.Extractor.Internal.scheduledBlockState_iterate_mem_FP
{initial entropy E count B : List Bool → ℕ}
(hinitial : Complexity.UnaryFn initial)
(hentropy : Complexity.UnaryFn entropy)
(hE : Complexity.UnaryFn E)
(hcount : Complexity.UnaryFn count)
(hB : Complexity.UnaryFn B)
(bounded :
∀ (z : List Bool),
∀ j ≤ count z,
((scheduledBlockStateStep (E z))^[j] (initial z, entropy z)).1 ≤ B z ∧ ((scheduledBlockStateStep (E z))^[j] (initial z, entropy z)).2 ≤ B z)
:
(fun (z : List Bool) =>
encodeScheduledBlockState (E z) ((scheduledBlockStateStep (E z))^[count z] (initial z, entropy z))) ∈ Complexity.FP
theorem
Algebraic.Cutwidth.Extractor.Internal.scheduledBlockState_mem_FP
{initial h Q E count : List Bool → ℕ}
(hinitial : Complexity.UnaryFn initial)
(hentropy : Complexity.UnaryFn fun (z : List Bool) => recursiveBlockEntropy (h z) (Q z) 0)
(hE : Complexity.UnaryFn E)
(hcount : Complexity.UnaryFn count)
(capacity : ∀ (z : List Bool), recursiveBlockEntropy (h z) (Q z) 0 ≤ initial z)
(budget :
∀ (z : List Bool),
3 * (24 * explicitCondenserBudget (initial z) (recursiveBlockEntropy (h z) (Q z) 0) (E z)) + 6 * E z ≤ 2 * Q z)
(levels : ∀ (z : List Bool), count z ≤ h z)
:
(fun (z : List Bool) =>
encodeScheduledBlockState (E z)
(recursiveBlockWidth (initial z) (h z) (Q z) (E z) (count z), recursiveBlockEntropy (h z) (Q z) (count z))) ∈ Complexity.FP
theorem
Algebraic.Cutwidth.Extractor.Internal.recursiveBlockEntropy_zero_unaryFn
{initial h Q : List Bool → ℕ}
(hinitial : Complexity.UnaryFn initial)
(hh : Complexity.UnaryFn h)
(hQ : Complexity.UnaryFn Q)
(capacity : ∀ (z : List Bool), recursiveBlockEntropy (h z) (Q z) 0 ≤ initial z)
:
Complexity.UnaryFn fun (z : List Bool) => recursiveBlockEntropy (h z) (Q z) 0