AlexanderDualityCert
plain-language theorem explainer
The AlexanderDualityCert structure packages the three topological facts required to derive three spatial dimensions from circle linking: reduced cohomology of the circle has rank one exactly in degree one, and the linking dimension for a one-dimensional object equals three. Researchers deriving the dimension of space from algebraic topology in the Recognition Science forcing chain would cite this certificate. It is assembled directly by reading the ranks from the circle cohomology data definition and applying the linking dimension formula at p=
Claim. A structure consisting of the assertions that the reduced cohomology rank of the circle in degree $1$ equals $1$, that this rank vanishes for all degrees $k ≠ 1$, and that the linking dimension of a one-dimensional object equals $3$.
background
This module addresses the question of replacing three Alexander duality axioms used in the forcing chain step T8, which derives three spatial dimensions. The circle_cohomology definition supplies a SphereCohomologyData object for the one-dimensional sphere whose reduced cohomology rank is one in degree one and zero otherwise. The linking_dimension function is defined by linking_dimension p := 2 * p + 1, which for p=1 gives three. The local setting is the mathematical content that the linking argument forces D=3 exactly when the linking object is one-dimensional.
proof idea
The definition packages three fields directly: the first two are read off from the circle_cohomology data by case analysis on the degree, while the third applies the linking_dimension formula at argument one.
why it matters
This certificate is the input to the theorem alexander_duality_cert_exists, which shows it is inhabited. It fills the structural framework for the Alexander duality argument in the Recognition Science forcing chain, specifically supporting the derivation of D=3 in T8. The module notes that full Mathlib support for reduced cohomology of spheres is pending, so this remains a placeholder structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.