Native polynomial-time point arithmetic

Polynomial-time certificates for the binary-coordinate point operations shared by the orthogonal subdivision compiler and the exact-one and paired planar drawing compilers. They are not global @[fun_prop] rules, since their encodings are fixed; clients that compose them add them with attribute [local fun_prop].

Main results

• Cslib.Orthogonal.computableInPolyTime_pointAdd: adding two points.
• Cslib.Orthogonal.computableInPolyTime_direction: the unit direction between two points.
• Cslib.Orthogonal.computableInPolyTime_translate: translating a route by a point.

theorem Cslib.Orthogonal.computableInPolyTime_pointAdd : Turing.MultiTapeTM.ComputableInPolyTime (fun (p : Point × Point) => p.1 + p.2) (Turing.MultiTapeTM.encPair encPoint encPoint) encPoint

Adding two binary-coordinate points is native polynomial-time.

theorem Cslib.Orthogonal.computableInPolyTime_direction : Turing.MultiTapeTM.ComputableInPolyTime (fun (p : Point × Point) => direction p.1 p.2) (Turing.MultiTapeTM.encPair encPoint encPoint) encPoint

The unit direction from one binary-coordinate point to another is native polynomial-time.

theorem Cslib.Orthogonal.computableInPolyTime_translate : Turing.MultiTapeTM.ComputableInPolyTime (fun (p : Point × Route) => translate p.1 p.2) (Turing.MultiTapeTM.encPair encPoint encRoute) encRoute

Translating a route by a point is native polynomial-time.