Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

Real Scalar Sequence

Abstract

The actual continuous real scalar null sequence needed by the binary cancellation argument for the bounded-real quotient. This is a function into topological R, not an assertion about modules over discrete R. New proofs, Apache-2.0. The scalar sequence is in Rodriguez Camargo, Notes on Solid Geometry, Proposition 3.2.5.

Theorem 1.1 (real Binary Depth tendsto).

Lean statement: D5/S3/HomologicalAlgebra/Solid/RealScalarSequence.realBinaryDepth_tendsto

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

Source. Repository-derived.

Commentary.

The binary depth tends to infinity; no bounded-index argument is used.

Theorem 1.2 (real Binary Weight tendsto).

Lean statement: D5/S3/HomologicalAlgebra/Solid/RealScalarSequence.realBinaryWeight_tendsto

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

Source. Repository-derived.

Commentary.

The exact declaration is supplied by the compiled Lean source. The actual continuous real scalar null sequence needed by the binary cancellation argument for the bounded-real quotient. This is a function into topological R, not an assertion about modules over discrete R. New proofs, Apache-2.0. The scalar sequence is in Rodriguez Camargo, Notes on Solid Geometry, Proposition 3.2.5.

References

  • Truth anchor: D5/S3/HomologicalAlgebra/Solid/RealScalarSequence.realBinaryDepth_tendsto
  • Truth anchor: D5/S3/HomologicalAlgebra/Solid/RealScalarSequence.realBinaryWeight_tendsto
  • Dependency: D5/S3/HomologicalAlgebra/Solid/Definitions