Documentation

Complexitylib.SAT.Tseitin.Machine.Internal.InvalidBranchSpec

Invalid-input branch of the Tseitin reduction machine #

On an input rejected by validEncoding, the total reduction machine never enters its supplied valid-input emitter. The validation verdict selects the else branch, that branch clears the verdict, and the fixed no-instance fallbackEncoding is emitted from a clean output accumulator.

The proof uses ifTM_hoareTime directly. Its then-branch precondition is False, justified by the known zero validator verdict, so the theorem and its time bound are completely independent of the supplied validEmitter.

Main results #

source
def Complexity.SAT.ThreeSAT.Machine.invalidReductionPost (z : List Bool) :
TapePred workTapeCount

The fully assembled invalid-path postcondition.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    theorem Complexity.SAT.ThreeSAT.Machine.invalidReductionTime_le_linear_internal (n : ℕ) :
    5 * n + 49 ≤ 49 * (n + 1)

    The explicit invalid-path budget is bounded by a single-coefficient linear polynomial.

    Validation branch routing #

    Full invalid path #

    source
    theorem Complexity.SAT.ThreeSAT.Machine.reductionTMWith_invalid_hoareTime_internal (validEmitter : TM workTapeCount) (z : List Bool) (hvalid : validEncoding z = false) :
    (reductionTMWith validEmitter).HoareTime (fun (inp : Tape) (work : Fin workTapeCount → Tape) (out : Tape) => inp = Tape.init (List.map Γ.ofBool z) ∧ (∀ (i : Fin workTapeCount), work i = Tape.init []) ∧ out = Tape.init []) (invalidReductionPost z) (5 * z.length + 49)

    Invalid branch of the total reduction. For every supplied valid-side emitter, a rejected input selects the else branch, clears the validator verdict, emits exactly fallbackEncoding, and halts within 5|z| + 49 steps.

    source
    theorem Complexity.SAT.ThreeSAT.Machine.reductionTMWith_invalid_reachesIn_internal (validEmitter : TM workTapeCount) (z : List Bool) (hvalid : validEncoding z = false) :
    ∃ (c' : Cfg workTapeCount (reductionTMWith validEmitter).Q), ∃ t ≤ 5 * z.length + 49, (reductionTMWith validEmitter).reachesIn t ((reductionTMWith validEmitter).initCfg z) c' ∧ (reductionTMWith validEmitter).halted c' ∧ c'.output.HasOutput fallbackEncoding

    Execution-level corollary from the standard initial configuration.