def
definition
RobustnessHypothesis
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.Papers.DraftV1 on GitHub at line 272.
browse module
All declarations in this module, on Recognition.
explainer page
used by
formal source
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. -/
298theorem dimensional_rigidity_main (D : ℕ)
299 (_hT : LinkingInvariantHypothesis D)
300 (hK : ConstraintK D)
301 (_hS : ConstraintS D) :
302 D = 3 :=