Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

Measures

Abstract

The canonical measure map from the protected P to the countable product of discrete integers. This is the concrete map in Rodriguez Camargo, Notes on Solid Geometry, Lemmas 3.3.3–3.3.4. The proofs here are new, Apache-2.0. No realization or total-derived existence is assumed.

Theorem 1.1 (measure Numerator Coordinate relation).

Lean statement: D5/S3/HomologicalAlgebra/Solid/Measures.measureNumeratorCoordinate_relation

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

Source. Repository-derived.

Commentary.

The exact declaration is supplied by the compiled Lean source. The canonical measure map from the protected P to the countable product of discrete integers. This is the concrete map in Rodriguez Camargo, Notes on Solid Geometry, Lemmas 3.3.3–3.3.4. The proofs here are new, Apache-2.0. No realization or total-derived existence is assumed.

Theorem 1.2 (integer Measures solid).

Lean statement: D5/S3/HomologicalAlgebra/Solid/Measures.integerMeasures_solid

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

Source. Repository-derived.

Commentary.

The exact declaration is supplied by the compiled Lean source. The canonical measure map from the protected P to the countable product of discrete integers. This is the concrete map in Rodriguez Camargo, Notes on Solid Geometry, Lemmas 3.3.3–3.3.4. The proofs here are new, Apache-2.0. No realization or total-derived existence is assumed.

References