SphereCohomologyData
plain-language theorem explainer
SphereCohomologyData packages the reduced cohomology ranks of an n-sphere, recording rank one solely in degree n. Researchers deriving spatial dimension from linking topology would cite it when assembling Alexander duality constraints. The declaration is a direct structure definition that bundles dimension, rank function, and the characterizing equality.
Claim. Let $d$ be a natural number, let $r$ map integers to natural numbers, and let $e$ be a proof that $r(k)$ equals 1 when $k=d$ and 0 otherwise, for every integer $k$. The triple $(d,r,e)$ records the reduced cohomology data of the $d$-sphere.
background
The module replaces three ad-hoc axioms for Alexander duality with statements drawn from algebraic topology libraries, in service of the T8 step that forces exactly three spatial dimensions. Reduced cohomology of the n-sphere is rank one in degree n and zero elsewhere; Alexander duality then identifies the cohomology of the complement of an embedded circle in an ambient sphere with the cohomology of the circle itself. Nontrivial linking therefore occurs only when the ambient dimension is three. The structure records precisely this cohomology signature for use in the linking argument.
proof idea
The declaration is a structure definition. It directly assembles the dimension field, the rank function, and the universal equality constraint into a single record. No lemmas are applied.
why it matters
The structure is instantiated for the circle inside the definition of circle cohomology, which supplies the input to the linking argument that forces D=3. It advances the program of discharging the three Alexander duality axioms in favor of Mathlib statements and sits inside the unified forcing chain at the T8 step. The module leaves open the question of when full reduced-cohomology support arrives in the library.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.