circle_trivial_elsewhere
plain-language theorem explainer
The reduced cohomology rank of the circle vanishes for every integer degree except one. Researchers deriving spatial dimension from linking conditions in Recognition Science cite this when closing the T8 step that forces D=3. The proof is a direct simplification from the explicit definition of circle_cohomology that encodes the rank function.
Claim. For the circle $S^1$, the reduced cohomology rank satisfies $r(k)=0$ whenever $k$ is an integer with $k≠1$.
background
The module replaces three Alexander duality axioms used in the T8 forcing step with explicit data. SphereCohomologyData packages a dimension, a rank function on reduced cohomology, and an equality lemma. circle_cohomology instantiates this data for dimension 1 with rank 1 exactly at degree 1 and rank 0 elsewhere. Upstream Dimension structures from Constants and DimensionForcing track the spatial integer that will be forced to equal 3 by the linking argument.
proof idea
One-line wrapper that applies simp on the circle_cohomology definition together with the hypothesis k≠1, which immediately yields the zero rank.
why it matters
Supplies the circle_only_degree component of the AlexanderDualityCert constructed in alexander_duality_cert_exists. This cert closes the structural replacement for the three axioms that had been used to force D=3 via circle linking in S^D. The result sits inside the eight-tick octave and phi-ladder machinery that already fixes the spatial dimension at 3.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.