Branch 1 assembly: the unconditional SphereSuspensionTower

This file assembles the two Mayer–Vietoris ingredients proved in the previous modules into a single concrete, unconditional term of type SphereSuspensionTower:

• the base case sphereTopHomologyIsoOne : SphereTopHomologyIso 1 (i.e. H₁(S¹; ℤ) ≅ ℤ), from SphereHomologyS1BaseMV.lean, and
• the recursive step sphereTopHomologyStepMV : Hₙ₊₁(Sⁿ⁺¹; ℤ) ≅ Hₙ(Sⁿ; ℤ) (n ≥ 1), from SphereHomologyMVStep.lean.

The tower is constructed from the exported Mayer--Vietoris results. Downstream files may import this file and use sphereSuspensionTowerFromMV (or its aliases) to obtain

/-! # Sphere Suspension Tower From MV -/ the full positive-dimensional sphere top-homology family and orientation data.

noncomputable def SphereOddDegree.sphereSuspensionTowerFromMV : SphereSuspensionTower

The unconditional sphere suspension tower, assembled from the Mayer–Vietoris base case sphereTopHomologyIsoOne and the Mayer–Vietoris recursive step sphereTopHomologyStepMV.

Equations

• SphereOddDegree.sphereSuspensionTowerFromMV = { base := SphereOddDegree.sphereTopHomologyIsoOne, step := fun (n : ℕ) (hn : 1 ≤ n) => SphereOddDegree.sphereTopHomologyStepMV n hn }

noncomputable def SphereOddDegree.sphereSuspensionTowerUnconditional : SphereSuspensionTower

Compatibility alias: the unconditional suspension tower.

Equations

• SphereOddDegree.sphereSuspensionTowerUnconditional = SphereOddDegree.sphereSuspensionTowerFromMV

noncomputable def SphereOddDegree.branch1SphereSuspensionTower : SphereSuspensionTower

Compatibility alias: the Branch 1 suspension tower.

Equations

• SphereOddDegree.branch1SphereSuspensionTower = SphereOddDegree.sphereSuspensionTowerFromMV

noncomputable def SphereOddDegree.sphereOrientationPosFromMV : SphereOrientationPos

From the unconditional suspension tower, the genuine positive-dimensional sphere orientation SphereOrientationPos.

Equations

• SphereOddDegree.sphereOrientationPosFromMV = SphereOddDegree.sphereSuspensionTowerFromMV.orientation