Literal occurrences in the paired-port compiler

Each directed path half has its own port on each lane. These keys are distinct across all canonical source paths. The emitted external literals form a submultiset of those keys, so a port receives at most one external occurrence. Each emitted ring contributes two internal occurrences per port; the paired crossover contributes two at its ports and at most three at its internal variables.

Main results

• count_vars_rawFormula_le_three: the actual structured output respects the occurrence bound.
• count_vars_formula_le_three: injective compaction preserves that bound.

References

This literal-position accounting for the paired compiler is original.

def Cslib.Complexity.SAT.ParsimoniousPlanar.pathPortKeys (r : Orthogonal.Route) : List (Orthogonal.Point × Fin 4)

The directed side used by each half of every unit step.

def Cslib.Complexity.SAT.ParsimoniousPlanar.portKeySignal (sites : List Orthogonal.Point) (k : (Orthogonal.Point × Fin 4) × Fin 2) : Variable

The signal attached to one directed half on one lane.

def Cslib.Complexity.SAT.ParsimoniousPlanar.pathPortSignals (sites : List Orthogonal.Point) (r : Orthogonal.Route) : List Variable

Both lanes of each directed path half, including the unused halves at the final clause.

theorem Cslib.Complexity.SAT.ParsimoniousPlanar.count_links_lastLiteral_le (sites : List Orthogonal.Point) (positive : Bool) (r : Orthogonal.Route) (hlen : 2 ≤ List.length r) (v : Variable) : List.count v (Logic.PL.CNF.vars (List.map Prod.fst (links sites r))) + List.count v [(lastLiteral sites r positive).1.1] ≤ List.count v (pathPortSignals sites r)

External literals use only their actual path-half ports; unused clause halves overcount.

def Cslib.Complexity.SAT.ParsimoniousPlanar.allPathPortSignals (φ : Logic.PL.CNF ℕ) : List Variable

Both lanes of every directed port in all actual canonical paths.

theorem Cslib.Complexity.SAT.ParsimoniousPlanar.allPathPortSignals_nodup {φ : Logic.PL.CNF ℕ} (hw : ∀ c ∈ φ, List.length c ≤ 3) (hv : ∀ (v : ℕ), List.count v φ.vars ≤ 3) : (allPathPortSignals φ).Nodup

Across all canonical paths each presented side/lane variable is distinct.

def Cslib.Complexity.SAT.ParsimoniousPlanar.ordinarySignals (φ : Logic.PL.CNF ℕ) : List Variable

Literal positions supplied by all emitted ordinary rings.

def Cslib.Complexity.SAT.ParsimoniousPlanar.crossingSignals (φ : Logic.PL.CNF ℕ) : List Variable

Literal positions supplied by all emitted paired crossovers.

theorem Cslib.Complexity.SAT.ParsimoniousPlanar.count_vars_rawFormula_le (φ : Logic.PL.CNF ℕ) (v : Variable) : List.count v (rawFormula φ).vars ≤ List.count v (ordinarySignals φ) + List.count v (crossingSignals φ) + List.count v (allPathPortSignals φ)

Count actual emitted literals by internal template literals and actual path-half ports.

theorem Cslib.Complexity.SAT.ParsimoniousPlanar.count_vars_rawFormula_le_three {φ : Logic.PL.CNF ℕ} (hw : ∀ c ∈ φ, List.length c ≤ 3) (hv : ∀ (v : ℕ), List.count v φ.vars ≤ 3) (v : Variable) : List.count v (rawFormula φ).vars ≤ 3

Every actual output variable has at most three literal occurrences, including repetitions inside a clause. No occurrence certificate is assumed for the output.

theorem Cslib.Complexity.SAT.ParsimoniousPlanar.count_vars_formula_le_three {φ : Logic.PL.CNF ℕ} (hw : ∀ c ∈ φ, List.length c ≤ 3) (hv : ∀ (v : ℕ), List.count v φ.vars ≤ 3) (v : ℕ) : List.count v (formula φ).vars ≤ 3

Injective compaction preserves the actual literal-occurrence bound.