pith. machine review for the scientific record. sign in
theorem proved term proof high

linking_selection_principle

show as:
view Lean formalization →

The linking selection principle asserts that if a sphere in D dimensions admits a circle-linking invariant and the selection hypothesis holds, then D equals 3. Researchers deriving spatial dimensions from the Recognition Science functional equation would cite this as the forward direction of the Draft V1 main theorem. The proof is a direct one-line application of the hypothesis definition via modus ponens.

claimIf a sphere in dimension $D$ admits circle linking (i.e., SphereAdmitsCircleLinking $D$) and the linking selection principle hypothesis holds, then $D = 3$.

background

This module mirrors theorem statements from Draft_v1.tex by re-exporting proved results or supplying explicit hypothesis interfaces for external mathematics such as Alexander duality. LinkingInvariantHypothesis $D$ is defined as SphereAdmitsCircleLinking $D$, the existence of an integer-valued loop-linking invariant. LinkingSelectionPrincipleHypothesis $D$ is the implication from that predicate to $D=3$, now supplied by the bridge alexander_duality_circle_linking rather than left as an axiom.

proof idea

The proof is a one-line term wrapper that applies the selection hypothesis directly to the linking invariant hypothesis.

why it matters in Recognition Science

This supplies the forward direction of the paper proposition that (T), (K), (S) imply D=3. It sits inside the Recognition Science forcing chain at T8, where the eight-tick octave and phi fixed point force three spatial dimensions. The declaration closes one interface in the Draft V1 audit surface without introducing new global axioms.

scope and limits

formal statement (Lean)

 289theorem linking_selection_principle (D : ℕ)
 290    (h : LinkingSelectionPrincipleHypothesis D) (hLink : LinkingInvariantHypothesis D) :
 291    D = 3 :=

proof body

Term-mode proof.

 292  h hLink
 293
 294/-- Paper main theorem (forward direction): if (T), (K), (S) hold then `D=3`.
 295
 296In the current repo, (S) and (K) are fully formalized at the arithmetic/algebraic level;
 297(T) is recorded but not used in the proof here. -/

depends on (15)

Lean names referenced from this declaration's body.