Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

Integer Rounding

Abstract

Concrete integer rounding for a possible direct cancellation of M_Z/B_Z. Truncated division has uniformly bounded additivity and binary-subdivision defects, independent of the integer and the denominator. These defects can therefore be absorbed in B_Z. This file does not yet construct the condensed null-sequence action or assert quotient vanishing. New proofs, Apache-2.0.

Theorem 1.1 (integer Rounding dyadic eventually zero).

Lean statement: D5/S3/HomologicalAlgebra/Solid/IntegerRounding.integerRounding_dyadic_eventually_zero

Proof. Machine-checked in Lean as D5/S3/HomologicalAlgebra/Solid/IntegerRounding.integerRounding_dyadic_eventually_zero (✓ std3). ∎

Source. Repository-derived.

Commentary.

The exact declaration is supplied by the compiled Lean source. Concrete integer rounding for a possible direct cancellation of M_Z/B_Z. Truncated division has uniformly bounded additivity and binary-subdivision defects, independent of the integer and the denominator. These defects can therefore be absorbed in B_Z. This file does not yet construct the condensed null-sequence action or assert quotient vanishing. New proofs, Apache-2.0.

Theorem 1.2 (integer Rounding preserves bound).

Lean statement: D5/S3/HomologicalAlgebra/Solid/IntegerRounding.integerRounding_preserves_bound

Proof. Machine-checked in Lean as D5/S3/HomologicalAlgebra/Solid/IntegerRounding.integerRounding_preserves_bound (✓ std3). ∎

Source. Repository-derived.

Commentary.

The exact declaration is supplied by the compiled Lean source. Concrete integer rounding for a possible direct cancellation of M_Z/B_Z. Truncated division has uniformly bounded additivity and binary-subdivision defects, independent of the integer and the denominator. These defects can therefore be absorbed in B_Z. This file does not yet construct the condensed null-sequence action or assert quotient vanishing. New proofs, Apache-2.0.

References

  • Truth anchor: D5/S3/HomologicalAlgebra/Solid/IntegerRounding.integerRounding_dyadic_eventually_zero
  • Truth anchor: D5/S3/HomologicalAlgebra/Solid/IntegerRounding.integerRounding_preserves_bound