H_ThreeDimensionalLinkingUnique
plain-language theorem explainer
Defines the proposition that spatial dimension equals 3 if and only if a strictly positive Hopf linking penalty exists and equals ln φ. Anyone citing the linking-based force of D=3 uses this as the named hypothesis. It is a bare Prop abbreviation, not a proved theorem; the body is the biconditional itself.
Claim. The hypothesis asserts: for every natural number $D$, one has $D = 3$ if and only if there exists a real penalty $> 0$ equal to the Hopf linking penalty $\ln\varphi$.
background
The Verification.Dimension module shows that RSCounting plus 45-gap synchronization forces spatial dimension three, with the iff RSCounting_Gap45_Absolute D ↔ D = 3. A parallel, topology-flavored route appears here: non-trivial linking of 1-spheres should single out D=3.
The Hopf linking penalty is defined in-module as hopf_linking_penalty := Real.log phi, i.e. $\ln\varphi$. Across the monolith, the constant D is fixed at 3 by several independent landmarks (T8 spatial forcing in GapDerivation, T9 linking in AlphaDerivation, the FermionDOFGapBridge cadence). This hypothesis packages the linking uniqueness claim as a single Prop so downstream theorems can take it as an assumption rather than re-stating the biconditional.
proof idea
No proof: the declaration is a definition of a proposition. The right-hand side is the universal biconditional equating D=3 with existence of a positive penalty equal to the Hopf linking penalty. A commented axiom line records the intended future discharge; nothing is proved here.
why it matters
Feeds the theorem dimension_three_from_linking_requirement, which under this hypothesis concludes that any D admitting a positive Hopf linking penalty must equal 3 (one direction of the biconditional). In the Recognition Science chain this is the T8/T9-style linking argument for D=3, complementary to the RSCounting-plus-gap-45 arithmetic path already proved in the same module. The doc-comment flags the open scaffold: prove that the linking number of 1-spheres is an invariant only in three dimensions, so the hypothesis can be discharged rather than assumed.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.