Documentation

DescriptiveComplexity.InductiveCounting.Complete

Completeness of the inductive-counting machine #

If no target is reachable from a source, the machine has an accepting run: the honest one, which certifies every node of every layer. The proof builds that run, four nested loops at a time – the certifying walk, the inner scan, the outer scan, and the sequence of stages – each by an induction along the finite linear order of nodes or, for the stages, on how much room the layer still has to grow.

Walking a finite linear order downwards #

source
theorem DescriptiveComplexity.InductiveCounting.order_induction_down {A : Type} [LinearOrder A] [Finite A] {P : A → Prop} (hmax : ∀ (z : A), (∀ (a : A), a ≤ z) → P z) (hstep : ∀ (w z : A), w ⋖ z → P z → P w) (z : A) :
P z

Induction from the greatest element downwards, one cover at a time.

Dependency graph

Configurations, explicitly #

source
def DescriptiveComplexity.InductiveCounting.mkCfg {V : Type} (ph : Phase) (fl : Bool) (rd rc rc2 rv rcnt ru rw rj : WithBot V) :
Cfg V

A configuration with its eight registers given one by one.

Equations
Instances For
    Dependency graph
    source
    @[simp]
    theorem DescriptiveComplexity.InductiveCounting.mkCfg_phase {V : Type} {ph : Phase} {fl : Bool} {rd rc rc2 rv rcnt ru rw rj : WithBot V} :
    (mkCfg ph fl rd rc rc2 rv rcnt ru rw rj).phase = ph
    Dependency graph
    source
    @[simp]
    theorem DescriptiveComplexity.InductiveCounting.mkCfg_flag {V : Type} {ph : Phase} {fl : Bool} {rd rc rc2 rv rcnt ru rw rj : WithBot V} :
    (mkCfg ph fl rd rc rc2 rv rcnt ru rw rj).flag = fl
    Dependency graph
    source
    @[simp]
    theorem DescriptiveComplexity.InductiveCounting.mkCfg_d {V : Type} {ph : Phase} {fl : Bool} {rd rc rc2 rv rcnt ru rw rj : WithBot V} :
    (mkCfg ph fl rd rc rc2 rv rcnt ru rw rj).regs Reg.d = rd
    Dependency graph
    source
    @[simp]
    theorem DescriptiveComplexity.InductiveCounting.mkCfg_c {V : Type} {ph : Phase} {fl : Bool} {rd rc rc2 rv rcnt ru rw rj : WithBot V} :
    (mkCfg ph fl rd rc rc2 rv rcnt ru rw rj).regs Reg.c = rc
    Dependency graph
    source
    @[simp]
    theorem DescriptiveComplexity.InductiveCounting.mkCfg_c2 {V : Type} {ph : Phase} {fl : Bool} {rd rc rc2 rv rcnt ru rw rj : WithBot V} :
    (mkCfg ph fl rd rc rc2 rv rcnt ru rw rj).regs Reg.c2 = rc2
    Dependency graph
    source
    @[simp]
    theorem DescriptiveComplexity.InductiveCounting.mkCfg_v {V : Type} {ph : Phase} {fl : Bool} {rd rc rc2 rv rcnt ru rw rj : WithBot V} :
    (mkCfg ph fl rd rc rc2 rv rcnt ru rw rj).regs Reg.v = rv
    Dependency graph
    source
    @[simp]
    theorem DescriptiveComplexity.InductiveCounting.mkCfg_cnt {V : Type} {ph : Phase} {fl : Bool} {rd rc rc2 rv rcnt ru rw rj : WithBot V} :
    (mkCfg ph fl rd rc rc2 rv rcnt ru rw rj).regs Reg.cnt = rcnt
    Dependency graph
    source
    @[simp]
    theorem DescriptiveComplexity.InductiveCounting.mkCfg_u {V : Type} {ph : Phase} {fl : Bool} {rd rc rc2 rv rcnt ru rw rj : WithBot V} :
    (mkCfg ph fl rd rc rc2 rv rcnt ru rw rj).regs Reg.u = ru
    Dependency graph
    source
    @[simp]
    theorem DescriptiveComplexity.InductiveCounting.mkCfg_w {V : Type} {ph : Phase} {fl : Bool} {rd rc rc2 rv rcnt ru rw rj : WithBot V} :
    (mkCfg ph fl rd rc rc2 rv rcnt ru rw rj).regs Reg.w = rw
    Dependency graph
    source
    @[simp]
    theorem DescriptiveComplexity.InductiveCounting.mkCfg_j {V : Type} {ph : Phase} {fl : Bool} {rd rc rc2 rv rcnt ru rw rj : WithBot V} :
    (mkCfg ph fl rd rc rc2 rv rcnt ru rw rj).regs Reg.j = rj
    Dependency graph

    The transitions, one lemma each #

    The certifying walk #

    The inner scan #

    The outer scan, the source count, and the stages #

    Completeness #