Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

Finite Approximation Differences

Abstract

The actual compact light-profinite parameter space for the representative differences used in the generator retract. Every finite fiber is the stated pair of representatives, and every infinity fiber is diagonal. Projection onto the convergent sequence is surjective. No ordinary/derived free descent or realization is asserted in this topology module. New proofs, Apache-2.0; Rodriguez Camargo, Notes on Solid Geometry, Lemma 3.3.2. The closure/fiber proof follows the accepted immutable CWComparison.BinaryEdgeSpace pattern; no frozen source is modified.

Theorem 1.1 (finite Approximation Difference infty fiber).

Lean statement: D5/S3/HomologicalAlgebra/Solid/FiniteApproximationDifferences.finiteApproximationDifference_infty_fiber

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

Source. Repository-derived.

Commentary.

The exact declaration is supplied by the compiled Lean source. The actual compact light-profinite parameter space for the representative differences used in the generator retract. Every finite fiber is the stated pair of representatives, and every infinity fiber is diagonal. Projection onto the convergent sequence is surjective. No ordinary/derived free descent or realization is asserted in this topology module. New proofs, Apache-2.0; Rodriguez Camargo, Notes on Solid Geometry, Lemma 3.3.2. The closure/fiber proof follows the accepted immutable CWComparison.BinaryEdgeSpace pattern; no frozen source is modified.

Theorem 1.2 (finite Approximation Difference Projection surjective).

Lean statement: D5/S3/HomologicalAlgebra/Solid/FiniteApproximationDifferences.finiteApproximationDifferenceProjection_surjective

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

Source. Repository-derived.

Commentary.

The exact declaration is supplied by the compiled Lean source. The actual compact light-profinite parameter space for the representative differences used in the generator retract. Every finite fiber is the stated pair of representatives, and every infinity fiber is diagonal. Projection onto the convergent sequence is surjective. No ordinary/derived free descent or realization is asserted in this topology module. New proofs, Apache-2.0; Rodriguez Camargo, Notes on Solid Geometry, Lemma 3.3.2. The closure/fiber proof follows the accepted immutable CWComparison.BinaryEdgeSpace pattern; no frozen source is modified.

References