rg_derivation_of_central_potentials

formal source

 264Status: not yet formalized (Laplacian / Green's functions). -/
 265def CentralPotentialDerivationHypothesis : Prop := True
 266
 267theorem rg_derivation_of_central_potentials (_h : CentralPotentialDerivationHypothesis) : True := trivial
 268
 269/-- Placeholder for the paper proposition ``Robustness of D=3 Signature''.
 270
 271Status: not yet formalized (perturbation theory / IFT / continuity). -/
 272def RobustnessHypothesis : Prop := True
 273
 274theorem robustness_of_D3_signature (_h : RobustnessHypothesis) : True := trivial
 275
 276/-- The (T) setup assumptions required for Alexander duality in the paper
 277are satisfied for this dimension. Now delegates to the cohomology-based
 278`SphereAdmitsCircleLinking` rather than being vacuous. -/
 279def AlexanderDualityApplies (D : ℕ) : Prop :=
 280  AlexanderDualityForCircleHypothesis D
 281
 282/-- Paper proposition (T): Linking selection principle.
 283
 284Previously an explicit hypothesis interface; now the bridge from
 285linking to D = 3 is provided by `alexander_duality_circle_linking`. -/
 286def LinkingSelectionPrincipleHypothesis (D : ℕ) : Prop :=
 287  LinkingInvariantHypothesis D → D = 3
 288
 289theorem linking_selection_principle (D : ℕ)
 290    (h : LinkingSelectionPrincipleHypothesis D) (hLink : LinkingInvariantHypothesis D) :
 291    D = 3 :=
 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. -/