Finite occurrence-label buffers

Shared positional buffer operations for native edge-CSP augmentation and forest search. The namespace is retained from the augmentation API so existing imports and public names remain available. Constraint and port positions are unary; original variable names are binary. Every scan uses actual lists, including global validity on arbitrary explicit tables.

@[reducible, inline]

abbrev Cslib.Complexity.CSP.EdgeAugmenting.encRecord : ℕ × ℕ × ℕ ↪ List Bool

Positional occurrence records use unary constraint and scope positions and a binary name. Both positions are framed; the name is the last field.

@[reducible, inline]

abbrev Cslib.Complexity.CSP.EdgeAugmenting.Record : Type

Positional constraint index, scope index and original variable name.

@[reducible, inline]

abbrev Cslib.Complexity.CSP.EdgeAugmenting.encBuffer : Logic.PL.CSP Logic.PL.CSP.Table ℕ × List Bool ↪ List Bool

A framed explicit-table CSP followed by its framed occurrence-bit buffer.

def Cslib.Complexity.CSP.EdgeAugmenting.occurrenceIndex {F : Logic.PL.CSP Logic.PL.CSP.Table ℕ} (o : F.Occurrence) : ℕ

Global position in the actual incidence list, with no dependence on the variable's value.

def Cslib.Complexity.CSP.EdgeAugmenting.labeling (F : Logic.PL.CSP Logic.PL.CSP.Table ℕ) (bits : List Bool) : F.OccurrenceLabeling Bool

Read a finite buffer at an actual typed occurrence's global incidence-list position. The default makes this total even for a short buffer.

def Cslib.Complexity.CSP.EdgeAugmenting.readRecord (F : Logic.PL.CSP Logic.PL.CSP.Table ℕ) (bits : List Bool) (o : Record) : Bool

Read a positional record, defaulting to false outside the finite buffer.

def Cslib.Complexity.CSP.EdgeAugmenting.valid (F : Logic.PL.CSP Logic.PL.CSP.Table ℕ) (bits : List Bool) : Bool

Test every constraint against the complete finite labeling buffer.

def Cslib.Complexity.CSP.EdgeAugmenting.inconsistent (F : Logic.PL.CSP Logic.PL.CSP.Table ℕ) (bits : List Bool) (v : ℕ) : Bool

Test for unequal buffer bits at two actual occurrences of the requested variable.

def Cslib.Complexity.CSP.EdgeAugmenting.flip (bits : List Bool) (indices : List ℕ) : List Bool

Flip precisely the selected global positions, preserving the buffer width.

theorem Cslib.Complexity.CSP.EdgeAugmenting.poly_zipIdx {α β : Type} {e : α ↪ List Bool} {eb : β ↪ List Bool} {f : α → List β} (hf : Turing.MultiTapeTM.ComputableInPolyTime f e (Turing.MultiTapeTM.encList eb)) : Turing.MultiTapeTM.ComputableInPolyTime (fun (x : α) => (f x).zipIdx) e (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encPair eb Turing.MultiTapeTM.encUnary))

theorem Cslib.Complexity.CSP.EdgeAugmenting.poly_product {α β : Type} (ea : α ↪ List Bool) (eb : β ↪ List Bool) : Turing.MultiTapeTM.ComputableInPolyTime (fun (p : List α × List β) => p.1.product p.2) (Turing.MultiTapeTM.encPair (Turing.MultiTapeTM.encList ea) (Turing.MultiTapeTM.encList eb)) (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encPair ea eb))

theorem Cslib.Complexity.CSP.EdgeAugmenting.poly_idxOf {α β : Type} [DecidableEq β] {e : α ↪ List Bool} {eb : β ↪ List Bool} {list : α → List β} {value : α → β} (hl : Turing.MultiTapeTM.ComputableInPolyTime list e (Turing.MultiTapeTM.encList eb)) (hv : Turing.MultiTapeTM.ComputableInPolyTime value e eb) : Turing.MultiTapeTM.ComputableInPolyTime (fun (x : α) => List.idxOf (value x) (list x)) e Turing.MultiTapeTM.encUnary

theorem Cslib.Complexity.CSP.EdgeAugmenting.poly_records : Turing.MultiTapeTM.ComputableInPolyTime Logic.PL.CSP.occurrences (encCSP encTable Turing.MultiTapeTM.encNat) (Turing.MultiTapeTM.encList encRecord)

theorem Cslib.Complexity.CSP.EdgeAugmenting.poly_readRecord : Turing.MultiTapeTM.ComputableInPolyTime (fun (p : (Logic.PL.CSP Logic.PL.CSP.Table ℕ × List Bool) × Record) => readRecord p.1.1 p.1.2 p.2) (Turing.MultiTapeTM.encPair encBuffer encRecord) Turing.MultiTapeTM.encBool

theorem Cslib.Complexity.CSP.EdgeAugmenting.poly_readWith {α : Type} {e : α ↪ List Bool} {F : α → Logic.PL.CSP Logic.PL.CSP.Table ℕ} {bits : α → List Bool} {o : α → Record} (hF : Turing.MultiTapeTM.ComputableInPolyTime F e (encCSP encTable Turing.MultiTapeTM.encNat)) (hb : Turing.MultiTapeTM.ComputableInPolyTime bits e (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encBool)) (ho : Turing.MultiTapeTM.ComputableInPolyTime o e encRecord) : Turing.MultiTapeTM.ComputableInPolyTime (fun (x : α) => readRecord (F x) (bits x) (o x)) e Turing.MultiTapeTM.encBool

theorem Cslib.Complexity.CSP.EdgeAugmenting.poly_semWith {α : Type} {e : α ↪ List Bool} {table : α → Logic.PL.CSP.Table} {bits : α → List Bool} (ht : Turing.MultiTapeTM.ComputableInPolyTime table e encTable) (hb : Turing.MultiTapeTM.ComputableInPolyTime bits e (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encBool)) : Turing.MultiTapeTM.ComputableInPolyTime (fun (x : α) => (table x).sem (bits x)) e Turing.MultiTapeTM.encBool

theorem Cslib.Complexity.CSP.EdgeAugmenting.poly_valid : Turing.MultiTapeTM.ComputableInPolyTime (fun (p : Logic.PL.CSP Logic.PL.CSP.Table ℕ × List Bool) => valid p.1 p.2) encBuffer Turing.MultiTapeTM.encBool

theorem Cslib.Complexity.CSP.EdgeAugmenting.poly_inconsistent : Turing.MultiTapeTM.ComputableInPolyTime (fun (p : (Logic.PL.CSP Logic.PL.CSP.Table ℕ × List Bool) × ℕ) => inconsistent p.1.1 p.1.2 p.2) (Turing.MultiTapeTM.encPair encBuffer Turing.MultiTapeTM.encNat) Turing.MultiTapeTM.encBool

@[reducible, inline]

abbrev Cslib.Complexity.CSP.EdgeAugmenting.encFlip : List Bool × List ℕ ↪ List Bool

Work on bounded unary indices, with binary names unchanged.

theorem Cslib.Complexity.CSP.EdgeAugmenting.poly_flip : Turing.MultiTapeTM.ComputableInPolyTime (fun (p : List Bool × List ℕ) => flip p.1 p.2) encFlip (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encBool)

theorem Cslib.Complexity.CSP.EdgeAugmenting.poly_validWith {α : Type} {e : α ↪ List Bool} {F : α → Logic.PL.CSP Logic.PL.CSP.Table ℕ} {bits : α → List Bool} (hF : Turing.MultiTapeTM.ComputableInPolyTime F e (encCSP encTable Turing.MultiTapeTM.encNat)) (hb : Turing.MultiTapeTM.ComputableInPolyTime bits e (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encBool)) : Turing.MultiTapeTM.ComputableInPolyTime (fun (x : α) => valid (F x) (bits x)) e Turing.MultiTapeTM.encBool

theorem Cslib.Complexity.CSP.EdgeAugmenting.poly_inconsistentWith {α : Type} {e : α ↪ List Bool} {F : α → Logic.PL.CSP Logic.PL.CSP.Table ℕ} {bits : α → List Bool} {v : α → ℕ} (hF : Turing.MultiTapeTM.ComputableInPolyTime F e (encCSP encTable Turing.MultiTapeTM.encNat)) (hb : Turing.MultiTapeTM.ComputableInPolyTime bits e (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encBool)) (hv : Turing.MultiTapeTM.ComputableInPolyTime v e Turing.MultiTapeTM.encNat) : Turing.MultiTapeTM.ComputableInPolyTime (fun (x : α) => inconsistent (F x) (bits x) (v x)) e Turing.MultiTapeTM.encBool

theorem Cslib.Complexity.CSP.EdgeAugmenting.length_flip (bits : List Bool) (indices : List ℕ) : (flip bits indices).length = bits.length

theorem Cslib.Complexity.CSP.EdgeAugmenting.record_index {F : Logic.PL.CSP Logic.PL.CSP.Table ℕ} (o : F.Occurrence) : List.idxOf o.record F.occurrences = occurrenceIndex o

theorem Cslib.Complexity.CSP.EdgeAugmenting.read_record {F : Logic.PL.CSP Logic.PL.CSP.Table ℕ} (bits : List Bool) (o : F.Occurrence) : readRecord F bits o.record = labeling F bits o

theorem Cslib.Complexity.CSP.EdgeAugmenting.labeling_map (F : Logic.PL.CSP Logic.PL.CSP.Table ℕ) (f : F.OccurrenceLabeling Bool) : labeling F (List.map f F.incidenceList) = f

Encoding a labeling as a positional buffer and reading it returns that labeling.

theorem Cslib.Complexity.CSP.EdgeAugmenting.buffer_eq {F : Logic.PL.CSP Logic.PL.CSP.Table ℕ} (bits : List Bool) (hlen : bits.length = F.incidenceList.length) : bits = List.map (labeling F bits) F.incidenceList

An exact-width occurrence buffer is recovered by materializing its positional labeling in incidence-list order. Width is the actual number of occurrences, not a declared arity.

theorem Cslib.Complexity.CSP.EdgeAugmenting.getElem?_occurrenceIndex {F : Logic.PL.CSP Logic.PL.CSP.Table ℕ} (o : F.Occurrence) : F.incidenceList[occurrenceIndex o]? = some o

Projection of an existing walk followed by positional decoding recovers its occurrences.

theorem Cslib.Complexity.CSP.EdgeAugmenting.valid_eq (F : Logic.PL.CSP Logic.PL.CSP.Table ℕ) (bits : List Bool) : valid F bits = decide (Logic.PL.CSP.ValidLabeling Logic.PL.CSP.Table.sem (labeling F bits))

theorem Cslib.Complexity.CSP.EdgeAugmenting.inconsistent_eq (F : Logic.PL.CSP Logic.PL.CSP.Table ℕ) (bits : List Bool) (v : ℕ) : inconsistent F bits v = decide (Logic.PL.CSP.Inconsistent (labeling F bits) v)

theorem Cslib.Complexity.CSP.EdgeAugmenting.occurrenceIndex_lt {F : Logic.PL.CSP Logic.PL.CSP.Table ℕ} (o : F.Occurrence) : occurrenceIndex o < F.incidenceList.length

theorem Cslib.Complexity.CSP.EdgeAugmenting.occurrenceIndex_injective (F : Logic.PL.CSP Logic.PL.CSP.Table ℕ) : Function.Injective occurrenceIndex

theorem Cslib.Complexity.CSP.EdgeAugmenting.labeling_flip {F : Logic.PL.CSP Logic.PL.CSP.Table ℕ} (bits : List Bool) (s : List F.Occurrence) (hlen : bits.length = F.incidenceList.length) : labeling F (flip bits (List.map occurrenceIndex s)) = BitString.flipOn s.toFinset (labeling F bits)