Identifying variables at consecutive directed argument positions

The selected later variable corner and the predecessor of the earlier variable corner are cofacial by two literal face steps. The constructor merges precisely those outgoing blocks, then transports to the actual renamed CSP. Full target order and numerical-genus acceptance are derived internally. No cofaciality or target-planarity provider remains in this application. The construction is original and static; no native runtime bound is claimed here.

def Cslib.Complexity.CSP.identifyConsecutiveRotation {Rel V W : Type} [DecidableEq V] [DecidableEq W] (F : Logic.PL.CSP Rel V) (f : V → W) (o p : F.Occurrence) (hv : o.var ≠ p.var) (hkernel : ∀ a ∈ F.vars, ∀ b ∈ F.vars, f a = f b ↔ Function.update id p.var o.var a = Function.update id p.var o.var b) (rho : (incidenceGraph F).RotationSystem) : (incidenceGraph (Logic.PL.CSP.relabel f F)).RotationSystem

Merge the variable names of two selected occurrences at their directed corner blocks. The label map identifies exactly those names on the actual occurring set.

theorem Cslib.Complexity.CSP.numericalGenusZero_identifyConsecutiveRotation {Rel V W : Type} [DecidableEq V] [DecidableEq W] (F : Logic.PL.CSP Rel V) (f : V → W) (o p : F.Occurrence) (hv : o.var ≠ p.var) (hkernel : ∀ a ∈ F.vars, ∀ b ∈ F.vars, f a = f b ↔ Function.update id p.var o.var a = Function.update id p.var o.var b) (hp : argumentSuccessor p = o) (rho : (incidenceGraph F).RotationSystem) (hr : rho.NumericalGenusZero) (ho : RespectsArgumentOrder rho) : (identifyConsecutiveRotation F f o p hv hkernel rho).NumericalGenusZero

Ordered consecutive arguments internally discharge the cofaciality needed by the actual variable merge. Disconnected components, nullaries and points are handled by the generic numerical surgery and actual incidence transport.

theorem Cslib.Complexity.CSP.respectsArgumentOrder_identifyConsecutiveRotation {Rel V W : Type} [DecidableEq V] [DecidableEq W] (F : Logic.PL.CSP Rel V) (f : V → W) (o p : F.Occurrence) (hv : o.var ≠ p.var) (hkernel : ∀ a ∈ F.vars, ∀ b ∈ F.vars, f a = f b ↔ Function.update id p.var o.var a = Function.update id p.var o.var b) (rho : (incidenceGraph F).RotationSystem) (ho : RespectsArgumentOrder rho) : RespectsArgumentOrder (identifyConsecutiveRotation F f o p hv hkernel rho)

Both selected outgoing corners are variable ends, so original argument chirality survives the literal merge and the dense-name transport.

noncomputable def Cslib.Complexity.CSP.identifyConsecutiveCertificate {Rel V W : Type} [DecidableEq V] [DecidableEq W] (F : Logic.PL.CSP Rel V) (f : V → W) (o p : F.Occurrence) (hv : o.var ≠ p.var) (hkernel : ∀ a ∈ F.vars, ∀ b ∈ F.vars, f a = f b ↔ Function.update id p.var o.var a = Function.update id p.var o.var b) (c : Graph.RotationCertificate) (hrot : Graph.RotationCertificate.verifyRotation (incidenceGraph F) c = true) : Graph.RotationCertificate

Generate the target successor table from the supplied source table by actual corner identification. The source verification proof only decodes the supplied rotation.

theorem Cslib.Complexity.CSP.verifyRotationCertificate_identifyConsecutiveCertificate {Rel V W : Type} [DecidableEq V] [DecidableEq W] (F : Logic.PL.CSP Rel V) (f : V → W) (o p : F.Occurrence) (hv : o.var ≠ p.var) (hkernel : ∀ a ∈ F.vars, ∀ b ∈ F.vars, f a = f b ↔ Function.update id p.var o.var a = Function.update id p.var o.var b) (hp : argumentSuccessor p = o) (c : Graph.RotationCertificate) (hrot : Graph.RotationCertificate.verifyRotation (incidenceGraph F) c = true) (hc : verifyRotationCertificate F c = true) : verifyRotationCertificate (Logic.PL.CSP.relabel f F) (identifyConsecutiveCertificate F f o p hv hkernel c hrot) = true

Full target checker soundness, with the original positive argument cycles and internally derived numerical genus. No cofaciality or target-certificate premise is supplied by a caller.

theorem Cslib.Complexity.CSP.identifyConsecutiveCertificate_eq_swapSuccessors {Rel V W : Type} [DecidableEq V] [DecidableEq W] (F : Logic.PL.CSP Rel V) (f : V → W) (o p : F.Occurrence) (hv : o.var ≠ p.var) (hkernel : ∀ a ∈ F.vars, ∀ b ∈ F.vars, f a = f b ↔ Function.update id p.var o.var a = Function.update id p.var o.var b) (c : Graph.RotationCertificate) (hrot : Graph.RotationCertificate.verifyRotation (incidenceGraph F) c = true) : identifyConsecutiveCertificate F f o p hv hkernel c hrot = c.swapSuccessors (incidenceDart o false).index (List.idxOf (incidenceDart p false).index c.successor)

Exact full successor-table program for consecutive identification. The only selected predecessor is the actual inverse rotation of the earlier argument's variable end.