Global Section Carry Criterion

Abstract

An additive section exists exactly when canonical carry is cancelled by section carry.

Theorem 1.1 (Section existence and canonical carry cancellation).

$$\forall X,B,q,r,hsection,\mathrm{AddCommGroup}\left(X\right)\wedge \mathrm{AddCommGroup}\left(B\right)\wedge q:\mathrm{AddMonoidHom}\left(X,B\right)\wedge r:B\to X\wedge hsection:\mathrm{RightInverse}\left(r,q\right)\wedge r(0)=0\Rightarrow \left(\exists s^{\prime }:\mathrm{AddMonoidHom}\left(B,X\right),\mathrm{RightInverse}\left(s^{\prime },q\right)\iff \exists beta:B\to \ker (q),\forall a,b\in B,\mathrm{kernelCarry}(q,r,hsection,a,b)+\mathrm{sectionCarry}(beta,a,b)=0\right)\wedge \left(\left(\neg \exists beta:B\to \ker (q),\forall a,b\in B,\mathrm{kernelCarry}(q,r,hsection,a,b)+\mathrm{sectionCarry}(beta,a,b)=0\right)\Rightarrow \left(\neg \exists s^{\prime }:\mathrm{AddMonoidHom}\left(B,X\right),\mathrm{RightInverse}\left(s^{\prime },q\right)\right)\right).$$

Proof. Machine-checked in Lean as D5/S1/Deficit/Cocycles/GlobalSectionCarryCriterion.global_section_iff_section_carry (✓ std3). ∎

Source. Repository-derived.

Commentary.

For additive commutative groups X and B, q is an additive quotient map and r is a normalized set-theoretic right inverse. The kernel-valued carry and the carry of beta are both instances of the repository’s canonical section-carry construction.

A homomorphic right-inverse section exists exactly when a kernel-valued change of section cancels the canonical carry. Consequently, absence of a cancellation witness rules out every additive section.

References

• Truth anchor: D5/S1/Deficit/Cocycles/GlobalSectionCarryCriterion.global_section_iff_section_carry
• Dependency: D5/S1/Deficit/Cocycles/AdditiveCarryCocycle