Exact sizes of the paired-port compiler

The actual output contains eight clauses and sixteen literal positions per ordinary ring, 78 clauses and 162 literal positions per paired crossover, and two binary clauses per retained path gap. Source literal repetitions are counted with multiplicity. These bounds apply to all inputs, without a geometric validity assumption.

Main results

• ordinaryCells_length_le_retained, ordinaryCells_length_le: occupied ordinary-cell bounds.
• length_formula, length_vars_formula: exact clause and literal accounting.
• width_formula: width-three inputs produce width-three outputs.
• length_formula_le, length_vars_formula_le: explicit quadratic output bounds.

References

The unchanged path estimates are reused from CslibFrontier.Computability.Complexity.Problems.SAT.Planar.PathBounds.

theorem Cslib.Complexity.SAT.ParsimoniousPlanar.crossingSites_length_le (φ : Logic.PL.CNF ℕ) : (crossingSites φ).length ≤ 2 * φ.vars.length ^ 2

Selected crossings reuse the canonical quadratic cover.

theorem Cslib.Complexity.SAT.ParsimoniousPlanar.ordinaryCells_length_le_retained (φ : Logic.PL.CNF ℕ) : (ordinaryCells φ).length ≤ (List.map (fun (r : Orthogonal.Route) => (List.dropLast r).length) (paths φ)).sum

Filtering and deduplication do not increase the number of retained path points.

theorem Cslib.Complexity.SAT.ParsimoniousPlanar.ordinaryCells_length_le (φ : Logic.PL.CNF ℕ) : (ordinaryCells φ).length ≤ φ.vars.length * (5 * PlanarCompile.budget φ + 1)

The ordinary-cell count is bounded by the canonical total path budget.

theorem Cslib.Complexity.SAT.ParsimoniousPlanar.length_originalClauses (φ : Logic.PL.CNF ℕ) (sites : List Orthogonal.Point) : (originalClauses φ sites).length = List.length φ

Original clauses keep their count.

theorem Cslib.Complexity.SAT.ParsimoniousPlanar.length_ordinaryClauses (p : Orthogonal.Point) : (ordinaryClauses p).length = 8

One ordinary cell contributes eight clauses.

theorem Cslib.Complexity.SAT.ParsimoniousPlanar.length_crossingClauses (p : Orthogonal.Point) : (crossingClauses p).length = 78

One crossing contributes 78 clauses.

theorem Cslib.Complexity.SAT.ParsimoniousPlanar.length_links (sites : List Orthogonal.Point) (r : Orthogonal.Route) : (links sites r).length = 2 * (List.length r - 2)

Each retained path gap contributes two clauses.

theorem Cslib.Complexity.SAT.ParsimoniousPlanar.length_rawFormula (φ : Logic.PL.CNF ℕ) : List.length (rawFormula φ) = List.length φ + 8 * (ordinaryCells φ).length + 78 * (crossingSites φ).length + 2 * PlanarCompile.linkCount φ

Exact clause count of the emitted structured formula.

theorem Cslib.Complexity.SAT.ParsimoniousPlanar.length_formula (φ : Logic.PL.CNF ℕ) : List.length (formula φ) = List.length φ + 8 * (ordinaryCells φ).length + 78 * (crossingSites φ).length + 2 * PlanarCompile.linkCount φ

Compaction preserves the exact output clause count.

theorem Cslib.Complexity.SAT.ParsimoniousPlanar.width_originalClauses {φ : Logic.PL.CNF ℕ} {k : ℕ} (h : ∀ c ∈ φ, List.length c ≤ k) (sites : List Orthogonal.Point) (c : PlacedClause) : c ∈ originalClauses φ sites → List.length c.1 ≤ k

Original clause records preserve their widths.

theorem Cslib.Complexity.SAT.ParsimoniousPlanar.width_ordinaryClauses (p : Orthogonal.Point) (c : PlacedClause) : c ∈ ordinaryClauses p → List.length c.1 = 2

Every ordinary ring clause is binary.

theorem Cslib.Complexity.SAT.ParsimoniousPlanar.width_crossingClauses (p : Orthogonal.Point) (c : PlacedClause) : c ∈ crossingClauses p → List.length c.1 ≤ 3

Every crossover clause has width at most three.

theorem Cslib.Complexity.SAT.ParsimoniousPlanar.width_links (sites : List Orthogonal.Point) (r : Orthogonal.Route) (c : PlacedClause) : c ∈ links sites r → List.length c.1 = 2

Every seam clause is binary.

theorem Cslib.Complexity.SAT.ParsimoniousPlanar.width_rawFormula {φ : Logic.PL.CNF ℕ} (h : ∀ c ∈ φ, List.length c ≤ 3) (c : Logic.PL.Clause Variable) : c ∈ rawFormula φ → List.length c ≤ 3

Width-three inputs produce structured formulas of width at most three.

theorem Cslib.Complexity.SAT.ParsimoniousPlanar.width_formula {φ : Logic.PL.CNF ℕ} (h : ∀ c ∈ φ, List.length c ≤ 3) (c : Logic.PL.Clause ℕ) : c ∈ formula φ → List.length c ≤ 3

Compaction preserves the width-three guarantee.

theorem Cslib.Complexity.SAT.ParsimoniousPlanar.length_vars_rawFormula (φ : Logic.PL.CNF ℕ) : (rawFormula φ).vars.length = φ.vars.length + 16 * (ordinaryCells φ).length + 162 * (crossingSites φ).length + 4 * PlanarCompile.linkCount φ

Exact literal count, including repetitions and all ordinary ring ports.

theorem Cslib.Complexity.SAT.ParsimoniousPlanar.length_vars_formula (φ : Logic.PL.CNF ℕ) : (formula φ).vars.length = φ.vars.length + 16 * (ordinaryCells φ).length + 162 * (crossingSites φ).length + 4 * PlanarCompile.linkCount φ

Compaction preserves the exact number of output literal occurrences.

theorem Cslib.Complexity.SAT.ParsimoniousPlanar.length_formula_le (φ : Logic.PL.CNF ℕ) : List.length (formula φ) ≤ 5000 * (φ.numVars + List.length φ + φ.vars.length + 1) ^ 2

A generous explicit quadratic clause bound in the source incidence size.

theorem Cslib.Complexity.SAT.ParsimoniousPlanar.length_vars_formula_le (φ : Logic.PL.CNF ℕ) : (formula φ).vars.length ≤ 10000 * (φ.numVars + List.length φ + φ.vars.length + 1) ^ 2

A generous explicit quadratic bound on output literal occurrences.