A Decision Procedure for Structural Admissibility in the Quantized Dimensional Ledger

This paper develops the computational phase of the Quantized Dimensional Ledger (QDL) programme by reformulating structural admissibility as a finite decision problem. In QDL, physical constructions are represented by integer ledger vectors and judged by closure rather than by dimensional homogeneity alone. Earlier work introduced the ledger lattice, the closure subgroup generated by the Quantized Dimensional Cell, and applications to operator filtering, renormalization, metrology, physical constants, and coupled-sector admissibility. The present paper asks whether admissibility itself can be made executable. A symbolic construction is treated as a finite word over a typed representational alphabet equipped with a ledger map into a five-dimensional integer lattice and a declared quotient by admissible representation transformations. Within this setting, four main formal results are established. First, a decidability theorem shows that admissibility of any finite symbolic construction is computable in finite time. Secondly, an equivalence theorem shows that the closure-subgroup formulation of admissibility is canonically equivalent to a kernel formulation via an obstruction homomorphism into a quotient obstruction group. Thirdly, a strict-refinement theorem shows that, except in the collapse case where the quotient lattice has rank one, QDL admissibility is strictly stronger than ordinary dimensional homogeneity: there exist homogeneous constructions that are nevertheless closure-inadmissible. Fourthly, a complexity proposition shows that for a fixed rule set, admissibility evaluation has linear aggregation cost in the length of a normalized input expression, with fixed-cost quotient and closure evaluation at fixed lattice rank. A finite benchmark family and a physics-motivated effective-field-theory operator benchmark are then given, together with exact candidate-space filtering consequences. The paper does not claim automated discovery of correct physical law or replacement of dynamics by computation. Its claim is narrower: structural admissibility in QDL can be formalized as an exact decision procedure and used as an upstream structural filter on finite candidate model spaces. This paper therefore marks the executable stage of the broader QDL Unified Admissibility Theory programme.