Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

Finite Approximation Index

Abstract

Actual countable indexing and finite stage bounds for the coefficient selector in the free-profinite generator retract. An injection into N is sufficient: no bijection with N is claimed for finite or empty S. New proofs, Apache-2.0. Research construction: Rodriguez Camargo, Notes on Solid Geometry, Lemma 3.3.2.

Theorem 1.1 (finite Approximation Index Code injective).

Lean statement: D5/S3/HomologicalAlgebra/Solid/FiniteApproximationIndex.finiteApproximationIndexCode_injective

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

Source. Repository-derived.

Commentary.

The exact declaration is supplied by the compiled Lean source. Actual countable indexing and finite stage bounds for the coefficient selector in the free-profinite generator retract. An injection into N is sufficient: no bijection with N is claimed for finite or empty S. New proofs, Apache-2.0. Research construction: Rodriguez Camargo, Notes on Solid Geometry, Lemma 3.3.2.

Theorem 1.2 (finite Approximation Index stage le bound).

Lean statement: D5/S3/HomologicalAlgebra/Solid/FiniteApproximationIndex.finiteApproximationIndex_stage_le_bound

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

Source. Repository-derived.

Commentary.

The exact declaration is supplied by the compiled Lean source. Actual countable indexing and finite stage bounds for the coefficient selector in the free-profinite generator retract. An injection into N is sufficient: no bijection with N is claimed for finite or empty S. New proofs, Apache-2.0. Research construction: Rodriguez Camargo, Notes on Solid Geometry, Lemma 3.3.2.

References

  • Truth anchor: D5/S3/HomologicalAlgebra/Solid/FiniteApproximationIndex.finiteApproximationIndexCode_injective
  • Truth anchor: D5/S3/HomologicalAlgebra/Solid/FiniteApproximationIndex.finiteApproximationIndex_stage_le_bound
  • Dependency: D5/S3/HomologicalAlgebra/Solid/FiniteApproximation