Division and remainder of unary counters

A quotient/remainder loop scans the unary dividend and captures the divisor. One invariant proves its arithmetic specification and the linear bound on encoded intermediate states, including divisor zero. The fixed-divisor interface follows by composition.

Main results

• Turing.MultiTapeTM.ComputableTidilyInPolyTime.unary_divMod: compute quotient and remainder.
• Turing.MultiTapeTM.ComputableTidilyInPolyTime.unary_div, .unary_mod: project either result.
• Turing.MultiTapeTM.ComputableTidilyInPolyTime.unary_div_const: division by a fixed natural.
• Turing.MultiTapeTM.ComputableInPolyTime.unary_div', .unary_mod': composition rules for fun_prop on plain certificates.

References

The machine realization uses the invariant-based loop calculus in PolyTime.Iteration.

theorem Turing.MultiTapeTM.ComputableTidilyInPolyTime.unary_divMod : ComputableTidilyInPolyTime (fun (p : ℕ × ℕ) => (p.1 / p.2, p.1 % p.2)) (encPair encUnary encUnary) (encPair encUnary encUnary)

Compute both quotient and remainder with a runtime unary divisor. Division by zero returns (0, dividend), matching Lean's conventions. All intermediate counters have linear size.

theorem Turing.MultiTapeTM.ComputableTidilyInPolyTime.unary_div : ComputableTidilyInPolyTime (fun (p : ℕ × ℕ) => p.1 / p.2) (encPair encUnary encUnary) encUnary

Division of two unary counters.

theorem Turing.MultiTapeTM.ComputableTidilyInPolyTime.unary_mod : ComputableTidilyInPolyTime (fun (p : ℕ × ℕ) => p.1 % p.2) (encPair encUnary encUnary) encUnary

Remainder of two unary counters.

theorem Turing.MultiTapeTM.ComputableTidilyInPolyTime.unary_div_const (divisor : ℕ) : ComputableTidilyInPolyTime (fun (n : ℕ) => n / divisor) encUnary encUnary

Division by a fixed natural is a special case of runtime unary division.

theorem Turing.MultiTapeTM.ComputableInPolyTime.unary_div : ComputableInPolyTime (fun (p : ℕ × ℕ) => p.1 / p.2) (encPair encUnary encUnary) encUnary

Division of two unary counters, including divisor zero.

theorem Turing.MultiTapeTM.ComputableInPolyTime.unary_mod : ComputableInPolyTime (fun (p : ℕ × ℕ) => p.1 % p.2) (encPair encUnary encUnary) encUnary

Remainder of two unary counters, including divisor zero.

theorem Turing.MultiTapeTM.ComputableInPolyTime.unary_div' {α : Type} {input : α ↪ List Bool} {left right : α → ℕ} (hleft : ComputableInPolyTime left input encUnary) (hright : ComputableInPolyTime right input encUnary) : ComputableInPolyTime (fun (a : α) => left a / right a) input encUnary

Divide two computed unary naturals with the same full input context.

theorem Turing.MultiTapeTM.ComputableInPolyTime.unary_mod' {α : Type} {input : α ↪ List Bool} {left right : α → ℕ} (hleft : ComputableInPolyTime left input encUnary) (hright : ComputableInPolyTime right input encUnary) : ComputableInPolyTime (fun (a : α) => left a % right a) input encUnary

Take the remainder of two computed unary naturals with the same full input context.

theorem Turing.MultiTapeTM.ComputableInPolyTime.unary_divMod : ComputableInPolyTime (fun (p : ℕ × ℕ) => (p.1 / p.2, p.1 % p.2)) (encPair encUnary encUnary) (encPair encUnary encUnary)

Compute both quotient and remainder with a runtime unary divisor. Division by zero returns (0, dividend), matching Lean's conventions. All intermediate counters have linear size.

theorem Turing.MultiTapeTM.ComputableInPolyTime.unary_div_const (divisor : ℕ) : ComputableInPolyTime (fun (n : ℕ) => n / divisor) encUnary encUnary

Division by a fixed natural is a special case of runtime unary division.