Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

Finite Approximation Tail

Abstract

The actual tail-remainder morphism P tensor free(S) -> free(S). Its finite row n is identity minus r_(n-1), and its infinity row is zero. Row zero is identity minus r_0; the finite initial quotient must therefore be retained in the final retract. No invalid enumeration or free(S)=P assertion is used. New proofs, Apache-2.0; Rodriguez Camargo, Notes on Solid Geometry, Lemma 3.3.2, with the finite initial contribution kept explicit.

Theorem 1.1 (finite Approximation Remainder Numerator relation).

Lean statement: D5/S3/HomologicalAlgebra/Solid/FiniteApproximationTail.finiteApproximationRemainderNumerator_relation

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

Source. Repository-derived.

Commentary.

The exact declaration is supplied by the compiled Lean source. The actual tail-remainder morphism P tensor free(S) -> free(S). Its finite row n is identity minus r_(n-1), and its infinity row is zero. Row zero is identity minus r_0; the finite initial quotient must therefore be retained in the final retract. No invalid enumeration or free(S)=P assertion is used. New proofs, Apache-2.0; Rodriguez Camargo, Notes on Solid Geometry, Lemma 3.3.2, with the finite initial contribution kept explicit.

Theorem 1.2 (finite Approximation Row Section remainder).

Lean statement: D5/S3/HomologicalAlgebra/Solid/FiniteApproximationTail.finiteApproximationRowSection_remainder

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

Source. Repository-derived.

Commentary.

The exact declaration is supplied by the compiled Lean source. The actual tail-remainder morphism P tensor free(S) -> free(S). Its finite row n is identity minus r_(n-1), and its infinity row is zero. Row zero is identity minus r_0; the finite initial quotient must therefore be retained in the final retract. No invalid enumeration or free(S)=P assertion is used. New proofs, Apache-2.0; Rodriguez Camargo, Notes on Solid Geometry, Lemma 3.3.2, with the finite initial contribution kept explicit.

References