Native polynomial-time bounded orthogonal subdivision

Coordinates use the existing binary integer encoding. The per-segment step budget is unary; enumerating an unbounded binary-coordinate segment can require exponentially many output points. subdivideWithin_eq_subdivide recovers the full geometric subdivision when its budget suffices.

Main definitions

Uses the point and route encodings from Orthogonal.Encoding.

Main results

• Cslib.Orthogonal.computableInPolyTime_subdivideWithin: native plain polynomial-time computation of bounded subdivision with binary coordinates and unary budget.

References

This bounded compiler is an original construction.

theorem Cslib.Orthogonal.computableInPolyTime_subdivideWithin : Turing.MultiTapeTM.ComputableInPolyTime (fun (p : ℕ × Route) => subdivideWithin p.1 p.2) (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary encRoute) encRoute

Bounded unit enumeration is polynomial-time with binary coordinates and a unary budget. No orthogonality assumption is needed for the computational certificate. Geometric correctness for a sufficient budget is subdivideWithin_eq_subdivide.