Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

Measure Comparison Construction

Abstract

Concrete bounded inverse, dyadic integer-quotient cancellation and canonical P-measure comparison. The bounded inverse and integer-quotient continuation are separate compilation units at their existing component boundary. All new proofs are Apache-2.0. Research construction: Juan Esteban Rodriguez Camargo, Notes on Solid Geometry, Lemmas 3.3.3–3.3.4. Immutable formal suppliers retain their source/commit/license identities. No DSolid realization or original HasLeftDerivedFunctor/derived adjunction is assumed.

Theorem 1.1 (local PTo Integer Measures is Iso).

Lean statement: D5/S3/HomologicalAlgebra/Solid/MeasureComparisonConstruction.localPToIntegerMeasures_isIso

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

Source. Repository-derived.

Commentary.

The required concrete P-measure computation is unconditional. It is an equivalence in Dlocal, and does not identify Dlocal with DSolid.

Definition 1.2 (local Integer Measure Iso).

Lean statement: D5/S3/HomologicalAlgebra/Solid/MeasureComparisonConstruction.localIntegerMeasureIso

Formalization. D5/S3/HomologicalAlgebra/Solid/MeasureComparisonConstruction.localIntegerMeasureIso (✓ std3).

Source. Repository-derived.

Commentary.

The exact declaration is supplied by the compiled Lean source. Concrete bounded inverse, dyadic integer-quotient cancellation and canonical P-measure comparison. The bounded inverse and integer-quotient continuation are separate compilation units at their existing component boundary. All new proofs are Apache-2.0. Research construction: Juan Esteban Rodriguez Camargo, Notes on Solid Geometry, Lemmas 3.3.3–3.3.4. Immutable formal suppliers retain their source/commit/license identities. No DSolid realization or original HasLeftDerivedFunctor/derived adjunction is assumed.

References