Registry · Definition III.D94 tau-effective formalized

III.D94 — YM Mass Gap Persistence

τ-gap τ_gap(k) = min(B_k, C_k) is positive for all k ≥ 3 and grows monotonically. τ-internal analog of Yang-Mills mass gap. Bridge gap: identification with physical mass gap requires bridge functor. Verified at depth 5.

Book III Part 4 Ch. 36

Dependency Graph

Depends on (1)

Depended on by (1)

Lean Formalization

Module: TauLib.BookIII.Doors.BridgeTightening

Symbol: ym_gap_persistence_check