Measure Ordinary Reflection

Abstract

Compatibility of the actual canonical P-measure computation with the protected ordinary reflection unit. This does not assert DSolid realization, derived full faithfulness or the existence of an unbounded derived adjunction. New proofs, Apache-2.0; the generator route follows Rodriguez Camargo, Notes on Solid Geometry, Theorem 3.3.1.

Theorem 1.1 (solid PTo Integer Measures unit).

Lean statement: D5/S3/HomologicalAlgebra/Solid/MeasureOrdinaryReflection.solidPToIntegerMeasures_unit

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

Source. Repository-derived.

Commentary.

The exact declaration is supplied by the compiled Lean source. Compatibility of the actual canonical P-measure computation with the protected ordinary reflection unit. This does not assert DSolid realization, derived full faithfulness or the existence of an unbounded derived adjunction. New proofs, Apache-2.0; the generator route follows Rodriguez Camargo, Notes on Solid Geometry, Theorem 3.3.1.

Theorem 1.2 (solid PTo Integer Measures is Iso).

Lean statement: D5/S3/HomologicalAlgebra/Solid/MeasureOrdinaryReflection.solidPToIntegerMeasures_isIso

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

Source. Repository-derived.

Commentary.

The exact declaration is supplied by the compiled Lean source. Compatibility of the actual canonical P-measure computation with the protected ordinary reflection unit. This does not assert DSolid realization, derived full faithfulness or the existence of an unbounded derived adjunction. New proofs, Apache-2.0; the generator route follows Rodriguez Camargo, Notes on Solid Geometry, Theorem 3.3.1.

Definition 1.3 (solid PInteger Measures Iso).

Lean statement: D5/S3/HomologicalAlgebra/Solid/MeasureOrdinaryReflection.solidPIntegerMeasuresIso

Formalization. D5/S3/HomologicalAlgebra/Solid/MeasureOrdinaryReflection.solidPIntegerMeasuresIso (✓ std3).

Source. Repository-derived.

Commentary.

The exact declaration is supplied by the compiled Lean source. Compatibility of the actual canonical P-measure computation with the protected ordinary reflection unit. This does not assert DSolid realization, derived full faithfulness or the existence of an unbounded derived adjunction. New proofs, Apache-2.0; the generator route follows Rodriguez Camargo, Notes on Solid Geometry, Theorem 3.3.1.

References

• Truth anchor: D5/S3/HomologicalAlgebra/Solid/MeasureOrdinaryReflection.solidPIntegerMeasuresIso
• Truth anchor: D5/S3/HomologicalAlgebra/Solid/MeasureOrdinaryReflection.solidPToIntegerMeasures_isIso
• Truth anchor: D5/S3/HomologicalAlgebra/Solid/MeasureOrdinaryReflection.solidPToIntegerMeasures_unit
• Dependency: D5/S3/HomologicalAlgebra/Solid/MeasureComparisonConstruction