Analyze failed COBOL checks falling through to dynamic routes

Prove that a failed level-88 check falls through to routing with its unchanged condition variable. An explicit approved contract must require the condition at the routing operation. The local proof covers a selected failure branch followed by a dynamic CALL without arguments or a single CICS routing command. CICS supports the target option and optional RESP, RESP2 and NOHANDLE. Other options remain unproven. Select a failure THEN branch or an explicit failure ELSE branch. Effects in the other branch do not establish the selected path. An absent ELSE is not analyzed as an implicit failure path. Failure branches may use CONTINUE, simple EXIT, plain literal DISPLAY, supported disjoint assignments or a proven returning local message paragraph. A message paragraph may contain read-only IF or EVALUATE branches with supported assignments, bounded message construction, plain literal DISPLAY, CONTINUE or simple EXIT at every leaf. Allow nested noniterative single-paragraph PERFORM with explicit IN or OF section qualifiers. Limit the expanded call tree to 64 statements, 16 active paragraphs and 16 levels of conditions. Recursion, CALL, control transfers and unknown effects prevent the proof. A PERFORM between the completed check and the protected operation remains a barrier. The recipe does not infer entry reachability, approved targets, compiler name mapping or failure exits. Plain DISPLAY of quoted ASCII text preserves local fields and does not inspect a status value or terminate processing. Accept at most 16 literals of at most 256 characters each. Device options, screen positioning, exception clauses, field reads and functions remain barriers. Failure messages may SET condition names TO TRUE when every parent field is disjoint from the checked field. Validate all targets and complete value clauses before accepting the statement. Retain the existing 16-target and 64-value limits. Changes to the checked field remain barriers even when assigning a failing value. Intervening SET statements after a routing check remain barriers. Also permit plain INITIALIZE of disjoint error fields inside the failure branch and bounded returning message paragraphs. Validate at most 16 targets and 64 elementary writes using the declared storage. Every initialized field must be disjoint from the checked result. Initialization never establishes a successful check. FILLER, OCCURS, replacement phrases and unsupported storage prevent this proof. Intervening initialization after a routing check remains a barrier. Permit bounded STRING DELIMITED BY SIZE into ordinary PIC X storage disjoint from the checked value. Validate every operand and require the complete write to fit the receiver. Limit operands to 16 and fields to 256 characters. Overlap, pointers, overflow handlers and unsupported forms remain barriers. Allow these messages in the failure branch and bounded returning message paragraphs. Constructing a message does not reject the failed operation. Intervening STRING after a routing check remains a barrier. INITIALIZE VALUE and FILLER phrases require a separate effect proof and discard default-assignment facts. An explicit TO DEFAULT without a VALUE, FILLER or replacement phrase retains the default behavior.