Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

Measure Selectors

Abstract

The concrete bounded-coefficient tensor square for the measure comparison. For every light profinite test space S and every uniformly finite-range family of integer coordinates, construct the map P tensor Z[S] -> P by selecting finite points in the convergent sequence. This works for empty, finite and infinite S. The uniform bound is essential; no bound is imposed on the number of coordinates. New proofs, Apache-2.0, following the construction in Rodriguez Camargo, Notes on Solid Geometry, Lemma 3.3.3.

Theorem 1.1 (coefficient Selector Fun fiber clopen).

Lean statement: D5/S3/HomologicalAlgebra/Solid/MeasureSelectors.coefficientSelectorFun_fiber_clopen

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

Source. Repository-derived.

Commentary.

The exact declaration is supplied by the compiled Lean source. The concrete bounded-coefficient tensor square for the measure comparison. For every light profinite test space S and every uniformly finite-range family of integer coordinates, construct the map P tensor Z[S] -> P by selecting finite points in the convergent sequence. This works for empty, finite and infinite S. The uniform bound is essential; no bound is imposed on the number of coordinates. New proofs, Apache-2.0, following the construction in Rodriguez Camargo, Notes on Solid Geometry, Lemma 3.3.3.

Theorem 1.2 (coefficient Selector Fun continuous).

Lean statement: D5/S3/HomologicalAlgebra/Solid/MeasureSelectors.coefficientSelectorFun_continuous

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

Source. Repository-derived.

Commentary.

Continuity at infinity uses only preservation of the finite index: every output is either the input index or infinity. No convergence of c_n is needed.

References

  • Truth anchor: D5/S3/HomologicalAlgebra/Solid/MeasureSelectors.coefficientSelectorFun_continuous
  • Truth anchor: D5/S3/HomologicalAlgebra/Solid/MeasureSelectors.coefficientSelectorFun_fiber_clopen
  • Dependency: D5/S3/HomologicalAlgebra/Solid/DiscreteInt