Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

Measure Diagonal

Abstract

The actual diagonal/tail-difference identity, by a two-piece closed cover. This compares morphisms into the protected P itself; no injectivity of its map into integer measures is assumed. New proofs, Apache-2.0; research construction: Juan Esteban Rodríguez Camargo, Notes on Solid Geometry, Lemma 3.3.3.

Theorem 1.1 (measure Pointed Tail difference).

Lean statement: D5/S3/HomologicalAlgebra/Solid/MeasureDiagonal.measurePointedTail_difference

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

Source. Repository-derived.

Commentary.

The diagonal identity holds in free condensed P by genuine closed-cover joint epimorphy, not by testing coordinates of the integer-measure map.

Theorem 1.2 (bounded Coefficient Map unit Vectors).

Lean statement: D5/S3/HomologicalAlgebra/Solid/MeasureDiagonal.boundedCoefficientMap_unitVectors

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

Source. Repository-derived.

Commentary.

The coefficient map on the unit-vector family is its sole nonzero selector, with coefficients {0,1}.

References