Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

Measure Tails

Abstract

The actual protected-P tail map needed for the two-sided bounded-measure inverse: F_P(e_n tensor e_j) = e_j if n <= j, and zero otherwise. The pointed map is continuous and vanishes on both infinity fibers, so it descends through both exact protected cokernels. Its zeroth-row section is proved, rather than assumed. New proofs, Apache-2.0; the construction is in Rodriguez Camargo’s Notes on Solid Geometry, Lemma 3.3.3, and the checked immutable realization response supplied by root.

Theorem 1.1 (measure PTail Zero Numerator relation).

Lean statement: D5/S3/HomologicalAlgebra/Solid/MeasureTails.measurePTailZeroNumerator_relation

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

Source. Repository-derived.

Commentary.

The exact declaration is supplied by the compiled Lean source. The actual protected-P tail map needed for the two-sided bounded-measure inverse: F_P(e_n tensor e_j) = e_j if n <= j, and zero otherwise. The pointed map is continuous and vanishes on both infinity fibers, so it descends through both exact protected cokernels. Its zeroth-row section is proved, rather than assumed. New proofs, Apache-2.0; the construction is in Rodriguez Camargo’s Notes on Solid Geometry, Lemma 3.3.3, and the checked immutable realization response supplied by root.

Theorem 1.2 (measure PTail Section tail).

Lean statement: D5/S3/HomologicalAlgebra/Solid/MeasureTails.measurePTailSection_tail

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

Source. Repository-derived.

Commentary.

F_P epsilon_P = 1, the second inverse identity required by the bounded measure argument. This is an actual equality of condensed morphisms.

References