def
definition
LinkingInvariantHypothesis
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 250.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
247
248/-- Hypothesis interface for the paper's ``integer-valued loop-linking invariant exists'' premise.
249Now delegates to the cohomology-based linking predicate. -/
250def LinkingInvariantHypothesis (D : ℕ) : Prop :=
251 SphereAdmitsCircleLinking D
252
253/-! ## Remaining paper propositions (placeholders) -/
254
255/-- Placeholder for the paper proposition ``RG Conditions for Duality''.
256
257Status: not yet formalized (topology of quotients + local contractibility). -/
258def RGConditionsForDualityHypothesis : Prop := True
259
260theorem rg_conditions_for_duality (_h : RGConditionsForDualityHypothesis) : True := trivial
261
262/-- Placeholder for the paper proposition ``RG Derivation of Central Potentials''.
263
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