Live ensemble validates an incomplete Arith provider circuit — model-coverage gap class

[codygunton]

Finding (verified 2026-07-19, refactor turn R14; full audit in REFACTOR_14_REPORT.md on branch refactor-14, PR #278)

The accepted-trace ensemble validates arithmetic provider rows through the shared ArithMul.componentWithArithTable component, whose circuit (mainWithArithTable) mirrors only a subset of the physical Arith AIR's generated constraints — the carry chains, table/range lookups, and (as of the refactor stack) the selector booleans. The Div-block generated constraints (zero-divisor/overflow boundary constraint_9–24, inverse-sum detector constraint_25, scope/disjointness constraint_26–30, W-mode lanes constraint_47–48) are not validated by the live ensemble:

• ArithMulRow does not model the Arith AIR's inv_sum_all_bs witness column (stage-1 col 38), and the row-view converter vOfDivuRow fabricates it as 0 — under which the generated inverse-sum equation is false on ordinary nonzero DIV/REM rows.
• The complete constraint mirrors exist in Lean (AirsClean/ArithCompleteConstraints.lean, every assertZero cited to its constraint_N_every_row extraction fact + arith.pil line) but as dormant circuits the ensemble never runs.
• Consequently the Div-family wrappers carry 16 caller-supplied row-constraint premises that cannot currently be derived. An attempted derivation (refactor turn T13/R14) was correctly refused as unconstructible — discharging them against the incomplete live supply would have been obligation laundering.

Why this matters beyond Arith

This is a class, not a one-off: "the Clean circuit the ensemble actually validates" can silently cover fewer generated constraints than the Lean mirrors or the legacy Valid_<AIR> models suggest. Wherever that happens, facts get carried as caller premises instead of derived, and the modeled acceptance predicate is weaker than the real AIR. The per-family Q2 audits compare constraint lists; they do not check which circuit the ensemble validates — that dimension needs its own audit (in progress: a live-provider coverage matrix across Main/Mem/MemAlign/RegisterBoundary and the static-table families).

Remediation

In flight as refactor turn R15 (branch refactor-15): materialize inv_sum_all_bs and the full audited generated local-constraint set in the shared provider row/circuit, swap the live ensemble onto the completed component with real witness values (constructibility prechecked per concrete row), then derive the 16 premises. Constraint list frozen to the cited generated mirrors; Compliance/Defects.lean (DIV/REM defect boundary) byte-unchanged throughout.

Not a ZisK bug

The physical AIR has all of these constraints and real prover witnesses satisfy them (the real inv_sum_all_bs column is always populated). Nothing currently proven is wrong — the gap is model coverage: premises demanded where derivation should be possible.

[codygunton]

Full live-provider coverage matrix (local audit, 2026-07-19, two read-only sweeps over the refactor stack tip)

Question audited: for each family, does the circuit the ensemble ACTUALLY validates cover the physical AIR's generated constraints, or are facts silently premise-carried (the gap class this issue names)?

Family	Arith-class gap?	Detail
Arith (shared provider)	YES — this issue	remediation in flight (refactor R15)
Main	PARTIAL — one item	the source-C copy constraint (main.pil:386) exists only as a dormant mirror and is carried as caller premises in the JALR-unaligned bridge (EquivCore/Bridge/ControlFlow.lean:35). Cross-row fact → belongs on Main's Component.transition beside the PC handshake; bounded fix, witness re-discharge sites enumerated. Everything else per-row is validated live
Mem	PARTIAL, structurally closed	missing per-row groups are homed on Component.transition and mechanically derived via transitions_hold (TableProjections.lean:1123-1141) — the mechanism Arith lacked. Residue mem_replay_segment_ranges is pre-S3 state on the stack; already derived+deleted on main (#265), disappears at rebase
MemAlign (general)	YES — known & planned	MemAlignLoadProviderRomValueFacts premise-carries MemAlignRom-derived width/value facts ("MemAlignRom is not currently extracted as a first-class Lean table"); 9 cross-row constraints mirror-dormant; 8 forward-rotated (+1 rowOffset) constraints absent even from extraction. This is exactly closeout stream S4 / #242's scope — no new work item, but the refactor must NOT attempt MemAlign deletion before #242 lands
MemAlignByte / MemAlignReadByte	NO	Clean main emits every F-constraint plus the range lookups — a strict superset of the legacy core
RegisterBoundary	NO (n/a)	Spec := True provider by design; correctness rides on MemBus telescoping balance; nothing premise-substituted
BinaryTable / BinaryExtensionTable / RangeTables / ZiskInstructionRom	NO	membership-only static tables, membership closed live by in-circuit lookups, zero axioms
ArithTable (standalone module)	PARTIAL (wart, not load-bearing)	ArithTable.lean:66-75 documents projection facts that OVER-claim beyond ROM data (np = na XOR nb, W-mode sext = 0 — refuted by concrete MULW/DIVUW/DIVW rows); module is explicitly not on the global theorem's dependency graph. Hazard only if someone consumes these later; flagging for disposition

Net: after R15 (Arith) + the small Main source-C transition extension + the already-planned #242, the live ensemble validates the full modeled constraint surface everywhere except by-design provider scopes. No additional hidden skeletons found.