No prose has been written for this declaration yet. The Lean source and graph data below render
without it.
generate prose now
formal statement (Lean)
278theorem gap_topologically_protected :
279 ∀ (seq : ℕ → ℤ),
280 (∀ k, seq k ≠ 0) →
281 ∀ k, massGap ≤ Jcost (PhiLadder (seq k)) :=
proof body
Term-mode proof.
282 fun seq hseq k => spectral_gap (seq k) (hseq k)
283
284/-- **Gap rigidity**: the gap cannot close along any sequence of lattice excitations. -/
depends on (13)
Lean names referenced from this declaration's body.
-
of
in IndisputableMonolith.Astrophysics.NucleosynthesisTiers
decl_use
-
of
in IndisputableMonolith.Foundation.DAlembert.LedgerFactorization
decl_use
-
PhiLadder
in IndisputableMonolith.Foundation.PhiEmergence
decl_use
-
of
in IndisputableMonolith.Foundation.PhiForcingDerived
decl_use
-
of
in IndisputableMonolith.Foundation.SpectralEmergence
decl_use
-
gap
in IndisputableMonolith.Gap45.Derivation
decl_use
-
of
in IndisputableMonolith.Information.PhysicsComplexityStructure
decl_use
-
gap
in IndisputableMonolith.Masses.AnchorPolicy
decl_use
-
gap
in IndisputableMonolith.Masses.RSBridge.Anchor
decl_use
-
gap
in IndisputableMonolith.RSBridge.Anchor
decl_use
-
massGap
in IndisputableMonolith.Unification.YangMillsMassGap
decl_use
-
PhiLadder
in IndisputableMonolith.Unification.YangMillsMassGap
decl_use
-
spectral_gap
in IndisputableMonolith.Unification.YangMillsMassGap
decl_use