We introduce f mod (K) = #φ: φ ∈ Thm (T), μρT (φ) ≤ K, counting logical equivalence T classes of theorems with short proofs, and the proof-length abscissa σ0 (T) = lim supK→∞ log f mod (K) / log K. T We establish three unconditional results: (I) f mod (K) ≥ f mod (K) + ⌊K/c0⌋ − n0, hence PA Q ρ (PA, Q) ≥ 1/c > 0; (II) σnew (PA, Q) ≥ 1 > −∞ = σnew (Q, PA) (exact value conjectured 2, el00 0 open) ; (III) ρel (ZFC, PA) ≥ 1/c0 > 0 (via G ̈odel’s Second Incompleteness Theorem and Fefer- man 1960). Numerically verified: f mod (K) ≈ K2/ (2L2) (L = 15), so σ0 (Q) → 2; the absolute Qinvariant does not separate Q from PA. The strict chain ρel (IΣk+1, IΣk) ≥ 1/ck > 0 holds unconditionally.
Eugene Sporyshev (Sun,) studied this question.