Graph invariants and iteration size

A client-supplied invariant establishes well-formed endpoints, bounded descriptor lengths, and constant-factor growth of the total number of vertices and edges. These properties give a bound on every complete encoded graph throughout an iteration. The bound charges the initial state even when the growth factor is zero, and includes the pair and list framing from the graph encoding.

For a ceiling-logarithmic number of rounds, the existing fixed-factor power certificate makes this size bound polynomial in the original input encoding. Clients can pass it directly to the existing iteration calculus; no new iteration rule or machine construction is needed.

Main definitions

• Cslib.PCP.Encoded.Graph.iterationSize: a bound on all intermediate encoded graph sizes.

Main results

• Cslib.PCP.Encoded.Graph.iterate_length_encoding_le: a preserved graph invariant supplies the full intermediate-state bound.
• Cslib.PCP.Encoded.Graph.polyBounded_iterationSize_clog: the bound is polynomial for a logarithmic number of rounds, including an efficiently computed initial graph.

References

• I. Dinur, The PCP theorem by gap amplification

def Cslib.PCP.Encoded.Graph.iterationSize {C : Type} (factor descriptorBound rounds : ℕ) (g : Graph C) : ℕ

A graph-size invariant bounds the complete framed state throughout the loop.

theorem Cslib.PCP.Encoded.Graph.polyBounded_iterationSize_clog {C Input : Type} {enc : C ↪ List Bool} {input : Input ↪ List Bool} {graph : Input → Graph C} (hgraph : Turing.MultiTapeTM.ComputableTidilyInPolyTime graph input (encoding enc)) (factor descriptorBound : ℕ) : Turing.MultiTapeTM.PolyBounded (fun (x : Input) => (input x).length) fun (x : Input) => iterationSize factor descriptorBound (Nat.clog 2 (graph x).edges.length) (graph x)

The logarithmic-round state bound is polynomial in any efficiently computed initial graph. Its fixed-factor power is computed by the existing charged logarithm/power certificate.

theorem Cslib.PCP.Encoded.Graph.iterate_length_encoding_le {C : Type} {enc : C ↪ List Bool} {step : Graph C → Graph C} {valid : Graph C → Prop} (factor descriptorBound : ℕ) (hvalid : ∀ (g : Graph C), valid g → valid (step g)) (hwellFormed : ∀ (g : Graph C), valid g → g.WellFormed) (hdescriptors : ∀ (g : Graph C), valid g → ∀ edge ∈ g.edges, (enc edge.constraint).length ≤ descriptorBound) (hgrowth : ∀ (g : Graph C), valid g → (step g).vertices + (step g).edges.length ≤ factor * (g.vertices + g.edges.length)) {g : Graph C} (hg : valid g) {i rounds : ℕ} (hi : i ≤ rounds) : ((encoding enc) (step^[i] g)).length ≤ iterationSize factor descriptorBound rounds g

A preserved graph invariant with fixed linear cardinality growth and bounded descriptors bounds every intermediate encoding, including the initial state and all list framing.