Finite chronological ancestry and blossom compilation

A single backwards scan reconstructs actual root paths. Timestamps are paid for by the older log's length and retain copied-constraint identity. Original names and public occurrence positions remain binary. The representation bookkeeping is original; the two LCA cases are those of [KKR18], arXiv:1602.03124v6, Section 5.3, printed pp. 11–12.

structure Cslib.Complexity.CSP.EdgeSolver.NativeForest.TraceCode : Type

Backwards-scan state: queried binary variable and the already reconstructed suffix.

• start : ℕ

  Current ancestor's binary original name.

• steps : List (ℕ × ℕ)

  Actual binary global port pairs in root-to-leaf order.

• times : List ℕ

  Actual copy timestamps, in the same order and encoded unary.

theorem Cslib.Complexity.CSP.EdgeSolver.NativeForest.encTraceCode_mk_inO {γ : Type} {encIn : γ ↪ List Bool} {x0 T0 S0 : γ → ℕ} {x1 : γ → List (ℕ × ℕ)} {T1 S1 : γ → ℕ} {x2 : γ → List ℕ} {T2 S2 : γ → ℕ} (h0 : Turing.MultiTapeTM.ComputableInO x0 encIn Turing.MultiTapeTM.encNat T0 S0) (h1 : Turing.MultiTapeTM.ComputableInO x1 encIn (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encNat Turing.MultiTapeTM.encNat)) T1 S1) (h2 : Turing.MultiTapeTM.ComputableInO x2 encIn (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encUnary) T2 S2) : Turing.MultiTapeTM.ComputableInO (fun (x : γ) => { start := x0 x, steps := x1 x, times := x2 x }) encIn encTraceCode (fun (x : γ) => T0 x + (T1 x + T2 x)) fun (x : γ) => S0 x + (S1 x + S2 x)

theorem Cslib.Complexity.CSP.EdgeSolver.NativeForest.encTraceCode_start_polyTime {γ✝ : Type} {encIn✝ : γ✝ ↪ List Bool} {g✝ : γ✝ → TraceCode} : Turing.MultiTapeTM.ComputableInPolyTime g✝ encIn✝ encTraceCode → Turing.MultiTapeTM.ComputableInPolyTime (fun (a : γ✝) => (g✝ a).start) encIn✝ Turing.MultiTapeTM.encNat

theorem Cslib.Complexity.CSP.EdgeSolver.NativeForest.encTraceCode_start_inO : Turing.MultiTapeTM.ComputableInO TraceCode.start encTraceCode Turing.MultiTapeTM.encNat (fun (a : TraceCode) => (encTraceCode a).length) fun (a : TraceCode) => (encTraceCode a).length

theorem Cslib.Complexity.CSP.EdgeSolver.NativeForest.encTraceCode_mk_deg : Turing.MultiTapeTM.ComputableInDegree (fun (p : ℕ × List (ℕ × ℕ) × List ℕ) => { start := p.1, steps := p.2.1, times := p.2.2 }) encTraceCodeFields encTraceCode 1 1

@[reducible, inline]

abbrev Cslib.Complexity.CSP.EdgeSolver.NativeForest.encTraceCodeFields : ℕ × List (ℕ × ℕ) × List ℕ ↪ List Bool

The tuple of the fields of encTraceCode.

theorem Cslib.Complexity.CSP.EdgeSolver.NativeForest.encTraceCode_steps_deg : Turing.MultiTapeTM.ComputableInDegree TraceCode.steps encTraceCode (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encNat Turing.MultiTapeTM.encNat)) 1 1

theorem Cslib.Complexity.CSP.EdgeSolver.NativeForest.encTraceCode_times_polyTime {γ✝ : Type} {encIn✝ : γ✝ ↪ List Bool} {g✝ : γ✝ → TraceCode} : Turing.MultiTapeTM.ComputableInPolyTime g✝ encIn✝ encTraceCode → Turing.MultiTapeTM.ComputableInPolyTime (fun (a : γ✝) => (g✝ a).times) encIn✝ (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encUnary)

theorem Cslib.Complexity.CSP.EdgeSolver.NativeForest.encTraceCode_steps_inO : Turing.MultiTapeTM.ComputableInO TraceCode.steps encTraceCode (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encNat Turing.MultiTapeTM.encNat)) (fun (a : TraceCode) => (encTraceCode a).length) fun (a : TraceCode) => (encTraceCode a).length

theorem Cslib.Complexity.CSP.EdgeSolver.NativeForest.encTraceCode_times_deg : Turing.MultiTapeTM.ComputableInDegree TraceCode.times encTraceCode (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encUnary) 1 1

theorem Cslib.Complexity.CSP.EdgeSolver.NativeForest.encTraceCode_fields_deg : Turing.MultiTapeTM.ComputableInDegree (fun (a : TraceCode) => (a.start, a.steps, a.times)) encTraceCode encTraceCodeFields 1 1

theorem Cslib.Complexity.CSP.EdgeSolver.NativeForest.encTraceCode_steps_budget {γ✝ : Type} {encIn✝ : γ✝ ↪ List Bool} {S✝ : γ✝ → ℕ} {g✝ : γ✝ → TraceCode} : Turing.MultiTapeTM.ComputableInSpace g✝ encIn✝ encTraceCode S✝ → Turing.MultiTapeTM.ComputableInSpace (fun (a : γ✝) => (g✝ a).steps) encIn✝ (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encNat Turing.MultiTapeTM.encNat)) S✝

theorem Cslib.Complexity.CSP.EdgeSolver.NativeForest.encTraceCode_start_budget {γ✝ : Type} {encIn✝ : γ✝ ↪ List Bool} {S✝ : γ✝ → ℕ} {g✝ : γ✝ → TraceCode} : Turing.MultiTapeTM.ComputableInSpace g✝ encIn✝ encTraceCode S✝ → Turing.MultiTapeTM.ComputableInSpace (fun (a : γ✝) => (g✝ a).start) encIn✝ Turing.MultiTapeTM.encNat S✝

theorem Cslib.Complexity.CSP.EdgeSolver.NativeForest.encTraceCode_steps_polyTime {γ✝ : Type} {encIn✝ : γ✝ ↪ List Bool} {g✝ : γ✝ → TraceCode} : Turing.MultiTapeTM.ComputableInPolyTime g✝ encIn✝ encTraceCode → Turing.MultiTapeTM.ComputableInPolyTime (fun (a : γ✝) => (g✝ a).steps) encIn✝ (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encNat Turing.MultiTapeTM.encNat))

theorem Cslib.Complexity.CSP.EdgeSolver.NativeForest.encTraceCode_mk_budget {γ : Type} {encIn : γ ↪ List Bool} {budget x0 : γ → ℕ} {x1 : γ → List (ℕ × ℕ)} {x2 : γ → List ℕ} (h0 : Turing.MultiTapeTM.ComputableInSpace x0 encIn Turing.MultiTapeTM.encNat budget) (h1 : Turing.MultiTapeTM.ComputableInSpace x1 encIn (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encNat Turing.MultiTapeTM.encNat)) budget) (h2 : Turing.MultiTapeTM.ComputableInSpace x2 encIn (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encUnary) budget) : Turing.MultiTapeTM.ComputableInSpace (fun (x : γ) => { start := x0 x, steps := x1 x, times := x2 x }) encIn encTraceCode budget

theorem Cslib.Complexity.CSP.EdgeSolver.NativeForest.encTraceCode_times_inO : Turing.MultiTapeTM.ComputableInO TraceCode.times encTraceCode (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encUnary) (fun (a : TraceCode) => (encTraceCode a).length) fun (a : TraceCode) => (encTraceCode a).length

@[simp]

theorem Cslib.Complexity.CSP.EdgeSolver.NativeForest.encTraceCode_apply (a : TraceCode) : encTraceCode a = encTraceCodeFields (a.start, a.steps, a.times)

theorem Cslib.Complexity.CSP.EdgeSolver.NativeForest.encTraceCode_start_deg : Turing.MultiTapeTM.ComputableInDegree TraceCode.start encTraceCode Turing.MultiTapeTM.encNat 1 1

theorem Cslib.Complexity.CSP.EdgeSolver.NativeForest.encTraceCode_times_budget {γ✝ : Type} {encIn✝ : γ✝ ↪ List Bool} {S✝ : γ✝ → ℕ} {g✝ : γ✝ → TraceCode} : Turing.MultiTapeTM.ComputableInSpace g✝ encIn✝ encTraceCode S✝ → Turing.MultiTapeTM.ComputableInSpace (fun (a : γ✝) => (g✝ a).times) encIn✝ (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encUnary) S✝

def Cslib.Complexity.CSP.EdgeSolver.NativeForest.encTraceCode : TraceCode ↪ List Bool

Framed binary start and framed binary position pairs, followed by framed unary times.

theorem Cslib.Complexity.CSP.EdgeSolver.NativeForest.encTraceCode_mk_polyTime {γ : Type} {encIn : γ ↪ List Bool} {x0 : γ → ℕ} {x1 : γ → List (ℕ × ℕ)} {x2 : γ → List ℕ} (h0 : Turing.MultiTapeTM.ComputableInPolyTime x0 encIn Turing.MultiTapeTM.encNat) (h1 : Turing.MultiTapeTM.ComputableInPolyTime x1 encIn (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encNat Turing.MultiTapeTM.encNat))) (h2 : Turing.MultiTapeTM.ComputableInPolyTime x2 encIn (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encUnary)) : Turing.MultiTapeTM.ComputableInPolyTime (fun (x : γ) => { start := x0 x, steps := x1 x, times := x2 x }) encIn encTraceCode

def Cslib.Complexity.CSP.EdgeSolver.NativeForest.traceStep (F : Logic.PL.CSP Logic.PL.CSP.Table ℕ) (s : TraceCode) (e : EdgeForest.ExpansionCode × ℕ) : TraceCode

Follow one actual parent through a strictly older expansion.

def Cslib.Complexity.CSP.EdgeSolver.NativeForest.trace (F : Logic.PL.CSP Logic.PL.CSP.Table ℕ) (es : List EdgeForest.ExpansionCode) (s : TraceCode) : TraceCode

Scan newest-first expansions with the actual decreasing copy timestamps.

def Cslib.Complexity.CSP.EdgeSolver.NativeForest.ancestry (F : Logic.PL.CSP Logic.PL.CSP.Table ℕ) (es : List EdgeForest.ExpansionCode) (v : ℕ) : TraceCode

Root-to-variable ancestry with exact ordered step positions and actual copy times.

def Cslib.Complexity.CSP.EdgeSolver.NativeForest.walk (p : TraceCode) : EdgeAugmenting.WalkCode

Forget only the copy timestamps of an actual ancestry code.

@[reducible, inline]

abbrev Cslib.Complexity.CSP.EdgeSolver.NativeForest.NodeCode : Type

Actual variable/copy node codes; copied nodes keep original constraint and time.

@[reducible, inline]

abbrev Cslib.Complexity.CSP.EdgeSolver.NativeForest.encNodeCode : ℕ ⊕ ℕ × ℕ ↪ List Bool

A variable/copy tag precedes binary original names or unary constraint/time coordinates.

def Cslib.Complexity.CSP.EdgeSolver.NativeForest.nodes (F : Logic.PL.CSP Logic.PL.CSP.Table ℕ) (p : TraceCode) : List NodeCode

Original variables alternate with actual timestamped copied constraints.

def Cslib.Complexity.CSP.EdgeSolver.NativeForest.common (F : Logic.PL.CSP Logic.PL.CSP.Table ℕ) (left right : TraceCode) : List NodeCode

The full common root-path prefix, retaining both coordinates of a copied constraint.

structure Cslib.Complexity.CSP.EdgeSolver.NativeForest.BlossomCode : Type

The preparatory root path and actual closed cycle; metadata remain in the source layer.

• prepare : EdgeAugmenting.WalkCode

  Root-to-base path whose flip prepares the blossom.

• cycle : EdgeAugmenting.WalkCode

  Actual cycle in original global port order.

theorem Cslib.Complexity.CSP.EdgeSolver.NativeForest.encBlossomCode_cycle_deg : Turing.MultiTapeTM.ComputableInDegree BlossomCode.cycle encBlossomCode EdgeAugmenting.encWalkCode 1 1

theorem Cslib.Complexity.CSP.EdgeSolver.NativeForest.encBlossomCode_prepare_inO : Turing.MultiTapeTM.ComputableInO BlossomCode.prepare encBlossomCode EdgeAugmenting.encWalkCode (fun (a : BlossomCode) => (encBlossomCode a).length) fun (a : BlossomCode) => (encBlossomCode a).length

theorem Cslib.Complexity.CSP.EdgeSolver.NativeForest.encBlossomCode_prepare_polyTime {γ✝ : Type} {encIn✝ : γ✝ ↪ List Bool} {g✝ : γ✝ → BlossomCode} : Turing.MultiTapeTM.ComputableInPolyTime g✝ encIn✝ encBlossomCode → Turing.MultiTapeTM.ComputableInPolyTime (fun (a : γ✝) => (g✝ a).prepare) encIn✝ EdgeAugmenting.encWalkCode

theorem Cslib.Complexity.CSP.EdgeSolver.NativeForest.encBlossomCode_fields_deg : Turing.MultiTapeTM.ComputableInDegree (fun (a : BlossomCode) => (a.prepare, a.cycle)) encBlossomCode encBlossomCodeFields 1 1

theorem Cslib.Complexity.CSP.EdgeSolver.NativeForest.encBlossomCode_cycle_polyTime {γ✝ : Type} {encIn✝ : γ✝ ↪ List Bool} {g✝ : γ✝ → BlossomCode} : Turing.MultiTapeTM.ComputableInPolyTime g✝ encIn✝ encBlossomCode → Turing.MultiTapeTM.ComputableInPolyTime (fun (a : γ✝) => (g✝ a).cycle) encIn✝ EdgeAugmenting.encWalkCode

theorem Cslib.Complexity.CSP.EdgeSolver.NativeForest.encBlossomCode_prepare_budget {γ✝ : Type} {encIn✝ : γ✝ ↪ List Bool} {S✝ : γ✝ → ℕ} {g✝ : γ✝ → BlossomCode} : Turing.MultiTapeTM.ComputableInSpace g✝ encIn✝ encBlossomCode S✝ → Turing.MultiTapeTM.ComputableInSpace (fun (a : γ✝) => (g✝ a).prepare) encIn✝ EdgeAugmenting.encWalkCode S✝

theorem Cslib.Complexity.CSP.EdgeSolver.NativeForest.encBlossomCode_mk_inO {γ : Type} {encIn : γ ↪ List Bool} {x0 : γ → EdgeAugmenting.WalkCode} {T0 S0 : γ → ℕ} {x1 : γ → EdgeAugmenting.WalkCode} {T1 S1 : γ → ℕ} (h0 : Turing.MultiTapeTM.ComputableInO x0 encIn EdgeAugmenting.encWalkCode T0 S0) (h1 : Turing.MultiTapeTM.ComputableInO x1 encIn EdgeAugmenting.encWalkCode T1 S1) : Turing.MultiTapeTM.ComputableInO (fun (x : γ) => { prepare := x0 x, cycle := x1 x }) encIn encBlossomCode (fun (x : γ) => T0 x + T1 x) fun (x : γ) => S0 x + S1 x

theorem Cslib.Complexity.CSP.EdgeSolver.NativeForest.encBlossomCode_cycle_inO : Turing.MultiTapeTM.ComputableInO BlossomCode.cycle encBlossomCode EdgeAugmenting.encWalkCode (fun (a : BlossomCode) => (encBlossomCode a).length) fun (a : BlossomCode) => (encBlossomCode a).length

theorem Cslib.Complexity.CSP.EdgeSolver.NativeForest.encBlossomCode_mk_polyTime {γ : Type} {encIn : γ ↪ List Bool} {x0 x1 : γ → EdgeAugmenting.WalkCode} (h0 : Turing.MultiTapeTM.ComputableInPolyTime x0 encIn EdgeAugmenting.encWalkCode) (h1 : Turing.MultiTapeTM.ComputableInPolyTime x1 encIn EdgeAugmenting.encWalkCode) : Turing.MultiTapeTM.ComputableInPolyTime (fun (x : γ) => { prepare := x0 x, cycle := x1 x }) encIn encBlossomCode

theorem Cslib.Complexity.CSP.EdgeSolver.NativeForest.encBlossomCode_cycle_budget {γ✝ : Type} {encIn✝ : γ✝ ↪ List Bool} {S✝ : γ✝ → ℕ} {g✝ : γ✝ → BlossomCode} : Turing.MultiTapeTM.ComputableInSpace g✝ encIn✝ encBlossomCode S✝ → Turing.MultiTapeTM.ComputableInSpace (fun (a : γ✝) => (g✝ a).cycle) encIn✝ EdgeAugmenting.encWalkCode S✝

def Cslib.Complexity.CSP.EdgeSolver.NativeForest.encBlossomCode : BlossomCode ↪ List Bool

The preparation walk is framed, followed by the cycle walk.

theorem Cslib.Complexity.CSP.EdgeSolver.NativeForest.encBlossomCode_prepare_deg : Turing.MultiTapeTM.ComputableInDegree BlossomCode.prepare encBlossomCode EdgeAugmenting.encWalkCode 1 1

@[simp]

theorem Cslib.Complexity.CSP.EdgeSolver.NativeForest.encBlossomCode_apply (a : BlossomCode) : encBlossomCode a = encBlossomCodeFields (a.prepare, a.cycle)

theorem Cslib.Complexity.CSP.EdgeSolver.NativeForest.encBlossomCode_mk_deg : Turing.MultiTapeTM.ComputableInDegree (fun (p : EdgeAugmenting.WalkCode × EdgeAugmenting.WalkCode) => { prepare := p.1, cycle := p.2 }) encBlossomCodeFields encBlossomCode 1 1

theorem Cslib.Complexity.CSP.EdgeSolver.NativeForest.encBlossomCode_mk_budget {γ : Type} {encIn : γ ↪ List Bool} {budget : γ → ℕ} {x0 x1 : γ → EdgeAugmenting.WalkCode} (h0 : Turing.MultiTapeTM.ComputableInSpace x0 encIn EdgeAugmenting.encWalkCode budget) (h1 : Turing.MultiTapeTM.ComputableInSpace x1 encIn EdgeAugmenting.encWalkCode budget) : Turing.MultiTapeTM.ComputableInSpace (fun (x : γ) => { prepare := x0 x, cycle := x1 x }) encIn encBlossomCode budget

@[reducible, inline]

abbrev Cslib.Complexity.CSP.EdgeSolver.NativeForest.encBlossomCodeFields : EdgeAugmenting.WalkCode × EdgeAugmenting.WalkCode ↪ List Bool

The tuple of the fields of encBlossomCode.

def Cslib.Complexity.CSP.EdgeSolver.NativeForest.append (p q : EdgeAugmenting.WalkCode) : EdgeAugmenting.WalkCode

Append two actual walks, preserving the first one's original start.

def Cslib.Complexity.CSP.EdgeSolver.NativeForest.meetingWalk (F : Logic.PL.CSP Logic.PL.CSP.Table ℕ) (m : EdgeForest.MeetingCode) : EdgeAugmenting.WalkCode

Candidate augmentation: the left ancestry, meeting pair, and reversed right ancestry.

def Cslib.Complexity.CSP.EdgeSolver.NativeForest.blossom (F : Logic.PL.CSP Logic.PL.CSP.Table ℕ) (m : EdgeForest.MeetingCode) : Option BlossomCode

Both actual LCA cases, including the final child-to-child pair for a copied-constraint LCA. Every scope lookup and prefix length is bounded by an actual list.

theorem Cslib.Complexity.CSP.EdgeSolver.NativeForest.ancestry_code {F : Logic.PL.CSP Logic.PL.CSP.Table ℕ} (es : Logic.PL.CSP.Forest.Log F) (v : ℕ) : ancestry F (List.map EdgeForest.codeExpansion es) v = { start := (es.ancestry v).walk.start, steps := (EdgeAugmenting.code (es.ancestry v).walk).steps, times := (es.ancestry v).times }

A single native backwards scan has exactly the source's chronological ancestry. No forest invariant, validity, width or edge-instance premise is needed for this bridge.

theorem Cslib.Complexity.CSP.EdgeSolver.NativeForest.meetingWalk_code {F : Logic.PL.CSP Logic.PL.CSP.Table ℕ} (m : Logic.PL.CSP.Forest.Meeting F) : meetingWalk F (EdgeForest.codeMeeting m) = EdgeAugmenting.code m.walk

The native ancestry compiler constructs the exact original augmenting walk.

theorem Cslib.Complexity.CSP.EdgeSolver.NativeForest.blossom_code {F : Logic.PL.CSP Logic.PL.CSP.Table ℕ} (m : Logic.PL.CSP.Forest.Meeting F) : blossom F (EdgeForest.codeMeeting m) = Option.map (fun (b : Logic.PL.CSP.Forest.BlossomData F) => { prepare := EdgeAugmenting.code b.prepare, cycle := EdgeAugmenting.code b.cycle }) m.blossomData

The native compiler retains the exact preparation and cycle of both source LCA cases. The metadata and mathematical invariant remain the existing Meeting.blossomData API.