Dynamic Curry-Howard T: Basic Parameters of Information-Loss Accounting and Compositional Closure in Constraint Systems

This paper examines, within the Cartesian closed category framework of constraint systems, two composition rules for information-loss accounting. The additivity law with auxiliary coefficients as basic parameters requires the compositecoefficient to equal the sum of the single-step coefficients, and uses a unified topological complexity as the multiplier of the budget; the additivity law with the budgetas the basic parameter directly sets the composite budget equal to the sum of thesingle-step budgets, with auxiliary coefficients used only for single-step records. Thecore thesis of this paper is: the difficulty of the former lies not in “adding coefficients”itself, but in that composite complexity can strictly contract under morphism composition, so that the composite budget obtained by adding coefficients no longerdominates the composite minimum budget; the latter gives a feasible compositeclosure, but it is a conservative upper bound rather than an optimal budget. Tomake this distinction hold, this paper introduces the minimum budget as the feasible cone lower bound under a fixed measure, and distinguishes three propositions:the triangle inequality for the minimum budget, conservative closure for arbitraryfeasible budgets, and worst-case uniform closure. On this basis, this paper gives afunction-type realizability construction: embed ten nodes into an extended system,then compress the extended system back to ten nodes, so that the single-step complexity is equal while the composite complexity strictly decreases, and a matchinginformation measure is given that makes the single-step budget feasible but thecomposite budget infeasible. This construction excludes “single-point flattening—unfolding” type non-functional steps. Thus two argumentative routes are obtained:the combinatorial route uses a parameterized family of counterexamples to show rulefailure; the functorial route gives necessary and sufficient conditions for compositeclosure and tests the two rules. The two routes do not share the same sufficiencyproof, but both rely on realizability and minimum-budget feasibility premises. Thispaper marks the conclusion as a candidate theorem pending independent review,and clarifies its scope of applicability: non-normalized information measures, functional node mappings, finite discrete systems without hyperedges. Chapter 9 furtherelevates the domain declaration of decorated arrows to a formal component of theframework, and in the class of normalized measures gives a capped restatementand an existence negation for Rule A, closing the original open boundary G9 andregistering the degenerate-pair boundary G10.