Positional codes for chronological forest results

These codes represent the existing CSP.Forest.Result. Global occurrence indices reject when out of range. Logs are newest first; timestamps are the number of older expansions, so there is no independent timestamp to validate. No validity, edge-instance or reachability condition is imposed by the representation bridge.

structure Cslib.Complexity.CSP.EdgeForest.Input : Type

Complete native forest-search input. Labels follow actual constraint-then-port order.

• body : Logic.PL.CSP Logic.PL.CSP.Table ℕ

  Explicit relations and binary original variable names.

• labels : List Bool

  Finite occurrence-label buffer.

theorem Cslib.Complexity.CSP.EdgeForest.encInput_mk_budget {γ : Type} {encIn : γ ↪ List Bool} {budget : γ → ℕ} {x0 : γ → Logic.PL.CSP Logic.PL.CSP.Table ℕ} {x1 : γ → List Bool} (h0 : Turing.MultiTapeTM.ComputableInSpace x0 encIn (encCSP encTable Turing.MultiTapeTM.encNat) budget) (h1 : Turing.MultiTapeTM.ComputableInSpace x1 encIn (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encBool) budget) : Turing.MultiTapeTM.ComputableInSpace (fun (x : γ) => { body := x0 x, labels := x1 x }) encIn encInput budget

theorem Cslib.Complexity.CSP.EdgeForest.encInput_mk_deg : Turing.MultiTapeTM.ComputableInDegree (fun (p : Logic.PL.CSP Logic.PL.CSP.Table ℕ × List Bool) => { body := p.1, labels := p.2 }) encInputFields encInput 1 1

theorem Cslib.Complexity.CSP.EdgeForest.encInput_labels_deg : Turing.MultiTapeTM.ComputableInDegree Input.labels encInput (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encBool) 1 1

theorem Cslib.Complexity.CSP.EdgeForest.encInput_body_deg : Turing.MultiTapeTM.ComputableInDegree Input.body encInput (encCSP encTable Turing.MultiTapeTM.encNat) 1 1

theorem Cslib.Complexity.CSP.EdgeForest.encInput_body_polyTime {γ✝ : Type} {encIn✝ : γ✝ ↪ List Bool} {g✝ : γ✝ → Input} : Turing.MultiTapeTM.ComputableInPolyTime g✝ encIn✝ encInput → Turing.MultiTapeTM.ComputableInPolyTime (fun (a : γ✝) => (g✝ a).body) encIn✝ (encCSP encTable Turing.MultiTapeTM.encNat)

@[simp]

theorem Cslib.Complexity.CSP.EdgeForest.encInput_apply (a : Input) : encInput a = encInputFields (a.body, a.labels)

theorem Cslib.Complexity.CSP.EdgeForest.encInput_body_inO : Turing.MultiTapeTM.ComputableInO Input.body encInput (encCSP encTable Turing.MultiTapeTM.encNat) (fun (a : Input) => (encInput a).length) fun (a : Input) => (encInput a).length

def Cslib.Complexity.CSP.EdgeForest.encInput : Input ↪ List Bool

The explicit-table CSP is framed, followed by a framed Boolean list. Arity and variable names are binary; table rows and scopes are actual framed lists.

theorem Cslib.Complexity.CSP.EdgeForest.encInput_mk_inO {γ : Type} {encIn : γ ↪ List Bool} {x0 : γ → Logic.PL.CSP Logic.PL.CSP.Table ℕ} {T0 S0 : γ → ℕ} {x1 : γ → List Bool} {T1 S1 : γ → ℕ} (h0 : Turing.MultiTapeTM.ComputableInO x0 encIn (encCSP encTable Turing.MultiTapeTM.encNat) T0 S0) (h1 : Turing.MultiTapeTM.ComputableInO x1 encIn (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encBool) T1 S1) : Turing.MultiTapeTM.ComputableInO (fun (x : γ) => { body := x0 x, labels := x1 x }) encIn encInput (fun (x : γ) => T0 x + T1 x) fun (x : γ) => S0 x + S1 x

theorem Cslib.Complexity.CSP.EdgeForest.encInput_body_budget {γ✝ : Type} {encIn✝ : γ✝ ↪ List Bool} {S✝ : γ✝ → ℕ} {g✝ : γ✝ → Input} : Turing.MultiTapeTM.ComputableInSpace g✝ encIn✝ encInput S✝ → Turing.MultiTapeTM.ComputableInSpace (fun (a : γ✝) => (g✝ a).body) encIn✝ (encCSP encTable Turing.MultiTapeTM.encNat) S✝

theorem Cslib.Complexity.CSP.EdgeForest.encInput_mk_polyTime {γ : Type} {encIn : γ ↪ List Bool} {x0 : γ → Logic.PL.CSP Logic.PL.CSP.Table ℕ} {x1 : γ → List Bool} (h0 : Turing.MultiTapeTM.ComputableInPolyTime x0 encIn (encCSP encTable Turing.MultiTapeTM.encNat)) (h1 : Turing.MultiTapeTM.ComputableInPolyTime x1 encIn (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encBool)) : Turing.MultiTapeTM.ComputableInPolyTime (fun (x : γ) => { body := x0 x, labels := x1 x }) encIn encInput

@[reducible, inline]

abbrev Cslib.Complexity.CSP.EdgeForest.encInputFields : Logic.PL.CSP Logic.PL.CSP.Table ℕ × List Bool ↪ List Bool

The tuple of the fields of encInput.

theorem Cslib.Complexity.CSP.EdgeForest.encInput_labels_budget {γ✝ : Type} {encIn✝ : γ✝ ↪ List Bool} {S✝ : γ✝ → ℕ} {g✝ : γ✝ → Input} : Turing.MultiTapeTM.ComputableInSpace g✝ encIn✝ encInput S✝ → Turing.MultiTapeTM.ComputableInSpace (fun (a : γ✝) => (g✝ a).labels) encIn✝ (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encBool) S✝

theorem Cslib.Complexity.CSP.EdgeForest.encInput_labels_inO : Turing.MultiTapeTM.ComputableInO Input.labels encInput (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encBool) (fun (a : Input) => (encInput a).length) fun (a : Input) => (encInput a).length

theorem Cslib.Complexity.CSP.EdgeForest.encInput_fields_deg : Turing.MultiTapeTM.ComputableInDegree (fun (a : Input) => (a.body, a.labels)) encInput encInputFields 1 1

theorem Cslib.Complexity.CSP.EdgeForest.encInput_labels_polyTime {γ✝ : Type} {encIn✝ : γ✝ ↪ List Bool} {g✝ : γ✝ → Input} : Turing.MultiTapeTM.ComputableInPolyTime g✝ encIn✝ encInput → Turing.MultiTapeTM.ComputableInPolyTime (fun (a : γ✝) => (g✝ a).labels) encIn✝ (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encBool)

structure Cslib.Complexity.CSP.EdgeForest.ExpansionCode : Type

An expansion's input and ordered discovered output ports, as global positions.

• input : ℕ

  Global input position.

• outputs : List ℕ

  Ordered output positions.

def Cslib.Complexity.CSP.EdgeForest.instReprExpansionCode.repr : ExpansionCode → ℕ → Std.Format

@[instance_reducible]

instance Cslib.Complexity.CSP.EdgeForest.instReprExpansionCode : Repr ExpansionCode

@[reducible, inline]

abbrev Cslib.Complexity.CSP.EdgeForest.encExpansionCodeFields : ℕ × List ℕ ↪ List Bool

The tuple of the fields of encExpansionCode.

theorem Cslib.Complexity.CSP.EdgeForest.encExpansionCode_outputs_budget {γ✝ : Type} {encIn✝ : γ✝ ↪ List Bool} {S✝ : γ✝ → ℕ} {g✝ : γ✝ → ExpansionCode} : Turing.MultiTapeTM.ComputableInSpace g✝ encIn✝ encExpansionCode S✝ → Turing.MultiTapeTM.ComputableInSpace (fun (a : γ✝) => (g✝ a).outputs) encIn✝ (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encNat) S✝

theorem Cslib.Complexity.CSP.EdgeForest.encExpansionCode_mk_inO {γ : Type} {encIn : γ ↪ List Bool} {x0 T0 S0 : γ → ℕ} {x1 : γ → List ℕ} {T1 S1 : γ → ℕ} (h0 : Turing.MultiTapeTM.ComputableInO x0 encIn Turing.MultiTapeTM.encNat T0 S0) (h1 : Turing.MultiTapeTM.ComputableInO x1 encIn (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encNat) T1 S1) : Turing.MultiTapeTM.ComputableInO (fun (x : γ) => { input := x0 x, outputs := x1 x }) encIn encExpansionCode (fun (x : γ) => T0 x + T1 x) fun (x : γ) => S0 x + S1 x

theorem Cslib.Complexity.CSP.EdgeForest.encExpansionCode_fields_deg : Turing.MultiTapeTM.ComputableInDegree (fun (a : ExpansionCode) => (a.input, a.outputs)) encExpansionCode encExpansionCodeFields 1 1

theorem Cslib.Complexity.CSP.EdgeForest.encExpansionCode_input_budget {γ✝ : Type} {encIn✝ : γ✝ ↪ List Bool} {S✝ : γ✝ → ℕ} {g✝ : γ✝ → ExpansionCode} : Turing.MultiTapeTM.ComputableInSpace g✝ encIn✝ encExpansionCode S✝ → Turing.MultiTapeTM.ComputableInSpace (fun (a : γ✝) => (g✝ a).input) encIn✝ Turing.MultiTapeTM.encNat S✝

theorem Cslib.Complexity.CSP.EdgeForest.encExpansionCode_mk_budget {γ : Type} {encIn : γ ↪ List Bool} {budget x0 : γ → ℕ} {x1 : γ → List ℕ} (h0 : Turing.MultiTapeTM.ComputableInSpace x0 encIn Turing.MultiTapeTM.encNat budget) (h1 : Turing.MultiTapeTM.ComputableInSpace x1 encIn (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encNat) budget) : Turing.MultiTapeTM.ComputableInSpace (fun (x : γ) => { input := x0 x, outputs := x1 x }) encIn encExpansionCode budget

theorem Cslib.Complexity.CSP.EdgeForest.encExpansionCode_outputs_inO : Turing.MultiTapeTM.ComputableInO ExpansionCode.outputs encExpansionCode (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encNat) (fun (a : ExpansionCode) => (encExpansionCode a).length) fun (a : ExpansionCode) => (encExpansionCode a).length

theorem Cslib.Complexity.CSP.EdgeForest.encExpansionCode_input_deg : Turing.MultiTapeTM.ComputableInDegree ExpansionCode.input encExpansionCode Turing.MultiTapeTM.encNat 1 1

@[simp]

theorem Cslib.Complexity.CSP.EdgeForest.encExpansionCode_apply (a : ExpansionCode) : encExpansionCode a = encExpansionCodeFields (a.input, a.outputs)

theorem Cslib.Complexity.CSP.EdgeForest.encExpansionCode_outputs_polyTime {γ✝ : Type} {encIn✝ : γ✝ ↪ List Bool} {g✝ : γ✝ → ExpansionCode} : Turing.MultiTapeTM.ComputableInPolyTime g✝ encIn✝ encExpansionCode → Turing.MultiTapeTM.ComputableInPolyTime (fun (a : γ✝) => (g✝ a).outputs) encIn✝ (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encNat)

theorem Cslib.Complexity.CSP.EdgeForest.encExpansionCode_mk_deg : Turing.MultiTapeTM.ComputableInDegree (fun (p : ℕ × List ℕ) => { input := p.1, outputs := p.2 }) encExpansionCodeFields encExpansionCode 1 1

def Cslib.Complexity.CSP.EdgeForest.encExpansionCode : ExpansionCode ↪ List Bool

Binary input position, framed, followed by a framed list of binary output positions.

theorem Cslib.Complexity.CSP.EdgeForest.encExpansionCode_input_polyTime {γ✝ : Type} {encIn✝ : γ✝ ↪ List Bool} {g✝ : γ✝ → ExpansionCode} : Turing.MultiTapeTM.ComputableInPolyTime g✝ encIn✝ encExpansionCode → Turing.MultiTapeTM.ComputableInPolyTime (fun (a : γ✝) => (g✝ a).input) encIn✝ Turing.MultiTapeTM.encNat

theorem Cslib.Complexity.CSP.EdgeForest.encExpansionCode_input_inO : Turing.MultiTapeTM.ComputableInO ExpansionCode.input encExpansionCode Turing.MultiTapeTM.encNat (fun (a : ExpansionCode) => (encExpansionCode a).length) fun (a : ExpansionCode) => (encExpansionCode a).length

theorem Cslib.Complexity.CSP.EdgeForest.encExpansionCode_mk_polyTime {γ : Type} {encIn : γ ↪ List Bool} {x0 : γ → ℕ} {x1 : γ → List ℕ} (h0 : Turing.MultiTapeTM.ComputableInPolyTime x0 encIn Turing.MultiTapeTM.encNat) (h1 : Turing.MultiTapeTM.ComputableInPolyTime x1 encIn (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encNat)) : Turing.MultiTapeTM.ComputableInPolyTime (fun (x : γ) => { input := x0 x, outputs := x1 x }) encIn encExpansionCode

theorem Cslib.Complexity.CSP.EdgeForest.encExpansionCode_outputs_deg : Turing.MultiTapeTM.ComputableInDegree ExpansionCode.outputs encExpansionCode (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encNat) 1 1

def Cslib.Complexity.CSP.EdgeForest.instDecidableEqExpansionCode.decEq (x✝ x✝¹ : ExpansionCode) : Decidable (x✝ = x✝¹)

@[instance_reducible]

instance Cslib.Complexity.CSP.EdgeForest.instDecidableEqExpansionCode : DecidableEq ExpansionCode

structure Cslib.Complexity.CSP.EdgeForest.MeetingCode : Type

A complete meeting, retaining original roots, older expansions and partial current copy.

• roots : List ℕ

  Original root names in scan order.

• older : List ExpansionCode

  Completed expansions, newest first.

• current : ExpansionCode

  The current copy before the meeting output.

• output : ℕ

  Global meeting-output position.

def Cslib.Complexity.CSP.EdgeForest.instReprMeetingCode.repr : MeetingCode → ℕ → Std.Format

@[instance_reducible]

instance Cslib.Complexity.CSP.EdgeForest.instReprMeetingCode : Repr MeetingCode

theorem Cslib.Complexity.CSP.EdgeForest.encMeetingCode_current_deg : Turing.MultiTapeTM.ComputableInDegree MeetingCode.current encMeetingCode encExpansionCode 1 1

theorem Cslib.Complexity.CSP.EdgeForest.encMeetingCode_current_polyTime {γ✝ : Type} {encIn✝ : γ✝ ↪ List Bool} {g✝ : γ✝ → MeetingCode} : Turing.MultiTapeTM.ComputableInPolyTime g✝ encIn✝ encMeetingCode → Turing.MultiTapeTM.ComputableInPolyTime (fun (a : γ✝) => (g✝ a).current) encIn✝ encExpansionCode

theorem Cslib.Complexity.CSP.EdgeForest.encMeetingCode_roots_deg : Turing.MultiTapeTM.ComputableInDegree MeetingCode.roots encMeetingCode (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encNat) 1 1

theorem Cslib.Complexity.CSP.EdgeForest.encMeetingCode_older_polyTime {γ✝ : Type} {encIn✝ : γ✝ ↪ List Bool} {g✝ : γ✝ → MeetingCode} : Turing.MultiTapeTM.ComputableInPolyTime g✝ encIn✝ encMeetingCode → Turing.MultiTapeTM.ComputableInPolyTime (fun (a : γ✝) => (g✝ a).older) encIn✝ (Turing.MultiTapeTM.encList encExpansionCode)

def Cslib.Complexity.CSP.EdgeForest.encMeetingCode : MeetingCode ↪ List Bool

Roots, older log and current expansion are framed in field order; the last position is binary. Each list element is framed, including the nested expansion output lists.

theorem Cslib.Complexity.CSP.EdgeForest.encMeetingCode_older_inO : Turing.MultiTapeTM.ComputableInO MeetingCode.older encMeetingCode (Turing.MultiTapeTM.encList encExpansionCode) (fun (a : MeetingCode) => (encMeetingCode a).length) fun (a : MeetingCode) => (encMeetingCode a).length

theorem Cslib.Complexity.CSP.EdgeForest.encMeetingCode_mk_inO {γ : Type} {encIn : γ ↪ List Bool} {x0 : γ → List ℕ} {T0 S0 : γ → ℕ} {x1 : γ → List ExpansionCode} {T1 S1 : γ → ℕ} {x2 : γ → ExpansionCode} {T2 S2 x3 T3 S3 : γ → ℕ} (h0 : Turing.MultiTapeTM.ComputableInO x0 encIn (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encNat) T0 S0) (h1 : Turing.MultiTapeTM.ComputableInO x1 encIn (Turing.MultiTapeTM.encList encExpansionCode) T1 S1) (h2 : Turing.MultiTapeTM.ComputableInO x2 encIn encExpansionCode T2 S2) (h3 : Turing.MultiTapeTM.ComputableInO x3 encIn Turing.MultiTapeTM.encNat T3 S3) : Turing.MultiTapeTM.ComputableInO (fun (x : γ) => { roots := x0 x, older := x1 x, current := x2 x, output := x3 x }) encIn encMeetingCode (fun (x : γ) => T0 x + (T1 x + (T2 x + T3 x))) fun (x : γ) => S0 x + (S1 x + (S2 x + S3 x))

@[simp]

theorem Cslib.Complexity.CSP.EdgeForest.encMeetingCode_apply (a : MeetingCode) : encMeetingCode a = encMeetingCodeFields (a.roots, a.older, a.current, a.output)

@[reducible, inline]

abbrev Cslib.Complexity.CSP.EdgeForest.encMeetingCodeFields : List ℕ × List ExpansionCode × ExpansionCode × ℕ ↪ List Bool

The tuple of the fields of encMeetingCode.

theorem Cslib.Complexity.CSP.EdgeForest.encMeetingCode_output_deg : Turing.MultiTapeTM.ComputableInDegree MeetingCode.output encMeetingCode Turing.MultiTapeTM.encNat 1 1

theorem Cslib.Complexity.CSP.EdgeForest.encMeetingCode_current_budget {γ✝ : Type} {encIn✝ : γ✝ ↪ List Bool} {S✝ : γ✝ → ℕ} {g✝ : γ✝ → MeetingCode} : Turing.MultiTapeTM.ComputableInSpace g✝ encIn✝ encMeetingCode S✝ → Turing.MultiTapeTM.ComputableInSpace (fun (a : γ✝) => (g✝ a).current) encIn✝ encExpansionCode S✝

theorem Cslib.Complexity.CSP.EdgeForest.encMeetingCode_mk_deg : Turing.MultiTapeTM.ComputableInDegree (fun (p : List ℕ × List ExpansionCode × ExpansionCode × ℕ) => { roots := p.1, older := p.2.1, current := p.2.2.1, output := p.2.2.2 }) encMeetingCodeFields encMeetingCode 1 1

theorem Cslib.Complexity.CSP.EdgeForest.encMeetingCode_older_deg : Turing.MultiTapeTM.ComputableInDegree MeetingCode.older encMeetingCode (Turing.MultiTapeTM.encList encExpansionCode) 1 1

theorem Cslib.Complexity.CSP.EdgeForest.encMeetingCode_mk_budget {γ : Type} {encIn : γ ↪ List Bool} {budget : γ → ℕ} {x0 : γ → List ℕ} {x1 : γ → List ExpansionCode} {x2 : γ → ExpansionCode} {x3 : γ → ℕ} (h0 : Turing.MultiTapeTM.ComputableInSpace x0 encIn (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encNat) budget) (h1 : Turing.MultiTapeTM.ComputableInSpace x1 encIn (Turing.MultiTapeTM.encList encExpansionCode) budget) (h2 : Turing.MultiTapeTM.ComputableInSpace x2 encIn encExpansionCode budget) (h3 : Turing.MultiTapeTM.ComputableInSpace x3 encIn Turing.MultiTapeTM.encNat budget) : Turing.MultiTapeTM.ComputableInSpace (fun (x : γ) => { roots := x0 x, older := x1 x, current := x2 x, output := x3 x }) encIn encMeetingCode budget

theorem Cslib.Complexity.CSP.EdgeForest.encMeetingCode_roots_inO : Turing.MultiTapeTM.ComputableInO MeetingCode.roots encMeetingCode (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encNat) (fun (a : MeetingCode) => (encMeetingCode a).length) fun (a : MeetingCode) => (encMeetingCode a).length

theorem Cslib.Complexity.CSP.EdgeForest.encMeetingCode_output_inO : Turing.MultiTapeTM.ComputableInO MeetingCode.output encMeetingCode Turing.MultiTapeTM.encNat (fun (a : MeetingCode) => (encMeetingCode a).length) fun (a : MeetingCode) => (encMeetingCode a).length

theorem Cslib.Complexity.CSP.EdgeForest.encMeetingCode_fields_deg : Turing.MultiTapeTM.ComputableInDegree (fun (a : MeetingCode) => (a.roots, a.older, a.current, a.output)) encMeetingCode encMeetingCodeFields 1 1

theorem Cslib.Complexity.CSP.EdgeForest.encMeetingCode_roots_budget {γ✝ : Type} {encIn✝ : γ✝ ↪ List Bool} {S✝ : γ✝ → ℕ} {g✝ : γ✝ → MeetingCode} : Turing.MultiTapeTM.ComputableInSpace g✝ encIn✝ encMeetingCode S✝ → Turing.MultiTapeTM.ComputableInSpace (fun (a : γ✝) => (g✝ a).roots) encIn✝ (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encNat) S✝

theorem Cslib.Complexity.CSP.EdgeForest.encMeetingCode_mk_polyTime {γ : Type} {encIn : γ ↪ List Bool} {x0 : γ → List ℕ} {x1 : γ → List ExpansionCode} {x2 : γ → ExpansionCode} {x3 : γ → ℕ} (h0 : Turing.MultiTapeTM.ComputableInPolyTime x0 encIn (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encNat)) (h1 : Turing.MultiTapeTM.ComputableInPolyTime x1 encIn (Turing.MultiTapeTM.encList encExpansionCode)) (h2 : Turing.MultiTapeTM.ComputableInPolyTime x2 encIn encExpansionCode) (h3 : Turing.MultiTapeTM.ComputableInPolyTime x3 encIn Turing.MultiTapeTM.encNat) : Turing.MultiTapeTM.ComputableInPolyTime (fun (x : γ) => { roots := x0 x, older := x1 x, current := x2 x, output := x3 x }) encIn encMeetingCode

theorem Cslib.Complexity.CSP.EdgeForest.encMeetingCode_current_inO : Turing.MultiTapeTM.ComputableInO MeetingCode.current encMeetingCode encExpansionCode (fun (a : MeetingCode) => (encMeetingCode a).length) fun (a : MeetingCode) => (encMeetingCode a).length

theorem Cslib.Complexity.CSP.EdgeForest.encMeetingCode_roots_polyTime {γ✝ : Type} {encIn✝ : γ✝ ↪ List Bool} {g✝ : γ✝ → MeetingCode} : Turing.MultiTapeTM.ComputableInPolyTime g✝ encIn✝ encMeetingCode → Turing.MultiTapeTM.ComputableInPolyTime (fun (a : γ✝) => (g✝ a).roots) encIn✝ (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encNat)

theorem Cslib.Complexity.CSP.EdgeForest.encMeetingCode_output_budget {γ✝ : Type} {encIn✝ : γ✝ ↪ List Bool} {S✝ : γ✝ → ℕ} {g✝ : γ✝ → MeetingCode} : Turing.MultiTapeTM.ComputableInSpace g✝ encIn✝ encMeetingCode S✝ → Turing.MultiTapeTM.ComputableInSpace (fun (a : γ✝) => (g✝ a).output) encIn✝ Turing.MultiTapeTM.encNat S✝

theorem Cslib.Complexity.CSP.EdgeForest.encMeetingCode_output_polyTime {γ✝ : Type} {encIn✝ : γ✝ ↪ List Bool} {g✝ : γ✝ → MeetingCode} : Turing.MultiTapeTM.ComputableInPolyTime g✝ encIn✝ encMeetingCode → Turing.MultiTapeTM.ComputableInPolyTime (fun (a : γ✝) => (g✝ a).output) encIn✝ Turing.MultiTapeTM.encNat

theorem Cslib.Complexity.CSP.EdgeForest.encMeetingCode_older_budget {γ✝ : Type} {encIn✝ : γ✝ ↪ List Bool} {S✝ : γ✝ → ℕ} {g✝ : γ✝ → MeetingCode} : Turing.MultiTapeTM.ComputableInSpace g✝ encIn✝ encMeetingCode S✝ → Turing.MultiTapeTM.ComputableInSpace (fun (a : γ✝) => (g✝ a).older) encIn✝ (Turing.MultiTapeTM.encList encExpansionCode) S✝

def Cslib.Complexity.CSP.EdgeForest.instDecidableEqMeetingCode.decEq (x✝ x✝¹ : MeetingCode) : Decidable (x✝ = x✝¹)

@[instance_reducible]

instance Cslib.Complexity.CSP.EdgeForest.instDecidableEqMeetingCode : DecidableEq MeetingCode

@[reducible, inline]

abbrev Cslib.Complexity.CSP.EdgeForest.ResultCode : Type

Exhausted log, or augmentation meeting, or blossom meeting, in that order.

@[reducible, inline]

abbrev Cslib.Complexity.CSP.EdgeForest.encResultCode : List ExpansionCode ⊕ MeetingCode ⊕ MeetingCode ↪ List Bool

One sum tag for exhaustion versus event; an event has a second tag for augment versus blossom. Expansion lists and meetings use their documented binary positional encodings.

def Cslib.Complexity.CSP.EdgeForest.codeExpansion {F : Logic.PL.CSP Logic.PL.CSP.Table ℕ} (e : Logic.PL.CSP.Forest.Expansion F) : ExpansionCode

Encode an existing expansion by its actual incidence-list positions.

def Cslib.Complexity.CSP.EdgeForest.codeMeeting {F : Logic.PL.CSP Logic.PL.CSP.Table ℕ} (m : Logic.PL.CSP.Forest.Meeting F) : MeetingCode

Encode every field of an existing meeting, preserving the partial current expansion.

def Cslib.Complexity.CSP.EdgeForest.code {F : Logic.PL.CSP Logic.PL.CSP.Table ℕ} : Logic.PL.CSP.Forest.Result F → ResultCode

Encode the existing result without making any mathematical assertion about its event.

def Cslib.Complexity.CSP.EdgeForest.decodeExpansion (F : Logic.PL.CSP Logic.PL.CSP.Table ℕ) (e : ExpansionCode) : Option (Logic.PL.CSP.Forest.Expansion F)

Decode an expansion, rejecting any invalid input or output position.

def Cslib.Complexity.CSP.EdgeForest.decodeMeeting (F : Logic.PL.CSP Logic.PL.CSP.Table ℕ) (m : MeetingCode) : Option (Logic.PL.CSP.Forest.Meeting F)

Decode all positional fields of a meeting. Roots remain binary original names.

def Cslib.Complexity.CSP.EdgeForest.decode (F : Logic.PL.CSP Logic.PL.CSP.Table ℕ) : ResultCode → Option (Logic.PL.CSP.Forest.Result F)

Decode to the existing dependent forest result, rejecting malformed indices in every tag.

@[simp]

theorem Cslib.Complexity.CSP.EdgeForest.decodeExpansion_codeExpansion {F : Logic.PL.CSP Logic.PL.CSP.Table ℕ} (e : Logic.PL.CSP.Forest.Expansion F) : decodeExpansion F (codeExpansion e) = some e

Expansion codes are lossless even for externally supplied malformed forest histories.

@[simp]

theorem Cslib.Complexity.CSP.EdgeForest.decodeMeeting_codeMeeting {F : Logic.PL.CSP Logic.PL.CSP.Table ℕ} (m : Logic.PL.CSP.Forest.Meeting F) : decodeMeeting F (codeMeeting m) = some m

Meeting codes retain the full log, roots and partial copy.

@[simp]

theorem Cslib.Complexity.CSP.EdgeForest.decode_code {F : Logic.PL.CSP Logic.PL.CSP.Table ℕ} (r : Logic.PL.CSP.Forest.Result F) : decode F (code r) = some r

The complete result bridge is lossless, with no semantic or forest invariant premise.