Local-to-global actual variable position lookup

Main results

• positiveVariablePoint_profile_auxiliary: a private local profile variable resolves to its prescribed actual clause-box point.

References

This is an elementary consequence of the actual finite position-table construction.

theorem Cslib.Complexity.SAT.ExactOne.positiveVariablePoint_profile_auxiliary (φ : Logic.PL.CNF ℕ) (d : Graph.OrthogonalDrawing) {c : Logic.PL.Clause ℕ} {i : ℕ} (hci : (c, i) ∈ List.zipIdx φ) {w : Logic.PL.CNF.PositiveExactOneCompile.Variable ℕ} {j : ℕ} (hwj : (w, j) ∈ (profileVariables (clauseProfile c)).zipIdx) (ha : ∀ (n : ℕ), w ≠ Sum.inl (Sum.inl n)) : positiveVariablePoint φ d (profileVariableMap i (Logic.PL.CNF.PositiveExactOneCompile.signedOffset φ i) c w) = positiveBoxOrigin φ d i + (clauseGeometry φ d i c).variablePosition j

A local private variable resolves to its own point in the original clause's actual box.

theorem Cslib.Complexity.SAT.ExactOne.positiveVariablePoint_profile_auxiliary_getD (φ : Logic.PL.CNF ℕ) (d : Graph.OrthogonalDrawing) {c : Logic.PL.Clause ℕ} {i : ℕ} (hci : (c, i) ∈ List.zipIdx φ) {j : ℕ} (hj : j < (profileVariables (clauseProfile c)).length) (ha : ∀ (n : ℕ), (profileVariables (clauseProfile c)).getD j (Sum.inl (Sum.inl 0)) ≠ Sum.inl (Sum.inl n)) : positiveVariablePoint φ d (profileVariableMap i (Logic.PL.CNF.PositiveExactOneCompile.signedOffset φ i) c ((profileVariables (clauseProfile c)).getD j (Sum.inl (Sum.inl 0)))) = positiveBoxOrigin φ d i + (clauseGeometry φ d i c).variablePosition j

Indexed lookup of an actual local private variable has its prescribed actual point.