Joining the two structural probe centers

The source rows are left body, left probe, right body, right probe. Target rows are left body, right body, one probe with right scope followed by left scope. Every old argument occurrence is retained at its explicit target position. The two probe centers are the only constraint fibers identified. These are positional constructions on the actual CSP lists.

noncomputable def Cslib.Complexity.CSP.scopeJoinSourceEquiv {Rel V : Type} {m n : ℕ} (F H : Logic.PL.CSP Rel V) (r : Rel) (x : Fin m → V) (y : Fin n → V) : (F.Occurrence ⊕ Fin m) ⊕ H.Occurrence ⊕ Fin n ≃ (F ++ [(r, List.ofFn x)] ++ (H ++ [(r, List.ofFn y)])).Occurrence

Source coordinates for two bodies, each followed by its own probe scope.

noncomputable def Cslib.Complexity.CSP.scopeJoinTargetEquiv {Rel V : Type} {m n : ℕ} (F H : Logic.PL.CSP Rel V) (r : Rel) (x : Fin m → V) (y : Fin n → V) : (F.Occurrence ⊕ Fin m) ⊕ H.Occurrence ⊕ Fin n ≃ (F ++ H ++ [(r, List.ofFn fun (i : Fin (n + m)) => Fin.addCases y x i)]).Occurrence

Target coordinates retain both body blocks and put right probe arguments before left. The concatenated scope has the same positive cyclic orientation after the center splice.

noncomputable def Cslib.Complexity.CSP.scopeJoinOccurrenceEquiv {Rel V : Type} {m n : ℕ} (F H : Logic.PL.CSP Rel V) (r : Rel) (x : Fin m → V) (y : Fin n → V) : (F ++ [(r, List.ofFn x)] ++ (H ++ [(r, List.ofFn y)])).Occurrence ≃ (F ++ H ++ [(r, List.ofFn fun (i : Fin (n + m)) => Fin.addCases y x i)]).Occurrence

Every source edge occurrence has its exact target occurrence in the joined-scope body.

theorem Cslib.Complexity.CSP.record_scopeJoinSourceEquiv {Rel V : Type} {m n : ℕ} (F H : Logic.PL.CSP Rel V) (r : Rel) (x : Fin m → V) (y : Fin n → V) (a : (F.Occurrence ⊕ Fin m) ⊕ H.Occurrence ⊕ Fin n) : ((scopeJoinSourceEquiv F H r x y) a).record = match a with | Sum.inl (Sum.inl o) => o.record | Sum.inl (Sum.inr i) => (List.length F, ↑i, x i) | Sum.inr (Sum.inl o) => (List.length F + 1 + ↑o.fst, ↑o.snd, o.var) | Sum.inr (Sum.inr i) => (List.length F + 1 + List.length H, ↑i, y i)

Full source records in the four literal body/probe blocks.

theorem Cslib.Complexity.CSP.record_scopeJoinTargetEquiv {Rel V : Type} {m n : ℕ} (F H : Logic.PL.CSP Rel V) (r : Rel) (x : Fin m → V) (y : Fin n → V) (a : (F.Occurrence ⊕ Fin m) ⊕ H.Occurrence ⊕ Fin n) : ((scopeJoinTargetEquiv F H r x y) a).record = match a with | Sum.inl (Sum.inl o) => o.record | Sum.inl (Sum.inr i) => (List.length F + List.length H, n + ↑i, x i) | Sum.inr (Sum.inl o) => (List.length F + ↑o.fst, ↑o.snd, o.var) | Sum.inr (Sum.inr i) => (List.length F + List.length H, ↑i, y i)

Full target records retain original body order and the specified right-then-left probe.

theorem Cslib.Complexity.CSP.var_scopeJoinOccurrenceEquiv {Rel V : Type} {m n : ℕ} (F H : Logic.PL.CSP Rel V) (r : Rel) (x : Fin m → V) (y : Fin n → V) (o : (F ++ [(r, List.ofFn x)] ++ (H ++ [(r, List.ofFn y)])).Occurrence) : ((scopeJoinOccurrenceEquiv F H r x y) o).var = o.var

The occurrence map leaves every actual variable label unchanged.

theorem Cslib.Complexity.CSP.constraint_scopeJoinOccurrenceEquiv {Rel V : Type} {m n : ℕ} (F H : Logic.PL.CSP Rel V) (r : Rel) (x : Fin m → V) (y : Fin n → V) (o p : (F ++ [(r, List.ofFn x)] ++ (H ++ [(r, List.ofFn y)])).Occurrence) : ((scopeJoinOccurrenceEquiv F H r x y) o).fst = ((scopeJoinOccurrenceEquiv F H r x y) p).fst ↔ Function.update id (List.length F + 1 + List.length H) (List.length F) ↑o.fst = Function.update id (List.length F + 1 + List.length H) (List.length F) ↑p.fst

The target constraint fibers are exactly the source fibers with the two probe centers identified. This guard is about positions, including list-identical rows and nullaries.

theorem Cslib.Complexity.CSP.argumentSuccessor_scopeJoinOccurrenceEquiv {Rel V : Type} {m n : ℕ} (F H : Logic.PL.CSP Rel V) (r : Rel) (x : Fin (m + 1) → V) (y : Fin (n + 1) → V) (o : (F ++ [(r, List.ofFn x)] ++ (H ++ [(r, List.ofFn y)])).Occurrence) : (scopeJoinOccurrenceEquiv F H r x y) (argumentSuccessor ((Equiv.swap ((scopeJoinSourceEquiv F H r x y) (Sum.inl (Sum.inr (Fin.last m)))) ((scopeJoinSourceEquiv F H r x y) (Sum.inr (Sum.inr (Fin.last n))))) o)) = argumentSuccessor ((scopeJoinOccurrenceEquiv F H r x y) o)

Joining the last outgoing corner at each probe center gives exactly the target positive argument cycles, with no reflected scope or arbitrary all-port conjunction principle.

noncomputable def Cslib.Complexity.CSP.scopeJoinRotation {Rel V : Type} {m n : ℕ} [DecidableEq V] (F H : Logic.PL.CSP Rel V) (r : Rel) (x : Fin (m + 1) → V) (y : Fin (n + 1) → V) (hd : (F ++ [(r, List.ofFn x)]).vars.Disjoint (H ++ [(r, List.ofFn y)]).vars) (rho : (incidenceGraph (F ++ [(r, List.ofFn x)])).RotationSystem) (tau : (incidenceGraph (H ++ [(r, List.ofFn y)])).RotationSystem) : (incidenceGraph (F ++ H ++ [(r, List.ofFn fun (i : Fin (n + 1 + (m + 1))) => Fin.addCases y x i)])).RotationSystem

Join the two actual probe centers at their last outgoing corners. Both probe scopes are nonempty, so their actual constraint darts supply the corners even for empty bodies.

theorem Cslib.Complexity.CSP.numericalGenusZero_scopeJoinRotation {Rel V : Type} {m n : ℕ} [DecidableEq V] (F H : Logic.PL.CSP Rel V) (r : Rel) (x : Fin (m + 1) → V) (y : Fin (n + 1) → V) (hd : (F ++ [(r, List.ofFn x)]).vars.Disjoint (H ++ [(r, List.ofFn y)]).vars) (rho : (incidenceGraph (F ++ [(r, List.ofFn x)])).RotationSystem) (tau : (incidenceGraph (H ++ [(r, List.ofFn y)])).RotationSystem) (hr : rho.NumericalGenusZero) (hs : tau.NumericalGenusZero) : (scopeJoinRotation F H r x y hd rho tau).NumericalGenusZero

Different components are derived from the actual disjoint source supports. The target genus is proved from the two source genera and the literal center splice.

theorem Cslib.Complexity.CSP.respectsArgumentOrder_scopeJoinRotation {Rel V : Type} {m n : ℕ} [DecidableEq V] (F H : Logic.PL.CSP Rel V) (r : Rel) (x : Fin (m + 1) → V) (y : Fin (n + 1) → V) (hd : (F ++ [(r, List.ofFn x)]).vars.Disjoint (H ++ [(r, List.ofFn y)]).vars) (rho : (incidenceGraph (F ++ [(r, List.ofFn x)])).RotationSystem) (tau : (incidenceGraph (H ++ [(r, List.ofFn y)])).RotationSystem) (hr : RespectsArgumentOrder rho) (hs : RespectsArgumentOrder tau) : RespectsArgumentOrder (scopeJoinRotation F H r x y hd rho tau)

Every original body constraint keeps its directed order, and the two probe cycles become the precise positive cyclic concatenation specified by the target scope.

theorem Cslib.Complexity.CSP.verifyRotationCertificate_scopeJoinRotation {Rel V : Type} {m n : ℕ} [DecidableEq V] (F H : Logic.PL.CSP Rel V) (r : Rel) (x : Fin (m + 1) → V) (y : Fin (n + 1) → V) (hd : (F ++ [(r, List.ofFn x)]).vars.Disjoint (H ++ [(r, List.ofFn y)]).vars) (rho : (incidenceGraph (F ++ [(r, List.ofFn x)])).RotationSystem) (tau : (incidenceGraph (H ++ [(r, List.ofFn y)])).RotationSystem) (hr : rho.NumericalGenusZero) (hs : tau.NumericalGenusZero) (hor : RespectsArgumentOrder rho) (hos : RespectsArgumentOrder tau) : verifyRotationCertificate (F ++ H ++ [(r, List.ofFn fun (i : Fin (n + 1 + (m + 1))) => Fin.addCases y x i)]) (Graph.RotationCertificate.ofRotation (scopeJoinRotation F H r x y hd rho tau)) = true

The full target checker accepts the actual joined-scope table from source ordered numerical rotations, without a target certificate or genus premise.