LinkingSelectionPrincipleHypothesis
plain-language theorem explainer
LinkingSelectionPrincipleHypothesis encodes the claim that an integer-valued circle linking invariant on spheres forces ambient dimension D to equal 3. A researcher closing the topological derivation of spatial dimensionality from the Recognition framework would cite this interface when assembling the forward direction of the main theorem. The definition is a direct one-line wrapper packaging the implication from the upstream linking hypothesis.
Claim. If the sphere admits a circle linking invariant in dimension $D$, then $D = 3$.
background
The Papers.DraftV1 module mirrors theorem statements from Draft_v1.tex and supplies hypothesis interfaces for results that depend on external mathematics such as Alexander duality for embeddings. LinkingInvariantHypothesis D is defined as SphereAdmitsCircleLinking D, which encodes the cohomology-based linking predicate. The module doc-comment states that such interfaces keep the certified surface honest by avoiding global axioms for heavy topology.
proof idea
The declaration is a definition that directly sets the hypothesis equal to the implication LinkingInvariantHypothesis D → D = 3. It acts as a one-line wrapper that packages the logical step from the linking invariant to the dimension conclusion, with the bridge supplied by alexander_duality_circle_linking as noted in the doc-comment.
why it matters
This declaration implements paper proposition (T), the linking selection principle. It is applied directly by the downstream theorem linking_selection_principle to conclude D = 3 from the linking hypothesis. In the Recognition Science framework it advances T8 by forcing three spatial dimensions from the linking structure, consistent with the eight-tick octave. It touches the open question of discharging the hypothesis once the duality result is internalized.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.