Partition problem

AbbreviationPARTITION instance as a list of naturals#✓fully proved

A partition instance: a list of natural numbers.

abbrev PartitionInstance := List ℕ

Used by 4

Used byBinary-coded PARTITION decision problem · Binary PARTITION decider is correct on canonical encodings · Feasibility of a PARTITION instance · Correctness of the encoded PARTITION to SUBSET-SUM reduction

DefinitionFeasibility of a PARTITION instance#✓fully proved

A sublist summing to half the total.

def PartitionFeasible (i : PartitionInstance) : Prop :=
  ∃ s : List ℕ, s.Sublist i ∧ s.sum * 2 = i.sum

Uses 1 · Used by 6

Statement usesPARTITION instance as a list of naturals

Used byPARTITION as SUBSET-SUM on the doubled list · Correctness of the SUBSET-SUM to PARTITION padding map · Binary-coded PARTITION decision problem · Binary PARTITION decider is correct on canonical encodings · Correctness of the encoded SUBSET-SUM to PARTITION reduction · Correctness of the encoded PARTITION to SUBSET-SUM reduction

DefinitionBinary-coded PARTITION decision problem#✓fully proved

PARTITION using the canonical binary list decoder; bad framing rejects.

noncomputable def partitionDec : ComplexityTheory.DecisionProblem := fun x =>
  match BitstringEncoding.bitDecode (α := PartitionInstance) x with
  | some i => decide (PartitionFeasible i)
  | none => false

Uses 11 · Used by 6

Statement usesBitstring encodings · Decoding function of a bitstring encoding · Decoding inverts bitstring encoding · Encoding function of a bitstring encoding · Self-delimiting form of a bitstring · Parsing one self-delimiting block · Parsing a list of booleans into self-delimiting blocks · Bounded parsing of self-delimiting blocks · Feasibility of a PARTITION instance · PARTITION instance as a list of naturals · Decision problems

Used byBinary PARTITION decider is correct on canonical encodings · Binary-coded PARTITION is in NP · PARTITION is NP-complete · Correctness of the encoded SUBSET-SUM to PARTITION reduction · Correctness of the encoded PARTITION to SUBSET-SUM reduction · Polynomial-time reduction from SUBSET-SUM to PARTITION

TheoremBinary PARTITION decider is correct on canonical encodings#✓fully proved

A canonical encoding has exactly the intended feasibility semantics.

@[simp] theorem partitionDec_bitEncode (as : List ℕ) :
    partitionDec (BitstringEncoding.bitEncode as) = true ↔
      PartitionFeasible as

Uses 11 · Used by 1

Statement usesBitstring encodings · Decoding function of a bitstring encoding · Decoding inverts bitstring encoding · Encoding function of a bitstring encoding · Self-delimiting form of a bitstring · Parsing one self-delimiting block · Parsing a list of booleans into self-delimiting blocks · Bounded parsing of self-delimiting blocks · Feasibility of a PARTITION instance · Binary-coded PARTITION decision problem

Proof usesPARTITION instance as a list of naturals

Used byCorrectness of the encoded SUBSET-SUM to PARTITION reduction

DefinitionPadding map from SUBSET-SUM to PARTITION#✓fully proved

The two padding entries in the SUBSET-SUM reduction. No subtraction or range check is needed, even when t > as.sum.

def fromSubsetSum (as : List ℕ) (t : ℕ) : List ℕ :=
  as.sum :: (2 * t) :: as

Used by 7

Used byCorrectness of the SUBSET-SUM to PARTITION padding map · Padding reduction has linear output length · Encoded reduction from SUBSET-SUM to PARTITION · Correctness of the encoded SUBSET-SUM to PARTITION reduction · Encoded SUBSET-SUM to PARTITION map has linear output length · Quadratic run of the raw-input SUBSET-SUM to PARTITION machine · Quadratic run of the padding machine on canonical instances

TheoremCorrectness of the SUBSET-SUM to PARTITION padding map#✓fully proved

SUBSET-SUM reduces to PARTITION by adding two nonnegative entries.

theorem fromSubsetSum_feasible (as : List ℕ) (t : ℕ) :
    PartitionFeasible (fromSubsetSum as t) ↔
      ∃ s : List ℕ, s.Sublist as ∧ s.sum = t

Uses 2 · Used by 1

Statement usesFeasibility of a PARTITION instance · Padding map from SUBSET-SUM to PARTITION

Used byCorrectness of the encoded SUBSET-SUM to PARTITION reduction

TheoremPARTITION as SUBSET-SUM on the doubled list#✓fully proved

Doubling each entry reduces PARTITION membership to SUBSET-SUM without truncating division on odd totals.

theorem feasible_iff_doubled_sublist (as : List ℕ) :
    PartitionFeasible as ↔ ∃ s : List ℕ,
      s.Sublist (as.map (· * 2)) ∧ s.sum = as.sum

Uses 1 · Used by 1

Statement usesFeasibility of a PARTITION instance

Used byCorrectness of the encoded PARTITION to SUBSET-SUM reduction

InductiveScan phases of the PARTITION doubling pass#✓fully proved

Reading the first marker, a later marker, or a payload bit.

inductive Phase | start | marker | payload
  deriving DecidableEq

Used by 17

Used byOutput bits per input bit in the doubling pass · PARTITION doubling machine as a host component · Raw-input PARTITION membership machine as a host component · Canonical PARTITION membership transducer as a host component · Label map from the doubling halt to the prefix emitter · Membership transducer embeds the doubling machine · Membership transducer embeds the summation machine · PARTITION doubling pass is polynomial-time · Control labels of the PARTITION doubling machine · Phase transition of the PARTITION doubling pass · Program of the PARTITION doubling machine · Linear step bound for the PARTITION doubling machine · Canonical PARTITION membership transducer runs in quadratic time · Label map from summation halts to the doubling pass · Finite-state doubling pass on raw bitstrings · Doubling pass maps a number block to the block of its double · Doubling pass doubles every number in a list

DefinitionPhase transition of the PARTITION doubling pass#✓fully proved

Phase after reading one input bit.

def next : Phase → Bool → Phase
  | .payload, _ => .marker
  | _, b => if b then .payload else .start

Uses 1 · Used by 5

Statement usesScan phases of the PARTITION doubling pass

Used byMembership transducer embeds the doubling machine · Program of the PARTITION doubling machine · Linear step bound for the PARTITION doubling machine · Finite-state doubling pass on raw bitstrings · Doubling pass maps a number block to the block of its double

DefinitionOutput bits per input bit in the doubling pass#✓fully proved

Output bits for one input bit; at a nonzero block prepend its low zero.

def chunk : Phase → Bool → List Bool
  | .start, true => [true, false, true]
  | _, b => [b]

Uses 1 · Used by 5

Statement usesScan phases of the PARTITION doubling pass

Used byMembership transducer embeds the doubling machine · Program of the PARTITION doubling machine · Linear step bound for the PARTITION doubling machine · Finite-state doubling pass on raw bitstrings · Doubling pass maps a number block to the block of its double

DefinitionFinite-state doubling pass on raw bitstrings#✓fully proved

The raw finite-state pass. Malformed strings have a total output too; validation belongs to the preceding canonical decoder.

def transform : Phase → List Bool → List Bool
  | _, [] => []
  | q, b :: x => chunk q b ++ transform (next q b) x

Uses 3 · Used by 5

Statement usesScan phases of the PARTITION doubling pass · Output bits per input bit in the doubling pass · Phase transition of the PARTITION doubling pass

Used byPARTITION doubling pass is polynomial-time · Linear step bound for the PARTITION doubling machine · Canonical PARTITION membership transducer runs in quadratic time · Doubling pass maps a number block to the block of its double · Doubling pass doubles every number in a list

TheoremDoubling pass maps a number block to the block of its double#✓fully proved

A canonical number block becomes the canonical block of its double.

theorem transform_block (n : ℕ) (rest : List Bool) :
    transform .start (delimit (encodeNat n) ++ rest) =
      delimit (encodeNat (n * 2)) ++ transform .start rest

Uses 6 · Used by 1

Statement usesSelf-delimiting form of a bitstring · Scan phases of the PARTITION doubling pass · Finite-state doubling pass on raw bitstrings

Proof usesOutput bits per input bit in the doubling pass · Phase transition of the PARTITION doubling pass · Binary encoding, least significant bit first

Used byDoubling pass doubles every number in a list

TheoremDoubling pass doubles every number in a list#✓fully proved

The stream pass doubles every number and preserves list multiplicity.

theorem transform_nums (as : List ℕ) :
    transform .start (as.flatMap fun n => delimit (encodeNat n)) =
      (as.map (· * 2)).flatMap fun n => delimit (encodeNat n)

Uses 4 · Used by 1

Statement usesSelf-delimiting form of a bitstring · Scan phases of the PARTITION doubling pass · Finite-state doubling pass on raw bitstrings

Proof usesDoubling pass maps a number block to the block of its double

Used byCanonical PARTITION membership transducer runs in quadratic time

InductiveStacks of the PARTITION doubling machine#✓fully proved

Input, reversed output, and output stacks of the doubling pass.

inductive K | X | R | O
  deriving DecidableEq

Used by 17

Used byPARTITION doubling machine as a host component · Raw-input PARTITION membership machine as a host component · Canonical PARTITION membership transducer as a host component · Doubling-machine stack embedding in the membership transducer · Membership transducer embeds the doubling machine · Membership transducer embeds the summation machine · PARTITION to SUBSET-SUM map is polynomial-time · PARTITION doubling pass is polynomial-time · Stacks of the canonical PARTITION membership transducer · Program of the PARTITION doubling machine · Program of the raw-input PARTITION membership machine · Program of the canonical PARTITION membership transducer · Linear step bound for the PARTITION doubling machine · Raw-input PARTITION membership machine runs in quadratic time · Canonical PARTITION membership transducer runs in quadratic time · Summation-machine stack embedding in the membership transducer · Stack alphabets of the canonical PARTITION membership transducer

InductiveControl labels of the PARTITION doubling machine#✓fully proved

Three scan phases followed by reversal and a halting continuation.

inductive Lab | scan (q : Phase) | emit | done
  deriving DecidableEq

Uses 1 · Used by 15

Statement usesScan phases of the PARTITION doubling pass

Used byPARTITION doubling machine as a host component · Raw-input PARTITION membership machine as a host component · Canonical PARTITION membership transducer as a host component · Label map from the doubling halt to the prefix emitter · Membership transducer embeds the doubling machine · Membership transducer embeds the summation machine · PARTITION doubling pass is polynomial-time · Control labels of the canonical PARTITION membership transducer · Program of the PARTITION doubling machine · Program of the raw-input PARTITION membership machine · Program of the canonical PARTITION membership transducer · Linear step bound for the PARTITION doubling machine · Raw-input PARTITION membership machine runs in quadratic time · Canonical PARTITION membership transducer runs in quadratic time · Label map from summation halts to the doubling pass

DefinitionProgram of the PARTITION doubling machine#✓fully proved

Finite-stack implementation of transform.

def prog : Lab → TM2.Stmt (fun _ : K => Bool) Lab Bool
  | .scan q =>
    .peek .X (fun _ o => o.isNone) <| .branch id
      (.goto fun _ => .emit)
      (.pop .X (fun _ o => o.getD false) <| .branch id
        (TM2Program.emit .R (chunk q true) (.scan (next q true)))
        (TM2Program.emit .R (chunk q false) (.scan (next q false))))
  | .emit => moveB .R .O some id .emit .done
  | .done => .halt

Uses 8 · Used by 8

Statement usesStacks of the PARTITION doubling machine · Control labels of the PARTITION doubling machine · Scan phases of the PARTITION doubling pass · Output bits per input bit in the doubling pass · Phase transition of the PARTITION doubling pass · Flag bit of a machine state · Pushing a constant list · Bit-moving loop

Used byPARTITION doubling machine as a host component · Membership transducer embeds the doubling machine · Membership transducer embeds the summation machine · PARTITION doubling pass is polynomial-time · Program of the canonical PARTITION membership transducer · Linear step bound for the PARTITION doubling machine · Raw-input PARTITION membership machine runs in quadratic time · Canonical PARTITION membership transducer runs in quadratic time

TheoremLinear step bound for the PARTITION doubling machine#✓fully proved

The complete pass takes at most 4 * input.length + 2 steps.

theorem run (x : List Bool) (v₀ : Bool := false) :
    ∃ v S', RunLe prog (4 * x.length + 2)
      ⟨some (.scan .start), v₀, update (fun _ => []) .X x⟩
      ⟨some .done, v, S'⟩ ∧ S' .O = transform .start x

Uses 15 · Used by 2

Statement usesStacks of the PARTITION doubling machine · Control labels of the PARTITION doubling machine · Scan phases of the PARTITION doubling pass · Program of the PARTITION doubling machine · Finite-state doubling pass on raw bitstrings · Runs within a step budget

Proof usesOutput bits per input bit in the doubling pass · Phase transition of the PARTITION doubling pass · Flag bit of a machine state · Exact-length runs of a TM2 machine · A single step executes the statement at the current label · Bit on top of a stack · Pushing a constant list · Bit test for the top of a stack · Pushing a list of symbols onto one stack

Used byPARTITION doubling pass is polynomial-time · Canonical PARTITION membership transducer runs in quadratic time

AbbreviationPARTITION doubling machine as a host component#✓fully proved

The doubling transducer as a finite component for the canonical host.

abbrev comp : Cslib.Complexity.Host.Comp where
  K := K
  Γ := fun _ => Bool
  L := Lab
  prog := prog
  ks := [.X, .R, .O]
  ks_nodup := by decide
  mem_ks k := by cases k <;> simp

Uses 5 · Used by 1

Statement usesComponent machine · Stacks of the PARTITION doubling machine · Control labels of the PARTITION doubling machine · Scan phases of the PARTITION doubling pass · Program of the PARTITION doubling machine

Used byPARTITION doubling pass is polynomial-time

TheoremPARTITION doubling pass is polynomial-time#✓fully proved

Polynomial time in the canonical bitstring encoding, from the actual finite-state machine, including malformed raw strings.

theorem isPolyTime_transform : ComplexityTheory.IsPolyTime (transform .start)

Uses 19

Statement usesBitstring encodings · Decoding function of a bitstring encoding · Decoding inverts bitstring encoding · Encoding function of a bitstring encoding · Self-delimiting form of a bitstring · Parsing one self-delimiting block · Parsing a list of booleans into self-delimiting blocks · Bounded parsing of self-delimiting blocks · Scan phases of the PARTITION doubling pass · Finite-state doubling pass on raw bitstrings · Polynomial-time computable functions

Proof usesComponent machine · Reduction host, canonical form · Stacks of the PARTITION doubling machine · Control labels of the PARTITION doubling machine · PARTITION doubling machine as a host component · Program of the PARTITION doubling machine · Linear step bound for the PARTITION doubling machine · Runs within a step budget

DefinitionEncoded reduction from SUBSET-SUM to PARTITION#✓fully proved

SUBSET-SUM to PARTITION, with malformed inputs sent to [1].

def reduceFromSubsetSum (x : List Bool) : List Bool :=
  match SSVerify.decodeSS x with
  | some (as, t) => bitEncode (fromSubsetSum as t)
  | none => bitEncode ([1] : List ℕ)

Uses 10 · Used by 5

Statement usesDecoding a SUBSET-SUM instance · Bitstring encodings · Decoding function of a bitstring encoding · Decoding inverts bitstring encoding · Encoding function of a bitstring encoding · Self-delimiting form of a bitstring · Parsing one self-delimiting block · Parsing a list of booleans into self-delimiting blocks · Bounded parsing of self-delimiting blocks · Padding map from SUBSET-SUM to PARTITION

Used bySUBSET-SUM to PARTITION map is polynomial-time · Correctness of the encoded SUBSET-SUM to PARTITION reduction · Encoded SUBSET-SUM to PARTITION map has linear output length · Quadratic run of the raw-input SUBSET-SUM to PARTITION machine · Polynomial-time reduction from SUBSET-SUM to PARTITION

DefinitionEncoded reduction from PARTITION to SUBSET-SUM#✓fully proved

PARTITION to SUBSET-SUM, preserving the generic decoder's semantics.

def reduceToSubsetSum (x : List Bool) : List Bool :=
  match bitDecode (α := List ℕ) x with
  | some as => encodeSS (as.map (· * 2)) as.sum
  | none => noSS

Uses 10 · Used by 4

Statement usesBit-string encoding of SUBSET-SUM instances · Fixed no-instance of SUBSET-SUM · Bitstring encodings · Decoding function of a bitstring encoding · Decoding inverts bitstring encoding · Encoding function of a bitstring encoding · Self-delimiting form of a bitstring · Parsing one self-delimiting block · Parsing a list of booleans into self-delimiting blocks · Bounded parsing of self-delimiting blocks

Used byPARTITION to SUBSET-SUM map is polynomial-time · Binary-coded PARTITION is in NP · Correctness of the encoded PARTITION to SUBSET-SUM reduction · Raw-input PARTITION membership machine runs in quadratic time

TheoremCorrectness of the encoded SUBSET-SUM to PARTITION reduction#✓fully proved

The encoded reduction preserves every yes/no answer, including malformed source strings. This is the semantic, not the time, theorem.

theorem reduceFromSubsetSum_correct (x : List Bool) :
    subsetSumDec x = partitionDec (reduceFromSubsetSum x)

Uses 18 · Used by 1

Statement usesThe SUBSET-SUM problem · Binary-coded PARTITION decision problem · Encoded reduction from SUBSET-SUM to PARTITION

Proof usesDecoding a SUBSET-SUM instance · Decoding a SUBSET-SUM instance inverts its encoding · Bit-string encoding of SUBSET-SUM instances · Bitstring encodings · Decoding function of a bitstring encoding · Decoding inverts bitstring encoding · Encoding function of a bitstring encoding · Self-delimiting form of a bitstring · Parsing one self-delimiting block · Parsing a list of booleans into self-delimiting blocks · Bounded parsing of self-delimiting blocks · Feasibility of a PARTITION instance · Padding map from SUBSET-SUM to PARTITION · Correctness of the SUBSET-SUM to PARTITION padding map · Binary PARTITION decider is correct on canonical encodings

Used byPolynomial-time reduction from SUBSET-SUM to PARTITION

TheoremCorrectness of the encoded PARTITION to SUBSET-SUM reduction#✓fully proved

The membership map preserves the generic decoder, including accepted noncanonical payloads and rejected malformed framing.

theorem reduceToSubsetSum_correct (x : List Bool) :
    partitionDec x = subsetSumDec (reduceToSubsetSum x)

Uses 17 · Used by 1

Statement usesThe SUBSET-SUM problem · Binary-coded PARTITION decision problem · Encoded reduction from PARTITION to SUBSET-SUM

Proof usesBit-string encoding of SUBSET-SUM instances · Fixed no-instance of SUBSET-SUM · The fixed no-instance of SUBSET-SUM · Bitstring encodings · Decoding function of a bitstring encoding · Decoding inverts bitstring encoding · Encoding function of a bitstring encoding · Self-delimiting form of a bitstring · Parsing one self-delimiting block · Parsing a list of booleans into self-delimiting blocks · Bounded parsing of self-delimiting blocks · Feasibility of a PARTITION instance · PARTITION instance as a list of naturals · PARTITION as SUBSET-SUM on the doubled list

Used byBinary-coded PARTITION is in NP

TheoremBitlength of a PARTITION sum is at most the encoded length#✓fully proved

Summing a binary PARTITION instance cannot exceed its encoded length.

theorem sum_encoding_length_le (as : List ℕ) :
    (encodeNat as.sum).length ≤ (bitEncode as).length

Uses 12 · Used by 4

Statement usesBitstring encodings · Decoding function of a bitstring encoding · Decoding inverts bitstring encoding · Encoding function of a bitstring encoding · Self-delimiting form of a bitstring · Parsing one self-delimiting block · Parsing a list of booleans into self-delimiting blocks · Bounded parsing of self-delimiting blocks

Proof usesRipple-carry addition of bit lists · Addition is correct on canonical numbers · Carry bit of a full adder · Adding a carry bit

Used byPadding reduction has linear output length · Quadratic run of the padding machine on canonical instances · Canonical PARTITION membership transducer runs in quadratic time · PARTITION membership instance has linear bitlength

TheoremPadding reduction has linear output length#✓fully proved

The padding reduction has linear output length in its encoded input.

theorem fromSubsetSum_length (as : List ℕ) (t : ℕ) :
    (bitEncode (fromSubsetSum as t)).length ≤
      3 * (encodeSS as t).length + 1

Uses 15 · Used by 1

Statement usesBit-string encoding of SUBSET-SUM instances · Bitstring encodings · Decoding function of a bitstring encoding · Decoding inverts bitstring encoding · Encoding function of a bitstring encoding · Self-delimiting form of a bitstring · Parsing one self-delimiting block · Parsing a list of booleans into self-delimiting blocks · Bounded parsing of self-delimiting blocks · Padding map from SUBSET-SUM to PARTITION

Proof usesRipple-carry addition of bit lists · Addition is correct on canonical numbers · Carry bit of a full adder · Adding a carry bit · Bitlength of a PARTITION sum is at most the encoded length

Used byEncoded SUBSET-SUM to PARTITION map has linear output length

TheoremEncoded SUBSET-SUM to PARTITION map has linear output length#✓fully proved

Linear output bound on all strings, including malformed encodings.

theorem reduceFromSubsetSum_length (x : List Bool) :
    (reduceFromSubsetSum x).length ≤ 3 * x.length + 3

Uses 14

Statement usesEncoded reduction from SUBSET-SUM to PARTITION

Proof usesDecoding a SUBSET-SUM instance · Decoding a SUBSET-SUM instance inverts its encoding · Bit-string encoding of SUBSET-SUM instances · Bitstring encodings · Decoding function of a bitstring encoding · Decoding inverts bitstring encoding · Encoding function of a bitstring encoding · Self-delimiting form of a bitstring · Parsing one self-delimiting block · Parsing a list of booleans into self-delimiting blocks · Bounded parsing of self-delimiting blocks · Padding map from SUBSET-SUM to PARTITION · Padding reduction has linear output length

TheoremPARTITION membership instance has linear bitlength#✓fully proved

Linear bitlength bound for the membership instance.

theorem toSubsetSum_length (as : List ℕ) :
    (encodeSS (as.map (· * 2)) as.sum).length ≤
      5 * (bitEncode as).length + 1

Uses 14

Statement usesBit-string encoding of SUBSET-SUM instances · Bitstring encodings · Decoding function of a bitstring encoding · Decoding inverts bitstring encoding · Encoding function of a bitstring encoding · Self-delimiting form of a bitstring · Parsing one self-delimiting block · Parsing a list of booleans into self-delimiting blocks · Bounded parsing of self-delimiting blocks

Proof usesRipple-carry addition of bit lists · Addition is correct on canonical numbers · Carry bit of a full adder · Adding a carry bit · Bitlength of a PARTITION sum is at most the encoded length

InductiveStacks of the SUBSET-SUM to PARTITION padding machine#✓fully proved

Input, reverse buffer, target, output, and unchanged sum-machine stacks.

inductive K | X | R | T | O | sum (k : SSVerify.K)
  deriving DecidableEq

Uses 1 · Used by 10

Statement usesStacks of the SUBSET-SUM verifier

Used byRaw-input SUBSET-SUM to PARTITION machine as a host component · SUBSET-SUM to PARTITION padding machine as a host component · Padding machine embeds the summation machine · SUBSET-SUM to PARTITION map is polynomial-time · Stacks of the raw-input SUBSET-SUM to PARTITION machine · Program of the raw-input SUBSET-SUM to PARTITION machine · Program of the SUBSET-SUM to PARTITION padding machine · Quadratic run of the raw-input SUBSET-SUM to PARTITION machine · Quadratic run of the padding machine on canonical instances · Summation-machine stack embedding in the padding machine

InductiveControl labels of the SUBSET-SUM to PARTITION padding machine#✓fully proved

Parse target, preserve numbers, sum, then emit the two padding blocks.

inductive Lab
  | target | copy | distribute | sum (l : SSVerify.Lab)
  | targetStart | targetBits | prefix | bits | done
  deriving DecidableEq

Uses 1 · Used by 9

Statement usesLabels of the SUBSET-SUM verifier

Used byRaw-input SUBSET-SUM to PARTITION machine as a host component · SUBSET-SUM to PARTITION padding machine as a host component · Padding machine embeds the summation machine · Control labels of the raw-input SUBSET-SUM to PARTITION machine · Program of the raw-input SUBSET-SUM to PARTITION machine · Program of the SUBSET-SUM to PARTITION padding machine · Quadratic run of the raw-input SUBSET-SUM to PARTITION machine · Quadratic run of the padding machine on canonical instances · Label map from summation halts to target emission

DefinitionSummation-machine stack embedding in the padding machine#✓fully proved

The original sum component's stacks are not reimplemented.

def sumEmb : SEmb (fun _ : SSVerify.K => Sym) Γ where
  e := K.sum
  inj _ _ h := K.sum.inj h
  ι _ := Equiv.refl _

Uses 4 · Used by 4

Statement usesStacks of the SUBSET-SUM verifier · Stack alphabet of the SAT verifier · Stacks of the SUBSET-SUM to PARTITION padding machine · Stack embedding

Used byPadding machine embeds the summation machine · Program of the SUBSET-SUM to PARTITION padding machine · Quadratic run of the raw-input SUBSET-SUM to PARTITION machine · Quadratic run of the padding machine on canonical instances

DefinitionLabel map from summation halts to target emission#✓fully proved

Both genuine sum-machine halts resume at target emission.

def sumLabel : SSVerify.Lab → Lab
  | .yes | .no => .targetStart
  | l => .sum l

Uses 2 · Used by 4

Statement usesLabels of the SUBSET-SUM verifier · Control labels of the SUBSET-SUM to PARTITION padding machine

Used byPadding machine embeds the summation machine · Program of the SUBSET-SUM to PARTITION padding machine · Quadratic run of the raw-input SUBSET-SUM to PARTITION machine · Quadratic run of the padding machine on canonical instances

DefinitionProgram of the SUBSET-SUM to PARTITION padding machine#✓fully proved

Padding construction by binary stack operations.

MetaMathlibExt.Complexity.NPComplete.Partition.HardnessCore.prog · 32 lines

def prog : Lab → TM2.Stmt Γ Lab Bool
  | .target =>
    .pop .X (fun _ o => o.getD false) <| .branch id
      (.pop .X (fun _ o => o.getD false) <| .push .T id <|
        .goto fun _ => .target)
      (.goto fun _ => .copy)
  | .copy => moveB .X .R some id .copy .distribute
  | .distribute =>
    .peek .R (fun _ o => o.isNone) <| .branch id
      (.goto fun _ => .sum .next)
      (.pop .R (fun _ o => o.getD false) <|
        .push (.sum .X) Sym.bit <| .push .O id <|
        .push (.sum .W) (fun _ => .bit true) <|
        .goto fun _ => .distribute)
  | .sum l => mapS sumEmb sumLabel (SSVerify.prog l)
  | .targetStart =>
    .push .O (fun _ => false) <| .peek .T (fun _ o => o.isNone) <|
      .branch id (.goto fun _ => .prefix) (.goto fun _ => .targetBits)
  | .targetBits =>
    .peek .T (fun _ o => o.isNone) <| .branch id
      (.push .O (fun _ => false) <| .push .O (fun _ => true) <|
        .goto fun _ => .prefix)
      (.pop .T (fun _ o => o.getD false) <|
        .push .O id <| .push .O (fun _ => true) <|
        .goto fun _ => .targetBits)
  | .prefix => .push .O (fun _ => false) <| .goto fun _ => .bits
  | .bits =>
    .peek (.sum .B) (fun _ o => o.isNone) <| .branch id
      (.goto fun _ => .done)
      (.pop (.sum .B) (fun _ o => bitOf Sym.bit? o) <|
        .push .O id <| .push .O (fun _ => true) <| .goto fun _ => .bits)
  | .done => .halt

Uses 13 · Used by 5

Statement usesStacks of the SUBSET-SUM verifier · Labels of the SUBSET-SUM verifier · The SUBSET-SUM verifier program · Stack alphabet of the SAT verifier · Reading a symbol as a name bit · Stacks of the SUBSET-SUM to PARTITION padding machine · Control labels of the SUBSET-SUM to PARTITION padding machine · Summation-machine stack embedding in the padding machine · Label map from summation halts to target emission · Translating a statement along a stack embedding · Flag bit of a machine state · Bit on top of a stack · Bit-moving loop

Used bySUBSET-SUM to PARTITION padding machine as a host component · Padding machine embeds the summation machine · Program of the raw-input SUBSET-SUM to PARTITION machine · Quadratic run of the raw-input SUBSET-SUM to PARTITION machine · Quadratic run of the padding machine on canonical instances

TheoremPadding machine embeds the summation machine#✓fully proved

The host changes only the two original halting continuations.

theorem embeds_sum : Embeds sumEmb sumLabel SSVerify.prog prog

Uses 19 · Used by 1

Statement usesStacks of the SUBSET-SUM verifier · Labels of the SUBSET-SUM verifier · The SUBSET-SUM verifier program · Stack alphabet of the SAT verifier · Stacks of the SUBSET-SUM to PARTITION padding machine · Control labels of the SUBSET-SUM to PARTITION padding machine · Program of the SUBSET-SUM to PARTITION padding machine · Summation-machine stack embedding in the padding machine · Label map from summation halts to target emission · Embedding of a machine in a host

Proof usesAdding one payload bit to the sum · Carry step of the SUBSET-SUM verifier · Starting the next number · Reading one pair of a block · Reading a symbol as a name bit · Translating a statement along a stack embedding · Flag bit of a machine state · Bit-block comparison statement · Bit-moving loop

Used byQuadratic run of the padding machine on canonical instances

TheoremQuadratic run of the padding machine on canonical instances#✓fully proved

The subtraction-free padding map is computed by a quadratic binary machine on every canonical SUBSET-SUM instance, including t > as.sum.

theorem run (as : List ℕ) (t : ℕ) :
    ∃ v S, RunLe prog (20 * ((encodeSS as t).length + 1) ^ 2)
      ⟨some .target, false, update (fun _ => []) .X (encodeSS as t)⟩
      ⟨some .done, v, S⟩ ∧ S .O = bitEncode (fromSubsetSum as t)

Uses 35 · Used by 1

Statement usesStacks of the SUBSET-SUM verifier · Bit-string encoding of SUBSET-SUM instances · Stack alphabet of the SAT verifier · Bitstring encodings · Decoding function of a bitstring encoding · Decoding inverts bitstring encoding · Encoding function of a bitstring encoding · Self-delimiting form of a bitstring · Parsing one self-delimiting block · Parsing a list of booleans into self-delimiting blocks · Bounded parsing of self-delimiting blocks · Stacks of the SUBSET-SUM to PARTITION padding machine · Control labels of the SUBSET-SUM to PARTITION padding machine · Program of the SUBSET-SUM to PARTITION padding machine · Padding map from SUBSET-SUM to PARTITION · Runs within a step budget

Proof usesLabels of the SUBSET-SUM verifier · Numbers chosen by a mask · Stack contents of the SUBSET-SUM verifier · A long enough all-true mask selects the whole list · Embedded SUBSET-SUM summing component reaches the mapped label · Reading a symbol as a name bit · Padding machine embeds the summation machine · Summation-machine stack embedding in the padding machine · Label map from summation halts to target emission · Bitlength of a PARTITION sum is at most the encoded length · Agreement of host and sub-machine stacks · Frame condition for a stack embedding · Stack embedding · Flag bit of a machine state · Exact-length runs of a TM2 machine · A single step executes the statement at the current label · Bit on top of a stack · Running the bit-moving loop · Binary encoding, least significant bit first

Used byQuadratic run of the raw-input SUBSET-SUM to PARTITION machine

AbbreviationSUBSET-SUM to PARTITION padding machine as a host component#✓fully proved

Finite padding component for the strict source-decoding wrapper.

noncomputable abbrev comp : Cslib.Complexity.Host.Comp where
  K := K
  Γ := Γ
  finΓ k := by cases k <;> infer_instance
  L := Lab
  prog := prog
  ks := Finset.univ.toList
  ks_nodup := Finset.nodup_toList _
  mem_ks k := by simp

Uses 7 · Used by 1

Statement usesComponent machine · Stacks of the SUBSET-SUM verifier · Labels of the SUBSET-SUM verifier · Stack alphabet of the SAT verifier · Stacks of the SUBSET-SUM to PARTITION padding machine · Control labels of the SUBSET-SUM to PARTITION padding machine · Program of the SUBSET-SUM to PARTITION padding machine

Used byRaw-input SUBSET-SUM to PARTITION machine as a host component

InductiveStacks of the raw-input SUBSET-SUM to PARTITION machine#✓fully proved

Disjoint workspaces, a preserved input, and comparison scratch stacks.

inductive K
  | norm (k : ListNatMachine.K) | core (k : HardnessCore.K)
  | raw | buffer | left | right
  deriving DecidableEq

Uses 2 · Used by 4

Statement usesStacks of the list-of-naturals canonicalizer · Stacks of the SUBSET-SUM to PARTITION padding machine

Used byRaw-input SUBSET-SUM to PARTITION machine as a host component · SUBSET-SUM to PARTITION map is polynomial-time · Program of the raw-input SUBSET-SUM to PARTITION machine · Quadratic run of the raw-input SUBSET-SUM to PARTITION machine

InductiveControl labels of the raw-input SUBSET-SUM to PARTITION machine#✓fully proved

Copy, exact normalization, canonicality check, and numeric computation.

inductive Lab
  | copy1 | copy2 | norm (l : ListNatMachine.Lab) | nonempty | compare
  | restore | start | core (l : HardnessCore.Lab) | bad | done
  deriving DecidableEq

Uses 2 · Used by 4

Statement usesControl labels of the list-of-naturals canonicalizer · Control labels of the SUBSET-SUM to PARTITION padding machine

Used byRaw-input SUBSET-SUM to PARTITION machine as a host component · SUBSET-SUM to PARTITION map is polynomial-time · Program of the raw-input SUBSET-SUM to PARTITION machine · Quadratic run of the raw-input SUBSET-SUM to PARTITION machine

DefinitionProgram of the raw-input SUBSET-SUM to PARTITION machine#✓fully proved

A total finite-stack transducer for the exact source codec.

def prog : Lab → TM2.Stmt Γ Lab Bool
  | .copy1 => moveB .raw .buffer some id .copy1 .copy2
  | .copy2 => splitB .buffer .raw (.norm .input) some id id .copy2 (.norm .loop)
  | .norm l => mapS normEmb normLabel (ListNatMachine.prog l)
  | .nonempty => .peek (.norm .output) (fun _ o => o.isSome) <|
      .branch id (.goto fun _ => .compare) (.goto fun _ => .bad)
  | .compare => cmpB .raw (.norm .output) .left .right some some id id
      .compare .restore .bad
  | .restore => moveB .left (.core .X) some id .restore .start
  | .start => .load (fun _ => false) <| .goto fun _ => .core .target
  | .core l => mapS coreEmb coreLabel (HardnessCore.prog l)
  | .bad => emitR (.core .O) (bitEncode ([1] : List ℕ)) .done
  | .done => .halt

Uses 27 · Used by 3

Statement usesControl labels of the payload normalizer machine · Stacks of the SUBSET-SUM verifier · Labels of the SUBSET-SUM verifier · Stacks of the list-of-naturals canonicalizer · Control labels of the list-of-naturals canonicalizer · Program of the list-of-naturals canonicalizer · Two-destination bit-block transfer · Stack alphabet of the SAT verifier · Bitstring encodings · Decoding function of a bitstring encoding · Decoding inverts bitstring encoding · Encoding function of a bitstring encoding · Self-delimiting form of a bitstring · Parsing one self-delimiting block · Parsing a list of booleans into self-delimiting blocks · Bounded parsing of self-delimiting blocks · Stacks of the SUBSET-SUM to PARTITION padding machine · Control labels of the SUBSET-SUM to PARTITION padding machine · Program of the SUBSET-SUM to PARTITION padding machine · Stacks of the raw-input SUBSET-SUM to PARTITION machine · Control labels of the raw-input SUBSET-SUM to PARTITION machine · Stack embedding · Translating a statement along a stack embedding · Flag bit of a machine state · Bit-block comparison statement · Prepending a constant list · Bit-moving loop

Used byRaw-input SUBSET-SUM to PARTITION machine as a host component · SUBSET-SUM to PARTITION map is polynomial-time · Quadratic run of the raw-input SUBSET-SUM to PARTITION machine

TheoremQuadratic run of the raw-input SUBSET-SUM to PARTITION machine#✓fully proved

Total raw-input hardness reduction, with exact source rejection and an explicit bound polynomial in encoded length, not numeric magnitude.

theorem run (x : List Bool) :
    ∃ v S, RunLe prog (60 * (x.length + 1) ^ 2)
      ⟨some .copy1, false, update (fun _ => []) .raw x⟩
      ⟨some .done, v, S⟩ ∧ S (.core .O) = reduceFromSubsetSum x

Uses 62 · Used by 1

Statement usesStacks of the payload normalizer machine · Stacks of the SUBSET-SUM verifier · Stacks of the list-of-naturals canonicalizer · Stack alphabet of the SAT verifier · Stacks of the SUBSET-SUM to PARTITION padding machine · Stacks of the raw-input SUBSET-SUM to PARTITION machine · Control labels of the raw-input SUBSET-SUM to PARTITION machine · Program of the raw-input SUBSET-SUM to PARTITION machine · Encoded reduction from SUBSET-SUM to PARTITION · Runs within a step budget

Proof usesMachine step reading one framed payload pair · Control labels of the payload normalizer machine · Program of the payload normalizer machine · Stack contents for the payload normalizer invariant · Labels of the SUBSET-SUM verifier · Decoding a SUBSET-SUM instance · Decoding a SUBSET-SUM instance inverts its encoding · The SUBSET-SUM verifier program · Bit-string encoding of SUBSET-SUM instances · Control labels of the list-of-naturals canonicalizer · Stack embedding of the number normalizer in the list canonicalizer · Label embedding of the number normalizer in the list canonicalizer · Program of the list-of-naturals canonicalizer · Embedded list canonicalizer preserves outside stacks · Workspace layout of the list-of-naturals canonicalizer · Bit-block copy keeps the order and restores source and scratch · Reversed self-delimiting frame emitter · Reading a symbol as a name bit · Bitstring encodings · Decoding function of a bitstring encoding · Decoding inverts bitstring encoding · Encoding function of a bitstring encoding · Self-delimiting form of a bitstring · Parsing one self-delimiting block · Parsing a list of booleans into self-delimiting blocks · Bounded parsing of self-delimiting blocks · Control labels of the SUBSET-SUM to PARTITION padding machine · Program of the SUBSET-SUM to PARTITION padding machine · Quadratic run of the padding machine on canonical instances · Summation-machine stack embedding in the padding machine · Label map from summation halts to target emission · Padding map from SUBSET-SUM to PARTITION · Agreement of host and sub-machine stacks · Embedding of a machine in a host · Frame condition for a stack embedding · Stack embedding · Translating a statement along a stack embedding · Run embedding for bounded runs · Four pairwise distinct stacks · Flag bit of a machine state · Exact-length runs of a TM2 machine · A single step executes the statement at the current label · Bit on top of a stack · Bit-block comparison statement · Deciding step of the comparison · Comparison pops a common prefix · Correctness of the bit-block comparison · Pushing a constant list · Prepending a constant list · Bit-moving loop · Running the bit-moving loop · Pushing a list of symbols onto one stack

Used bySUBSET-SUM to PARTITION map is polynomial-time

AbbreviationRaw-input SUBSET-SUM to PARTITION machine as a host component#✓fully proved

The all-string hardness reduction in the existing finite host.

noncomputable abbrev comp : Cslib.Complexity.Host.Comp where
  K := K
  Γ := Γ
  finΓ k := by
    cases k with
    | norm _ | raw | buffer | left | right => infer_instance
    | core k => exact HardnessCore.comp.finΓ k
  L := Lab
  prog := prog
  ks := Finset.univ.toList
  ks_nodup := Finset.nodup_toList _
  mem_ks k := by simp

Uses 14 · Used by 1

Statement usesStacks of the payload normalizer machine · Control labels of the payload normalizer machine · Component machine · Stacks of the SUBSET-SUM verifier · Labels of the SUBSET-SUM verifier · Stacks of the list-of-naturals canonicalizer · Control labels of the list-of-naturals canonicalizer · Stack alphabet of the SAT verifier · Stacks of the SUBSET-SUM to PARTITION padding machine · Control labels of the SUBSET-SUM to PARTITION padding machine · SUBSET-SUM to PARTITION padding machine as a host component · Stacks of the raw-input SUBSET-SUM to PARTITION machine · Control labels of the raw-input SUBSET-SUM to PARTITION machine · Program of the raw-input SUBSET-SUM to PARTITION machine

Used bySUBSET-SUM to PARTITION map is polynomial-time

TheoremSUBSET-SUM to PARTITION map is polynomial-time#✓fully proved

The total SUBSET-SUM-to-PARTITION map is polynomial-time.

theorem isPolyTime_reduceFromSubsetSum : ComplexityTheory.IsPolyTime
    reduceFromSubsetSum

Uses 23 · Used by 1

Statement usesBitstring encodings · Decoding function of a bitstring encoding · Decoding inverts bitstring encoding · Encoding function of a bitstring encoding · Self-delimiting form of a bitstring · Parsing one self-delimiting block · Parsing a list of booleans into self-delimiting blocks · Bounded parsing of self-delimiting blocks · Encoded reduction from SUBSET-SUM to PARTITION · Polynomial-time computable functions

Proof usesStacks of the payload normalizer machine · Component machine · Reduction host, canonical form · Stacks of the SUBSET-SUM verifier · Stacks of the list-of-naturals canonicalizer · Stack alphabet of the SAT verifier · Stacks of the SUBSET-SUM to PARTITION padding machine · Stacks of the raw-input SUBSET-SUM to PARTITION machine · Control labels of the raw-input SUBSET-SUM to PARTITION machine · Raw-input SUBSET-SUM to PARTITION machine as a host component · Program of the raw-input SUBSET-SUM to PARTITION machine · Quadratic run of the raw-input SUBSET-SUM to PARTITION machine · Runs within a step budget

Used byPolynomial-time reduction from SUBSET-SUM to PARTITION

InductiveStacks of the canonical PARTITION membership transducer#✓fully proved

Input, reversal buffer, and the two embedded components' stacks.

inductive K | X | R | sum (k : SSVerify.K) | double (k : DoubleStream.K)
  deriving DecidableEq

Uses 2 · Used by 15

Statement usesStacks of the SUBSET-SUM verifier · Stacks of the PARTITION doubling machine

Used byRaw-input PARTITION membership machine as a host component · Canonical PARTITION membership transducer as a host component · Numeric-core workspace of the raw-input PARTITION membership machine · Doubling-machine stack embedding in the membership transducer · Membership transducer embeds the doubling machine · Membership transducer embeds the summation machine · PARTITION to SUBSET-SUM map is polynomial-time · Stacks of the raw-input PARTITION membership machine · Normalizer workspace of the raw-input PARTITION membership machine · Program of the raw-input PARTITION membership machine · Program of the canonical PARTITION membership transducer · Raw-input PARTITION membership machine runs in quadratic time · Canonical PARTITION membership transducer runs in quadratic time · Summation-machine stack embedding in the membership transducer · Stack alphabets of the canonical PARTITION membership transducer

DefinitionStack alphabets of the canonical PARTITION membership transducer#✓fully proved

The summation stacks use the existing verifier alphabet.

@[reducible] def Γ : K → Type
  | .sum _ => Sym
  | _ => Bool

Uses 4 · Used by 13

Statement usesStacks of the SUBSET-SUM verifier · Stack alphabet of the SAT verifier · Stacks of the PARTITION doubling machine · Stacks of the canonical PARTITION membership transducer

Used byRaw-input PARTITION membership machine as a host component · Canonical PARTITION membership transducer as a host component · Numeric-core workspace of the raw-input PARTITION membership machine · Doubling-machine stack embedding in the membership transducer · Membership transducer embeds the doubling machine · Membership transducer embeds the summation machine · PARTITION to SUBSET-SUM map is polynomial-time · Normalizer workspace of the raw-input PARTITION membership machine · Program of the raw-input PARTITION membership machine · Program of the canonical PARTITION membership transducer · Raw-input PARTITION membership machine runs in quadratic time · Canonical PARTITION membership transducer runs in quadratic time · Summation-machine stack embedding in the membership transducer

InductiveControl labels of the canonical PARTITION membership transducer#✓fully proved

Component phases and the final sum-prefix emitter.

inductive Lab
  | copy | distribute | sum (l : SSVerify.Lab)
  | double (l : DoubleStream.Lab) | prefix | bits | done
  deriving DecidableEq

Uses 2 · Used by 11

Statement usesLabels of the SUBSET-SUM verifier · Control labels of the PARTITION doubling machine

Used byRaw-input PARTITION membership machine as a host component · Canonical PARTITION membership transducer as a host component · Label map from the doubling halt to the prefix emitter · Membership transducer embeds the doubling machine · Membership transducer embeds the summation machine · Control labels of the raw-input PARTITION membership machine · Program of the raw-input PARTITION membership machine · Program of the canonical PARTITION membership transducer · Raw-input PARTITION membership machine runs in quadratic time · Canonical PARTITION membership transducer runs in quadratic time · Label map from summation halts to the doubling pass

DefinitionSummation-machine stack embedding in the membership transducer#✓fully proved

Stack embedding of the existing sum component.

def sumEmb : SEmb (fun _ : SSVerify.K => Sym) Γ where
  e := K.sum
  inj _ _ h := K.sum.inj h
  ι _ := Equiv.refl _

Uses 6 · Used by 4

Statement usesStacks of the SUBSET-SUM verifier · Stack alphabet of the SAT verifier · Stacks of the PARTITION doubling machine · Stacks of the canonical PARTITION membership transducer · Stack alphabets of the canonical PARTITION membership transducer · Stack embedding

Used byMembership transducer embeds the summation machine · Program of the canonical PARTITION membership transducer · Raw-input PARTITION membership machine runs in quadratic time · Canonical PARTITION membership transducer runs in quadratic time

DefinitionDoubling-machine stack embedding in the membership transducer#✓fully proved

Stack embedding of the doubling component.

def doubleEmb : SEmb (fun _ : DoubleStream.K => Bool) Γ where
  e := K.double
  inj _ _ h := K.double.inj h
  ι _ := Equiv.refl _

Uses 5 · Used by 5

Statement usesStacks of the SUBSET-SUM verifier · Stacks of the PARTITION doubling machine · Stacks of the canonical PARTITION membership transducer · Stack alphabets of the canonical PARTITION membership transducer · Stack embedding

Used byMembership transducer embeds the doubling machine · Membership transducer embeds the summation machine · Program of the canonical PARTITION membership transducer · Raw-input PARTITION membership machine runs in quadratic time · Canonical PARTITION membership transducer runs in quadratic time

DefinitionLabel map from summation halts to the doubling pass#✓fully proved

Both sum halts resume at the doubling pass.

def sumLabel : SSVerify.Lab → Lab
  | .yes | .no => .double (.scan .start)
  | l => .sum l

Uses 4 · Used by 4

Statement usesLabels of the SUBSET-SUM verifier · Control labels of the PARTITION doubling machine · Scan phases of the PARTITION doubling pass · Control labels of the canonical PARTITION membership transducer

Used byMembership transducer embeds the summation machine · Program of the canonical PARTITION membership transducer · Raw-input PARTITION membership machine runs in quadratic time · Canonical PARTITION membership transducer runs in quadratic time

DefinitionLabel map from the doubling halt to the prefix emitter#✓fully proved

The doubling halt resumes at the prefix emitter.

def doubleLabel : DoubleStream.Lab → Lab
  | .done => .prefix
  | l => .double l

Uses 3 · Used by 5

Statement usesControl labels of the PARTITION doubling machine · Scan phases of the PARTITION doubling pass · Control labels of the canonical PARTITION membership transducer

Used byMembership transducer embeds the doubling machine · Membership transducer embeds the summation machine · Program of the canonical PARTITION membership transducer · Raw-input PARTITION membership machine runs in quadratic time · Canonical PARTITION membership transducer runs in quadratic time

DefinitionProgram of the canonical PARTITION membership transducer#✓fully proved

Copy, sum, double, and prepend the sum, using finite-stack operations.

MetaMathlibExt.Complexity.NPComplete.Partition.MembershipCore.prog · 20 lines

def prog : Lab → TM2.Stmt Γ Lab Bool
  | .copy => moveB .X .R some id .copy .distribute
  | .distribute =>
    .peek .R (fun _ o => o.isNone) <| .branch id
      (.goto fun _ => .sum .next)
      (.pop .R (fun _ o => o.getD false) <|
        .push (.sum .X) Sym.bit <| .push (.double .X) id <|
        .push (.sum .W) (fun _ => .bit true) <|
        .goto fun _ => .distribute)
  | .sum l => mapS sumEmb sumLabel (SSVerify.prog l)
  | .double l => mapS doubleEmb doubleLabel (DoubleStream.prog l)
  | .prefix =>
    .push (.double .O) (fun _ => false) <| .goto fun _ => .bits
  | .bits =>
    .peek (.sum .B) (fun _ o => o.isNone) <| .branch id
      (.goto fun _ => .done)
      (.pop (.sum .B) (fun _ o => bitOf Sym.bit? o) <|
        .push (.double .O) id <| .push (.double .O) (fun _ => true) <|
        .goto fun _ => .bits)
  | .done => .halt

Uses 19 · Used by 6

Statement usesStacks of the SUBSET-SUM verifier · Labels of the SUBSET-SUM verifier · The SUBSET-SUM verifier program · Stack alphabet of the SAT verifier · Reading a symbol as a name bit · Stacks of the PARTITION doubling machine · Control labels of the PARTITION doubling machine · Program of the PARTITION doubling machine · Stacks of the canonical PARTITION membership transducer · Control labels of the canonical PARTITION membership transducer · Doubling-machine stack embedding in the membership transducer · Label map from the doubling halt to the prefix emitter · Summation-machine stack embedding in the membership transducer · Label map from summation halts to the doubling pass · Stack alphabets of the canonical PARTITION membership transducer · Translating a statement along a stack embedding · Flag bit of a machine state · Bit on top of a stack · Bit-moving loop

Used byCanonical PARTITION membership transducer as a host component · Membership transducer embeds the doubling machine · Membership transducer embeds the summation machine · Program of the raw-input PARTITION membership machine · Raw-input PARTITION membership machine runs in quadratic time · Canonical PARTITION membership transducer runs in quadratic time

TheoremMembership transducer embeds the summation machine#✓fully proved

Only genuine halts are replaced when embedding the sum machine.

theorem embeds_sum : Embeds sumEmb sumLabel SSVerify.prog prog

Uses 26 · Used by 1

Statement usesStacks of the SUBSET-SUM verifier · Labels of the SUBSET-SUM verifier · The SUBSET-SUM verifier program · Stack alphabet of the SAT verifier · Stacks of the canonical PARTITION membership transducer · Control labels of the canonical PARTITION membership transducer · Program of the canonical PARTITION membership transducer · Summation-machine stack embedding in the membership transducer · Label map from summation halts to the doubling pass · Stack alphabets of the canonical PARTITION membership transducer · Embedding of a machine in a host

Proof usesAdding one payload bit to the sum · Carry step of the SUBSET-SUM verifier · Starting the next number · Reading one pair of a block · Reading a symbol as a name bit · Stacks of the PARTITION doubling machine · Control labels of the PARTITION doubling machine · Scan phases of the PARTITION doubling pass · Program of the PARTITION doubling machine · Doubling-machine stack embedding in the membership transducer · Label map from the doubling halt to the prefix emitter · Translating a statement along a stack embedding · Flag bit of a machine state · Bit-block comparison statement · Bit-moving loop

Used byCanonical PARTITION membership transducer runs in quadratic time

TheoremMembership transducer embeds the doubling machine#✓fully proved

Only the doubling halt is replaced by the prefix-emitter continuation.

theorem embeds_double :
    Embeds doubleEmb doubleLabel DoubleStream.prog prog

Uses 17 · Used by 1

Statement usesStacks of the PARTITION doubling machine · Control labels of the PARTITION doubling machine · Program of the PARTITION doubling machine · Stacks of the canonical PARTITION membership transducer · Control labels of the canonical PARTITION membership transducer · Doubling-machine stack embedding in the membership transducer · Label map from the doubling halt to the prefix emitter · Program of the canonical PARTITION membership transducer · Stack alphabets of the canonical PARTITION membership transducer · Embedding of a machine in a host

Proof usesScan phases of the PARTITION doubling pass · Output bits per input bit in the doubling pass · Phase transition of the PARTITION doubling pass · Translating a statement along a stack embedding · Flag bit of a machine state · Pushing a constant list · Bit-moving loop

Used byCanonical PARTITION membership transducer runs in quadratic time

TheoremCanonical PARTITION membership transducer runs in quadratic time#✓fully proved

The canonical PARTITION membership map is computed in quadratic time by summing, doubling, and prefixing, with no value-sized loop.

theorem run (as : List ℕ) :
    let r := as.flatMap fun a =>
      BitstringEncoding.delimit (Computability.encodeNat a)
    ∃ v S, RunLe prog (r.length * (2 * r.length + 14) + 9)
      ⟨some .copy, false, update (fun _ => []) .X r⟩
      ⟨some .done, v, S⟩ ∧
      S (.double .O) = encodeSS (as.map (· * 2)) as.sum

Uses 45 · Used by 1

Statement usesStacks of the SUBSET-SUM verifier · Bit-string encoding of SUBSET-SUM instances · Self-delimiting form of a bitstring · Stacks of the PARTITION doubling machine · Stacks of the canonical PARTITION membership transducer · Control labels of the canonical PARTITION membership transducer · Program of the canonical PARTITION membership transducer · Stack alphabets of the canonical PARTITION membership transducer · Runs within a step budget

Proof usesLabels of the SUBSET-SUM verifier · Numbers chosen by a mask · Stack contents of the SUBSET-SUM verifier · A long enough all-true mask selects the whole list · Embedded SUBSET-SUM summing component reaches the mapped label · Stack alphabet of the SAT verifier · Reading a symbol as a name bit · Bitstring encodings · Decoding function of a bitstring encoding · Decoding inverts bitstring encoding · Encoding function of a bitstring encoding · Parsing one self-delimiting block · Parsing a list of booleans into self-delimiting blocks · Bounded parsing of self-delimiting blocks · Control labels of the PARTITION doubling machine · Scan phases of the PARTITION doubling pass · Program of the PARTITION doubling machine · Linear step bound for the PARTITION doubling machine · Finite-state doubling pass on raw bitstrings · Doubling pass doubles every number in a list · Doubling-machine stack embedding in the membership transducer · Label map from the doubling halt to the prefix emitter · Membership transducer embeds the doubling machine · Membership transducer embeds the summation machine · Summation-machine stack embedding in the membership transducer · Label map from summation halts to the doubling pass · Bitlength of a PARTITION sum is at most the encoded length · Agreement of host and sub-machine stacks · Frame condition for a stack embedding · Stack embedding · Run embedding for bounded runs · Flag bit of a machine state · Exact-length runs of a TM2 machine · A single step executes the statement at the current label · Bit on top of a stack · Running the bit-moving loop

Used byRaw-input PARTITION membership machine runs in quadratic time

AbbreviationCanonical PARTITION membership transducer as a host component#✓fully proved

Finite component for normalization followed by the membership map.

noncomputable abbrev comp : Cslib.Complexity.Host.Comp where
  K := K
  Γ := Γ
  finΓ k := by cases k <;> infer_instance
  L := Lab
  prog := prog
  ks := Finset.univ.toList
  ks_nodup := Finset.nodup_toList _
  mem_ks k := by simp

Uses 11 · Used by 1

Statement usesComponent machine · Stacks of the SUBSET-SUM verifier · Labels of the SUBSET-SUM verifier · Stack alphabet of the SAT verifier · Stacks of the PARTITION doubling machine · Control labels of the PARTITION doubling machine · Scan phases of the PARTITION doubling pass · Stacks of the canonical PARTITION membership transducer · Control labels of the canonical PARTITION membership transducer · Program of the canonical PARTITION membership transducer · Stack alphabets of the canonical PARTITION membership transducer

Used byRaw-input PARTITION membership machine as a host component

InductiveStacks of the raw-input PARTITION membership machine#✓fully proved

Disjoint normalizer and numeric-core workspaces and a transfer buffer.

inductive K | norm (k : ListNatMachine.K) | core (k : MembershipCore.K) | buffer
  deriving DecidableEq

Uses 2 · Used by 6

Statement usesStacks of the list-of-naturals canonicalizer · Stacks of the canonical PARTITION membership transducer

Used byRaw-input PARTITION membership machine as a host component · Numeric-core workspace of the raw-input PARTITION membership machine · PARTITION to SUBSET-SUM map is polynomial-time · Normalizer workspace of the raw-input PARTITION membership machine · Program of the raw-input PARTITION membership machine · Raw-input PARTITION membership machine runs in quadratic time

InductiveControl labels of the raw-input PARTITION membership machine#✓fully proved

Normalization, transfer, canonical computation, and rejection.

inductive Lab
  | norm (l : ListNatMachine.Lab) | move1 | move2 | start
  | core (l : MembershipCore.Lab) | bad | done
  deriving DecidableEq

Uses 2 · Used by 4

Statement usesControl labels of the list-of-naturals canonicalizer · Control labels of the canonical PARTITION membership transducer

Used byRaw-input PARTITION membership machine as a host component · PARTITION to SUBSET-SUM map is polynomial-time · Program of the raw-input PARTITION membership machine · Raw-input PARTITION membership machine runs in quadratic time

DefinitionNormalizer workspace of the raw-input PARTITION membership machine#✓fully proved

The exact canonicalizer's workspace.

def normEmb : SEmb (fun _ : ListNatMachine.K => Bool) Γ where
  e := K.norm
  inj _ _ h := K.norm.inj h
  ι _ := Equiv.refl _

Uses 5 · Used by 2

Statement usesStacks of the list-of-naturals canonicalizer · Stacks of the canonical PARTITION membership transducer · Stack alphabets of the canonical PARTITION membership transducer · Stacks of the raw-input PARTITION membership machine · Stack embedding

Used byProgram of the raw-input PARTITION membership machine · Raw-input PARTITION membership machine runs in quadratic time

DefinitionNumeric-core workspace of the raw-input PARTITION membership machine#✓fully proved

The canonical numeric core's workspace.

def coreEmb : SEmb MembershipCore.Γ Γ where
  e := K.core
  inj _ _ h := K.core.inj h
  ι _ := Equiv.refl _

Uses 5 · Used by 2

Statement usesStacks of the list-of-naturals canonicalizer · Stacks of the canonical PARTITION membership transducer · Stack alphabets of the canonical PARTITION membership transducer · Stacks of the raw-input PARTITION membership machine · Stack embedding

Used byProgram of the raw-input PARTITION membership machine · Raw-input PARTITION membership machine runs in quadratic time

DefinitionProgram of the raw-input PARTITION membership machine#✓fully proved

Normalize exactly, then run the polynomial numeric core.

def prog : Lab → TM2.Stmt Γ Lab Bool
  | .norm l => mapS normEmb normLabel (ListNatMachine.prog l)
  | .move1 => moveB (.norm .output) .buffer some id .move1 .move2
  | .move2 => moveB .buffer (.core .X) some id .move2 .start
  | .start => .load (fun _ => false) <| .goto fun _ => .core .copy
  | .core l => mapS coreEmb coreLabel (MembershipCore.prog l)
  | .bad => emitR (.core (.double .O)) noSS .done
  | .done => .halt

Uses 20 · Used by 3

Statement usesControl labels of the payload normalizer machine · Labels of the SUBSET-SUM verifier · Fixed no-instance of SUBSET-SUM · Stacks of the list-of-naturals canonicalizer · Control labels of the list-of-naturals canonicalizer · Program of the list-of-naturals canonicalizer · Stacks of the PARTITION doubling machine · Control labels of the PARTITION doubling machine · Stacks of the canonical PARTITION membership transducer · Control labels of the canonical PARTITION membership transducer · Program of the canonical PARTITION membership transducer · Stack alphabets of the canonical PARTITION membership transducer · Stacks of the raw-input PARTITION membership machine · Control labels of the raw-input PARTITION membership machine · Numeric-core workspace of the raw-input PARTITION membership machine · Normalizer workspace of the raw-input PARTITION membership machine · Translating a statement along a stack embedding · Flag bit of a machine state · Prepending a constant list · Bit-moving loop

Used byRaw-input PARTITION membership machine as a host component · PARTITION to SUBSET-SUM map is polynomial-time · Raw-input PARTITION membership machine runs in quadratic time

TheoremRaw-input PARTITION membership machine runs in quadratic time#✓fully proved

The exact all-string membership reduction has a quadratic machine bound, including malformed inputs and noncanonical binary payloads.

theorem run (x : List Bool) :
    ∃ v S, RunLe prog (100 * (x.length + 1) ^ 2)
      ⟨some (.norm .loop), false,
        update (fun _ => []) (.norm .input) x⟩
      ⟨some .done, v, S⟩ ∧
      S (.core (.double .O)) = reduceToSubsetSum x

Uses 63 · Used by 1

Statement usesStacks of the payload normalizer machine · Stacks of the SUBSET-SUM verifier · Stacks of the list-of-naturals canonicalizer · Control labels of the list-of-naturals canonicalizer · Stacks of the PARTITION doubling machine · Stacks of the canonical PARTITION membership transducer · Stack alphabets of the canonical PARTITION membership transducer · Stacks of the raw-input PARTITION membership machine · Control labels of the raw-input PARTITION membership machine · Program of the raw-input PARTITION membership machine · Encoded reduction from PARTITION to SUBSET-SUM · Runs within a step budget

Proof usesMachine step reading one framed payload pair · Control labels of the payload normalizer machine · Program of the payload normalizer machine · Stack contents for the payload normalizer invariant · Moving a bit block through a buffer · Labels of the SUBSET-SUM verifier · The SUBSET-SUM verifier program · Bit-string encoding of SUBSET-SUM instances · Fixed no-instance of SUBSET-SUM · Stack embedding of the number normalizer in the list canonicalizer · Label embedding of the number normalizer in the list canonicalizer · Program of the list-of-naturals canonicalizer · Embedded list canonicalizer preserves outside stacks · Workspace layout of the list-of-naturals canonicalizer · Re-encoded decoded list of naturals is linear in raw input · Reversed self-delimiting frame emitter · Stack alphabet of the SAT verifier · Reading a symbol as a name bit · Bitstring encodings · Decoding function of a bitstring encoding · Decoding inverts bitstring encoding · Encoding function of a bitstring encoding · Self-delimiting form of a bitstring · Parsing one self-delimiting block · Parsing a list of booleans into self-delimiting blocks · Bounded parsing of self-delimiting blocks · Control labels of the PARTITION doubling machine · Program of the PARTITION doubling machine · Control labels of the canonical PARTITION membership transducer · Doubling-machine stack embedding in the membership transducer · Label map from the doubling halt to the prefix emitter · Program of the canonical PARTITION membership transducer · Canonical PARTITION membership transducer runs in quadratic time · Summation-machine stack embedding in the membership transducer · Label map from summation halts to the doubling pass · Numeric-core workspace of the raw-input PARTITION membership machine · Normalizer workspace of the raw-input PARTITION membership machine · Agreement of host and sub-machine stacks · Embedding of a machine in a host · Frame condition for a stack embedding · Stack embedding · Translating a statement along a stack embedding · Run embedding for bounded runs · Flag bit of a machine state · Exact-length runs of a TM2 machine · A single step executes the statement at the current label · Bit on top of a stack · Pushing a constant list · Prepending a constant list · Bit-moving loop · Pushing a list of symbols onto one stack

Used byPARTITION to SUBSET-SUM map is polynomial-time

AbbreviationRaw-input PARTITION membership machine as a host component#✓fully proved

The total membership reduction in the existing finite host.

noncomputable abbrev comp : Cslib.Complexity.Host.Comp where
  K := K
  Γ := Γ
  finΓ k := by
    cases k with
    | norm _ | buffer => infer_instance
    | core k => exact MembershipCore.comp.finΓ k
  L := Lab
  prog := prog
  ks := Finset.univ.toList
  ks_nodup := Finset.nodup_toList _
  mem_ks k := by simp

Uses 17 · Used by 1

Statement usesStacks of the payload normalizer machine · Control labels of the payload normalizer machine · Component machine · Stacks of the SUBSET-SUM verifier · Labels of the SUBSET-SUM verifier · Stacks of the list-of-naturals canonicalizer · Control labels of the list-of-naturals canonicalizer · Stacks of the PARTITION doubling machine · Control labels of the PARTITION doubling machine · Scan phases of the PARTITION doubling pass · Stacks of the canonical PARTITION membership transducer · Control labels of the canonical PARTITION membership transducer · Canonical PARTITION membership transducer as a host component · Stack alphabets of the canonical PARTITION membership transducer · Stacks of the raw-input PARTITION membership machine · Control labels of the raw-input PARTITION membership machine · Program of the raw-input PARTITION membership machine

Used byPARTITION to SUBSET-SUM map is polynomial-time

TheoremPARTITION to SUBSET-SUM map is polynomial-time#✓fully proved

The total PARTITION-to-SUBSET-SUM map is polynomial-time.

theorem isPolyTime_reduceToSubsetSum : ComplexityTheory.IsPolyTime
    reduceToSubsetSum

Uses 25 · Used by 1

Statement usesBitstring encodings · Decoding function of a bitstring encoding · Decoding inverts bitstring encoding · Encoding function of a bitstring encoding · Self-delimiting form of a bitstring · Parsing one self-delimiting block · Parsing a list of booleans into self-delimiting blocks · Bounded parsing of self-delimiting blocks · Encoded reduction from PARTITION to SUBSET-SUM · Polynomial-time computable functions

Proof usesStacks of the payload normalizer machine · Component machine · Reduction host, canonical form · Stacks of the SUBSET-SUM verifier · Stacks of the list-of-naturals canonicalizer · Control labels of the list-of-naturals canonicalizer · Stacks of the PARTITION doubling machine · Stacks of the canonical PARTITION membership transducer · Stack alphabets of the canonical PARTITION membership transducer · Stacks of the raw-input PARTITION membership machine · Control labels of the raw-input PARTITION membership machine · Raw-input PARTITION membership machine as a host component · Program of the raw-input PARTITION membership machine · Raw-input PARTITION membership machine runs in quadratic time · Runs within a step budget

Used byBinary-coded PARTITION is in NP

TheoremBinary-coded PARTITION is in NP#✓fully proved

Exact binary-coded PARTITION belongs to canonical NP.

theorem partitionDec_mem_NP : partitionDec ∈ ComplexityTheory.NP

Uses 19 · Used by 1

Statement usesBinary-coded PARTITION decision problem · Complexity classes · Decision problems · The complexity class NP

Proof usesThe SUBSET-SUM problem · SUBSET-SUM is in NP · Bitstring encodings · Decoding function of a bitstring encoding · Decoding inverts bitstring encoding · Encoding function of a bitstring encoding · Self-delimiting form of a bitstring · Parsing one self-delimiting block · Parsing a list of booleans into self-delimiting blocks · Bounded parsing of self-delimiting blocks · PARTITION to SUBSET-SUM map is polynomial-time · Encoded reduction from PARTITION to SUBSET-SUM · Correctness of the encoded PARTITION to SUBSET-SUM reduction · Polynomial-time computable functions · NP membership pulls back along polynomial many-one reductions

Used byPARTITION is NP-complete

TheoremPolynomial-time reduction from SUBSET-SUM to PARTITION#✓fully proved

Binary-coded SUBSET-SUM reduces to the exact PARTITION decision problem.

theorem subsetSum_polyManyOneRed_partition :
    PolyManyOneRed subsetSumDec partitionDec

Uses 15 · Used by 1

Statement usesThe SUBSET-SUM problem · Polynomial-time many-one reduction · Binary-coded PARTITION decision problem

Proof usesBitstring encodings · Decoding function of a bitstring encoding · Decoding inverts bitstring encoding · Encoding function of a bitstring encoding · Self-delimiting form of a bitstring · Parsing one self-delimiting block · Parsing a list of booleans into self-delimiting blocks · Bounded parsing of self-delimiting blocks · SUBSET-SUM to PARTITION map is polynomial-time · Encoded reduction from SUBSET-SUM to PARTITION · Correctness of the encoded SUBSET-SUM to PARTITION reduction · Polynomial-time computable functions

Used byPARTITION is NP-complete

TheoremPARTITION is NP-complete#✓fully proved

Source: M. R. Garey and D. S. Johnson, Computers and Intractability (1979), PARTITION; R. M. Karp, "Reducibility among combinatorial problems" (1972).

theorem partition_npComplete :
    partitionDec ∈ MetaMathlibExt.ComplexityTheory.NP ∧
      ∀ L : MetaMathlibExt.ComplexityTheory.DecisionProblem,
        L ∈ MetaMathlibExt.ComplexityTheory.NP →
          Cslib.CookLevin.PolyManyOneRed L partitionDec

Uses 10

Statement usesPolynomial-time many-one reduction · Binary-coded PARTITION decision problem · Complexity classes · Decision problems · The complexity class NP

Proof usesNP-hardness transfers along reductions · The SUBSET-SUM problem · SUBSET-SUM is NP-hard · Binary-coded PARTITION is in NP · Polynomial-time reduction from SUBSET-SUM to PARTITION

64 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.