Registry · Proposition III.P10 tau-effective formalized

III.P10 — K5 Off-Diagonal Exclusion

The K5 axiom (diagonal discipline) forbids off-diagonal coupling at the lemniscate crossing point. In spectral terms: H_L cannot have imaginary eigenvalues because the crossing-point boundary conditions enforce real spectral flow between lobes. This is the structural mechanism behind the critical line.

Book III Part 4 Ch. 25

Dependency Graph

Depends on (2)

Lean Formalization

Module: TauLib.BookIII.Doors.CriticalLine

Symbol: k5_exclusion_check