alexander_duality_cert_exists
plain-language theorem explainer
The theorem asserts existence of a certificate encoding that the circle has reduced cohomology rank one in degree one, rank zero elsewhere, and linking dimension exactly three. Researchers tracing the T0-T8 forcing chain would cite it to ground the D=3 step without external axioms. The proof is a direct term construction that populates the three fields of the certificate from the supporting lemmas on circle cohomology and linking.
Claim. There exists a certificate such that the reduced cohomology rank of the circle in degree 1 equals 1, the rank vanishes for every integer degree k ≠ 1, and the linking dimension of the circle equals 3.
background
The module develops a structural replacement for the three Alexander duality axioms used in T8 (D=3 forcing). AlexanderDualityCert is the record whose fields are: reduced cohomology rank of the circle equals 1 in degree 1; the rank is zero for all other integer degrees; and linking dimension of the circle is 3. These statements formalize the classical fact that S^1 links non-trivially in S^D precisely when D=3, via the isomorphism of reduced cohomology groups H̃_{D-2}(S^D ∖ S^1) ≅ H̃^1(S^1) ≅ ℤ when D ≥ 3. The three upstream lemmas supply the concrete values: circle_nontrivial_in_degree_one gives the rank-1 statement, circle_trivial_elsewhere gives the vanishing for k ≠ 1, and circle_links_in_three gives the dimension-3 result by direct normalization.
proof idea
The proof is a one-line term-mode wrapper. It constructs an element of Nonempty AlexanderDualityCert by supplying the three fields of the structure directly: circle_degree is taken from circle_nontrivial_in_degree_one, circle_only_degree from circle_trivial_elsewhere, and d3_from_linking from circle_links_in_three.
why it matters
This declaration closes the local existence claim for the Alexander duality certificate inside the module that prepares the replacement of axioms for T8. It thereby supports the Recognition Science step that forces exactly three spatial dimensions from the linking properties of circles. The module document notes that Mathlib's AlgebraicTopology library does not yet contain the required reduced cohomology of spheres, so the certificate records the mathematical content that will be discharged once that support arrives.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.