SHA: open product-layout linear claims without an inner sumcheck

[wu-s-john]

For eligible repeated SHA layouts, open the rank-one linear functional directly through BitZ instead of reducing it with an assignment-domain inner sumcheck. This issue owns the optional product layout, claim construction and its verifier; it must retain the generic fallback.

Sources and current behavior

The current inner handoff creates a point claim after quadratic sumcheck. The PoC direct product branch emits an empty inner proof and constructs a product claim. Current relation/field/commitment contracts are normative; the reference branch demonstrates the optimization, not permission to import different transcript or security parameters.

Required geometry

Represent the batched functional as D(i,j) = row_weight(i) × column_weight(j) over the chosen physical h grid. Public geometry must establish this factorization, including the constant coordinate, public-IO terms, live extents, chain links and padding. Keep the committed f order explicit and use a bound virtual map to relate it to h. Eligibility must follow from public shape, not witness contents.

Normative prover-verifier flow

1. Bind the route/version, commitment, public SHA statement, logical-to-physical map, both shapes, field/profile and padding before challenges; preserve the approved OOD prefix.
2. Execute the linear batching from SHA: batch linear constraints without the nonlinear outer sumcheck #77. The verifier independently derives both functional factors and the target from public data and transcript challenges.
3. Construct the existing admissible prime-field linear claim on h. No assignment-domain inner messages or prover-supplied factor vectors are trusted.
4. Absorb the opening statement under the new route, then prove the virtual BitZ opening back to f's commitment.

The modulus, integer lifts/chunk bounds and F2 map semantics remain those of the target opener. A factorization over Fq is not an equality over F128.

Ordered verifier

Validate eligibility and the bound layout; replay linear challenges; reconstruct factors/target; require the direct route to contain no inner-round messages; verify field/no-wrap bounds and the virtual opening; accept only after the underlying PCS verifies. For ineligible shapes invoke the existing inner route, with a distinct proof variant. Reject mismatched route tags, layouts, extra rounds and malformed lengths.

Done when

• Direct and fallback routes prove the same tiny relations, supported SHA batches and chained cases.
• Tampering with factorization metadata, public IO, constant location, padding, commitment or final opening is rejected.
• Zero factor/scale cases require no inversion and do not bypass PCS authentication.
• Transcript fixtures cover each route and prove route separation.
• Benchmarks isolate inner rounds/table memory/proof bytes removed and any extra layout or virtual-opening cost.

Dependencies and non-goals

Depends on #77 and #42. Coordinate the PCS boundary with #54 and PR #69 and OOD ordering with PR #76; do not replace the generic arbitrary-row/column claim reduction those own. This is not a universal R1CS inner-sumcheck bypass.

Potential impact

Eliminates the full assignment-domain inner sumcheck on eligible product layouts. GKR, virtual-map binding and the final PCS still run.