carddemo-cardupdate: COCRDUPC writes spaces into a PIC 9(3) CVV; the entity-backed file cannot hold them (+ 30 uncovered branches) #4875

carddemo-cardupdate (COCRDUPC) is still unproven in tests/equivalence/det_sweep_baseline.json; its entry pointed at #4085, a closed porting-loop PR/issue that does not describe the cause. Re-proved on origin/main 0ad5dba (after #4806 and #4871).

Findings (re-proof, 33 scenarios)

1. The COMMAREA bytes now travel (det: a LINK writes the callee's DTO back over the caller's COMMAREA -- a numeric field holding spaces the callee never wrote comes back as digits (CBSA BNK1UAC -> INQACC) #4806/det: RETURN TRANSID COMMAREA carries its bytes to the next task (Part of #4817) #4871), but two scenarios (pf5-confirms-and-rewrites, pf5-rewrite-fails) still differed on commarea.CARD-UPDATE-CVV-CD: COBOL (3 spaces), det port 0. Cause: the PF5 path never fills CCUP-NEW-CVV-CD (the BMS map has no CVV field), so MOVE CCUP-NEW-CVV-CD TO CARD-CVV-CD-X then MOVE CARD-CVV-CD-N TO CARD-UPDATE-CVV-CD carries spaces into a PIC 9(3). cobc compiles a MOVE between zoned items of one shape as a memcpy (cb_build_move_copy), so the spaces travel; the det runtime always ran libcob's store_common_region (space -> '0'). Fixed by the PR that files this (Cobol.move: same-shape zoned to zoned is a byte copy; measured against cobc in test_det_nondigit_zoned.py, receiver OWN).
2. Remaining difference (this issue): the REWRITE's record CARD-CVV-CD in the CARDDATA file: COBOL , Java 000. The det port's CICS file (DetCics.Store) persists through the generated JPA entity CardRecord (toRecord / fromRecord), whose CVV is a typed numeric: bytes that are not digits cannot be held. Same cause as the old baseline reason, but it is the entity layer (the DTO commarea is fine now), and it hits the java-facade side too.
3. Coverage: after the proof, not proven by coverage either: 33 scenarios cover 44/45 paragraphs, 159/189 branches (30 outcomes uncovered: mostly the never false edit-validity IFs 730..939, 2000-DECIDE-ACTION 949/972/1013, 3200/3250/3300 screen vars, 9100/9200, ABEND-ROUTINE). Each needs a scenario or a reviewed infeasible_outcomes.json entry.

What IBM does: a PIC 9(3) holding X'404040' is a stored non-numeric value; the record is written as the bytes. The program keeps that defect (real CardDemo behaviour), so a proof must carry it.

Design options for 2: (a) entities keep the record bytes beside the typed columns (lossless round trip when a column's bytes are not a valid number); (b) a declared difference for entity-typed numerics (loosens the proof: not preferred); (c) the det port's store keeps raw record bytes and the entity is a view.

Acceptance: carddemo-cardupdate proves with all scenarios equal on the port and the facade, coverage complete or stated, then the baseline entry goes.