Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

Integer Null Sequence

Abstract

Actual locally constant rounding matrices on the convergent sequence times every light profinite test space. Their additive and binary defects are uniformly bounded, and bounded input remains bounded. These are concrete inputs for direct cancellation of M_Z/B_Z; no condensed action or vanishing is asserted here. New proofs, Apache-2.0.

Theorem 1.1 (integer Binary Round Matrix preserves bound).

Lean statement: D5/S3/HomologicalAlgebra/Solid/IntegerNullSequence.integerBinaryRoundMatrix_preserves_bound

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

Source. Repository-derived.

Commentary.

The exact declaration is supplied by the compiled Lean source. Actual locally constant rounding matrices on the convergent sequence times every light profinite test space. Their additive and binary defects are uniformly bounded, and bounded input remains bounded. These are concrete inputs for direct cancellation of M_Z/B_Z; no condensed action or vanishing is asserted here. New proofs, Apache-2.0.

Theorem 1.2 (integer Binary Round children defect).

Lean statement: D5/S3/HomologicalAlgebra/Solid/IntegerNullSequence.integerBinaryRound_children_defect

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

Source. Repository-derived.

Commentary.

The exact declaration is supplied by the compiled Lean source. Actual locally constant rounding matrices on the convergent sequence times every light profinite test space. Their additive and binary defects are uniformly bounded, and bounded input remains bounded. These are concrete inputs for direct cancellation of M_Z/B_Z; no condensed action or vanishing is asserted here. New proofs, Apache-2.0.

References