Reflexive Compression Boundaries in Graded Categories

The complexity of self-referential computation decomposes into three independent gaps: naming, construction, and depth transfer. We prove, in a 93-file Lean 4 formalization with zero sorry and zero Classical.choice, that naming and fixed-point construction close from the categorical structure of a reflexive object D ≅ [D,D] alone, while depth transfer reduces to a quantitative growth-gap hypothesis on the graded slices of End(D) and D. The anti-compression theorem shows the three conditions are jointly unsatisfiable. A non-uniformity theorem establishes that computational growth gaps require graded non-uniformity in the reflexive isomorphism. The growth gap is proved for any computational model with finite-table representability, instantiated for Lean's Nat.Partrec.Code. Bounded linear logic's bounded exponential forces the gap via the cost of contraction. In the polynomial enrichment, Markov's principle at polynomial bounds is equivalent to P = NP — a bridge theorem identifying a resource-bounded witness-extraction principle with the classical search/verification collapse. Companion formalization archived at DOI:10.5281/zenodo.18915083.