def hypothesis interface def or abbrev

`LinkingInvariantHypothesis`

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

formal statement (Lean)

 250def LinkingInvariantHypothesis (D : ℕ) : Prop :=

proof body

Definition body.

 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). -/

used by (5)

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

dimensional_rigidity_full_forward in IndisputableMonolith.Papers.DraftV1 decl_use
dimensional_rigidity_main in IndisputableMonolith.Papers.DraftV1 decl_use
linking_selection_principle in IndisputableMonolith.Papers.DraftV1 decl_use
LinkingSelectionPrincipleHypothesis in IndisputableMonolith.Papers.DraftV1 decl_use
no_higher_dimensional_alternative in IndisputableMonolith.Papers.DraftV1 decl_use

depends on (8)

Lean names referenced from this declaration's body.

of in IndisputableMonolith.Astrophysics.NucleosynthesisTiers decl_use
SphereAdmitsCircleLinking in IndisputableMonolith.Foundation.AlexanderDuality decl_use
of in IndisputableMonolith.Foundation.DAlembert.LedgerFactorization decl_use
of in IndisputableMonolith.Foundation.PhiForcingDerived decl_use
of in IndisputableMonolith.Foundation.SpectralEmergence decl_use
for in IndisputableMonolith.Foundation.UniversalForcingSelfReference decl_use
of in IndisputableMonolith.Information.PhysicsComplexityStructure decl_use
Status in IndisputableMonolith.Measurement.RSNative.Core decl_use