生长式数学IV:鸽笼原理归结证明长度的精确闭式——构造式方法、对称群商与弱化计量

We give an exact closed-form formula for the constructive resolution proof length of the pigeonhole principle (PHP): D(n) = (n+1)!(11/6 + Σ 1/j!) ≈ (e − 1/6)(n+1)!, and prove the exact identity ⌊(e − 1/6)(n+1)!⌋ = D(n) + n + 2. A quotient folding of the proof DAG under the symmetric-group action compresses storage from factorial to exponential level, F(n) = 11·2^(n−1) − 3n − 5 (derived from the folding recurrence, verified pointwise for n ≤ 9; 671.4× at n = 8). Weakening usage is measured exactly; an equivalence reconstruction eliminating explicit weakening converges to the purification constant (2e − 7/3)/(e − 1/6) ≈ 1.2162 with closed form D′(n) = ⌊(2e − 7/3)(n+1)!⌋ − (2n + 3), so the bound holds in pure resolution up to a constant factor. A self-built checker verifies n = 2..8 (expanded) and n = 9 (folded). Paper IV of the Growth-Style Mathematics series.