Retaining a deterministic coordinate of the right state

This lift records the original right variable alongside a deterministic coordinate. Replacing the coordinate in a proof may preserve the original right marginal while changing its correlation with that coordinate.

noncomputable def Algebraic.Cutwidth.Extractor.rightCoordinateLift {Z : Type u_1} {B : Type u_2} {Q : Type u_3} [Fintype B] (r : Z → B → ℝ) (q : Z → B → Q) (z : Z) : B × Q → ℝ

Append a deterministic coordinate without discarding any original right-side information.

Equations

• Algebraic.Cutwidth.Extractor.rightCoordinateLift r q z = Algebraic.Cutwidth.Extractor.mapWeight (fun (b : B) => (b, q z b)) (r z)