Park's Conjecture via Escape Principles: A Roadmap with Non-Vacuity Diagnostics

Park's conjecture (1976) predicts that a finitely generated variety of finite type with a finite residual bound must be finitely based. This note presents a compact "roadmap" formalizing a standard contrapositive strategy through a two-parameter bounded fragment Th_{m,D}(V), minimal (critical) countermodels for bounded fragments, and an Escape Property EP(g) that transfers boundary obstructions in critical countermodels to the existence of large finite subdirectly irreducible algebras inside the target variety. The emphasis is logical hygiene: we isolate and repair two common sources of vacuity (absence of finite countermodels and hidden finiteness assumptions), so that implications of the form "FRB + EP(g) => finitely based" become formally sound. We also record two structural templates—commutator-theoretic and tame-congruence-theoretic—that encapsulate the substantive work required to verify EP(g).