theorem proved term proof

`D3_has_linking`

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

formal statement (Lean)

 287theorem D3_has_linking : SupportsNontrivialLinking 3 :=

proof body

Term-mode proof.

 288  (alexander_duality_circle_linking 3).mpr rfl
 289
 290/-- **T8 PRIMARY THEOREM**: Linking requires D = 3.
 291    Proof: Alexander duality — no reference to 8-tick or gap-45. -/

used by (2)

From the project-wide theorem graph. These declarations reference this one in their body.

D3_compatible in IndisputableMonolith.Foundation.DimensionForcing decl_use
high_D_no_linking in IndisputableMonolith.Foundation.DimensionForcing decl_use

depends on (9)

Lean names referenced from this declaration's body.

tick in IndisputableMonolith.Constants decl_use
or in IndisputableMonolith.Constants.EulerMascheroni decl_use
tick in IndisputableMonolith.Constants.RSNativeUnits decl_use
alexander_duality_circle_linking in IndisputableMonolith.Foundation.AlexanderDuality decl_use
SupportsNontrivialLinking in IndisputableMonolith.Foundation.DimensionForcing decl_use
gap in IndisputableMonolith.Gap45.Derivation decl_use
gap in IndisputableMonolith.Masses.AnchorPolicy decl_use
gap in IndisputableMonolith.Masses.RSBridge.Anchor decl_use
gap in IndisputableMonolith.RSBridge.Anchor decl_use