Capacity-Defect Profiles for Finite Permutation Models of Higman's Group: Exact Radius-Three Rigidity at Degree Twenty

This unified record contains the complete manuscript, mathematical source, explicit witnesses, exhaustive-search transcripts, independent propositional proof certificates, verification tools, correction history, structured SAT benchmarks, and cryptographic manifests establishing the exact finite capacity-defect value K*(20,3,0) = 14 and D20,3(0) = 7/10 for strict radius-three permutation models of the classical Higman group H₄ = ⟨a₀,a₁,a₂,a₃ | aᵢ⁻¹aᵢ₊₁aᵢ = aᵢ₊₁², i mod 4⟩. For a degree-n assignment of the four generators to permutations, test radius L, and fixed-point budget t, K*(n,L,t) is the minimum possible maximum moved-point support of the four defining relators, subject to every certified nonidentity test word of length at most L fixing at most t points. Under strict radius-three freeness, the associated undirected letter graph is simple, 8-regular, and triangle-free. Mantel’s theorem gives the degree threshold n ≥ 16, and the Andrásfai–Erdős–Sós theorem forces bipartiteness for 16 ≤ n < 20. At degree twenty, every non-bipartite admissible letter graph is proved to be the unique balanced pentagonal blow-up C₅[K̄₄]. Three explicit oriented 2-factorizations satisfy all 456 nonempty freely reduced radius-three constraints and make each of the four Higman relators move exactly 14 points. For the reverse inequality, 1084 canonical target-seven start sets reduce through a proved max-class symmetry to 432 representatives, while the 81 possible nondegenerate generator-flow tuples reduce to 14 symmetry orbits. The complete exact-cover computation certifies all 14 × 432 = 6048 cells as UNSAT, with zero timeout and zero missing transcript. A structurally independent direct-CNF encoding supplies one checked DRUP/RUP UNSAT proof in every flow-sector orbit. The publication package includes: - the human-readable manuscript and LaTeX source; - three independently verified K = 14 witnesses; - the complete 6048-cell exact-cover lower-bound certificate; - fourteen independent direct-CNF DRUP/RUP proof checks; - a mandatory SAT counterexample control; - machine-readable summaries and exhaustive transcripts; - reusable verification software and a Python wheel; - SHA-256 manifests; - the complete correction and audit history; - five separate domain-specific research-program specifications; - a standalone structured SAT benchmark bundle. The release also documents the withdrawal of two preliminary v0.8 reductions. The former prefix-injection argument lacked a complete treatment of mixed macro-orientations, and a proposed five-class bottleneck inequality was refuted by an explicit SAT witness. Neither statement is used in the final theorem. Version 1.0 re-established the lower bound on the larger complete 6048-cell domain, and Version 1.1 promotes the correction process to an explicit verification case study. This result is a finite-degree, finite-radius theorem. It neither proves nor disproves the soficity of Higman’s group. Licensing: source code and executable scripts are released under the MIT License. The manuscript, proofs, data, witnesses, certificates, transcripts, SAT instances, proof logs, metadata, and documentation are released under the Creative Commons Attribution 4.0 International License.