The Indexed Specification Algebra: One Object, Seven Theorems, and a Factorization Engine for Regimes as Dependency Systems

This paper develops an indexed algebra for the internal structure of sufficient declared-regime specifications. Its starting point is a bounded-verification problem: once a regime has declared the identity conditions, admissible transformations, evidence boundaries, authority, outcome types, and replay obligations governing a verdict, what dependency structure exists among those declarations, and which parts of that structure are recoverable, minimal, interactive, or realizable? A specification at a declared index is represented by a finite quotient-level dependency system, D_I, consisting of admissible role assignments paired with replay semantics at a declared grain. Quotient-level recoverability induces a semantic closure operator; functional determination characterizes replay sufficiency; minimal semantic keys characterize record sufficiency modulo mandatory provenance and version fields; and refinement is represented by dependency-preserving factorization. A consolidation theorem proves that factorization-based recoverability and quotient-level semantic closure are the same operator. Minimal sufficiency and interaction are shown to be distinct. Minimal keys describe which information jointly determines a result, whereas interaction describes failure of the semantic kernel to decompose across declared coordinate blocks. The paper establishes their nonidentity and gives separate fiberwise and section-level results, including a connectivity obstruction limiting where masking can occur. The realizability analysis distinguishes arbitrary finite dependency systems, systems representable in the declared presentation language, floor-gated systems, and systems induced by corpus-sufficient regimes. The presented class receives a sound and complete representation theorem. A fixed pre-verdict signature yields a strict gate separation and a universal gate quotient, characterized as the least-informative quotient sufficient for gate status. Every declared factorization obligation f = f̄ ∘ q is equivalent to a kernel inclusion and admits a labeled two-point obstruction certificate. In finite systems, these obligations compile into definite Horn implications. Countermodels further show that mixed raw/quotient determination need not form a closure operator, that the quotient-level closure is not generally matroidal, and that minimal generating sets may have unequal cardinalities. The paper does not claim to characterize corpus sufficiency. Its remaining realizability question is whether regime-induced systems coincide with systems satisfying the complete relational translation of the specification floor: Reg_I ?= FloorDep_I