Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

Bounded Measure Comparison

Abstract

The concrete bounded tail, descent and two-sided inverse of the protected P-measure unit in the derived-local reflector. Exact proofs are retained from the reviewed constructor at its existing component boundary. Apache-2.0; research construction: Juan Esteban Rodríguez Camargo, Notes on Solid Geometry, Lemma 3.3.3.

Theorem 1.1 (Bounded tail tensor square).

Lean statement: D5/S3/HomologicalAlgebra/Solid/MeasureComparisonBounded.boundedMeasureTail_tensorSquare

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

Source. Repository-derived.

Commentary.

The actual bounded tail descends through the defining finite-difference tensor square, supplying the first inverse identity.

Definition 1.2 (Derived-local bounded measure equivalence).

Lean statement: D5/S3/HomologicalAlgebra/Solid/MeasureComparisonBounded.localBoundedMeasureIso

Formalization. D5/S3/HomologicalAlgebra/Solid/MeasureComparisonBounded.localBoundedMeasureIso (✓ std3).

Source. Repository-derived.

Commentary.

The genuine two-sided inverse identifies the reflected protected P with the reflected bounded integer measures. The integer-quotient continuation consumes this equivalence.

References