Dynamic Curry-Howard S: A Compatibility Criterion for A Posteriori Universe Lifting—Positive-Weight Cycle Testing, Paradox Correspondence, and Implementation

Mainstream proof assistants maintain consistency via static universe hierarchies, with levels fixed at definition time; a posteriori level generalization of analready built development requires rewriting source code; non-predicative schemesthat abolish levels are inconsistent due to Girard’s paradox. This paper studiesan intermediate path: apply a posteriori universe lifting to an already compileddevelopment as a whole or to a subset, and give a decidable criterion for lifting compatibility. Formally, lifting is modeled as a boundary slack check undera fixed compiled level assignment: safety is equivalent to every outgoing boundaryedge having slack (the constraint slack under the compiled assignment) at leastone. This paper also establishes a cycle-weight invariance proposition: the sum ofboundary-edge changes around any closed cycle is always zero, and cycle weightsare invariant before and after lifting; this distinguishes two semantics—assignmentpreserving semantics (adopted here) and reassignment semantics (under which anylifting is always safe). The positive-weight cycle mechanism serves two adjacenttasks in this paper: compilation-graph validation (the initial dependency graph hasno positive-weight cycle; its S = ∅ degeneration is the definition-time check) andhybrid-system skeleton detection (an instantiable Hurkens skeleton leads to inconsistency). In hybrid systems with non-predicative universes, a positive-weight cycleleads to inconsistency only when the pivot edge points to a universe that permitsnon-predicative quantification and the retraction-section instantiation condition issatisfied; positive-weight cycles that do not satisfy this condition are classified as“untypable” rather than “inconsistent”. Accordingly, the predicate-fragment decisionoutputs two values, while the hybrid-system output is three-valued: safe, unsafe,and untypable. Slack scanning is linear time; cycle detection is decided in polynomial time by strongly connected component pruning and Bellman–Ford detection,with Karp’s minimum cycle mean as a structurally independent cross-check. Thecore detection path uses integer arithmetic normalized by least common multiples;timing and statistics use floating point, only for reporting and not participating indecisions.