AdditiveNTT: unify the round-index type on `Fin r`, and widen `iteratedQuotientMap` to admit `i = ℓ`

[alexanderlhicks]

Summary

While reviewing ArkLib PR #383 (FRI-Binius) I found that CompPoly's AdditiveNTT cannot currently
be used directly by the Binius formalization, and that the PR works around this by re-deriving 62
of CompPoly's declarations locally with different signatures. That workaround should not be the
end state — CompPoly exists precisely so consumers like Binius can plug in — so this issue records
what the plug-in blockers are.

There are two: one is a genuine expressiveness gap, the other is an ergonomic inconsistency.

How the two copies arose (worth recording)

This is parallel development, not a fork. CompPoly's AdditiveNTT gained Domain, Intermediate,
Algorithm and Correctness between d7b9f987 (v4.28.0) and 18c1613e (v4.30.0) — precisely the
four modules ArkLib re-derives. Over the same window, ArkLib PR #455 was independently adding an
AdditiveNTT/Domain.lean on the ArkLib side, against the older v4.28.0 pin where those CompPoly
modules did not yet exist. ArkLib #383 has already partly converged, importing CompPoly's
NovelPolynomialBasis. The residue is the 62 same-named declarations described below.

Blocker 1 (correctness of fit): iteratedQuotientMap cannot express i = ℓ

-- CompPoly/Fields/Binary/AdditiveNTT/Intermediate.lean:163
noncomputable def iteratedQuotientMap (i : Fin ℓ) (k : ℕ)
    (h_bound : i.val + k ≤ ℓ) (x : (sDomain 𝔽q β h_ℓ_add_R_rate) ⟨i, by omega⟩) :
    (sDomain 𝔽q β h_ℓ_add_R_rate) ⟨i.val + k, by omega⟩

i : Fin ℓ excludes i = ℓ, but the hypothesis i.val + k ≤ ℓ clearly contemplates reaching ℓ.
Binius needs the excluded case in normal operation, not as an edge case:

• fiberwiseDisagreementSet is stated with h_destIdx_le : destIdx ≤ ℓ (not <), and its
  steps = 0 specialisation instantiates iteratedQuotientMap (i := destIdx) (k := 0) at that
  bound;
• the final fold of the protocol lands on domain index exactly ℓ.

Proposed fix (strictly more general; no existing consumer breaks, since Fin ℓ ↪ Fin r):

noncomputable def iteratedQuotientMap (i : Fin r) {destIdx : Fin r} {k : ℕ}
    (h_destIdx : destIdx.val = i.val + k) (h_destIdx_le : destIdx.val ≤ ℓ)
    (x : (sDomain 𝔽q β h_ℓ_add_R_rate) i) :
    (sDomain 𝔽q β h_ℓ_add_R_rate) destIdx

Note the second change: taking the destination index as a parameter with an equation, rather
than computing ⟨i.val + k, _⟩ in the result type. Consumers that compose folds otherwise need
Fin.mk congruence and dcast reasoning at every composition; with destIdx explicit, the
transport happens once at the definition site. The old signature is recoverable as a one-liner
(destIdx := ⟨i.val + k, _⟩, h_destIdx := rfl) if a deprecated wrapper is wanted.

Blocker 2 (ergonomics): three index types for one concept

declaration	round-index type
sDomain, qMap, sBasis, normalizedW	Fin r
intermediateNormVpoly, intermediateNovelBasisX, intermediateEvaluationPoly	Fin (ℓ + 1)
iteratedQuotientMap, NTTStage_correctness	Fin ℓ

The domain layer is indexed by Fin r, the polynomial layer by Fin (ℓ+1), the map layer by
Fin ℓ. A consumer holding a Fin r index — which Binius does throughout, because
sDomain : Fin r → …, β : Fin r → L, and its oracle statements are Fin r-indexed — has to
rebuild ⟨i.val, proof⟩ at each crossing and then relate sDomain ⟨i.val, _⟩ back to sDomain i.

Unlike blocker 1 this loses no generality (Fin (ℓ+1) does cover i = ℓ); it is purely friction,
but it is friction at ~32 call sites in Binius alone.

Proposed fix: migrate the Fin (ℓ+1) declarations to Fin r + h_i : i ≤ ℓ, matching the
domain layer, with deprecated wrappers for the old form.

Also worth fixing while in here

ArkLib PR #383's local copy adds [NeZero ℓ] to its variable block, which CompPoly does not have.
If any of that work is upstreamed, do not bring [NeZero ℓ] with it: 8 shared declarations
carry it there, and while two are vestigial (CompPoly's take Fin ℓ, which already forces
ℓ > 0), the rest are a silent narrowing. additiveNTT_correctness and
initial_tiled_coeffs_correctness are otherwise character-identical to CompPoly's but no longer
cover ℓ = 0.

Suggested sequencing

1. Blocker 1 — small, strictly more general, no breakage. Unblocks the most-referenced gap.
2. Blocker 2 — the Fin (ℓ+1) → Fin r migration, with deprecated wrappers.
3. Accept the ~6 declarations ArkLib added on top (getINovelCoeffs, sDomain_eq_of_eq,
   degree_intermediateEvaluationPoly_lt, intermediateEvaluationPoly_from_inovel_coeffs_eq_self,
   iteratedQuotientMap_congr_k, iteratedQuotientMap_succ_comp), some of which become
   unnecessary once destIdx is explicit.
4. ArkLib then deletes its local copy and imports CompPoly.

The proofs for all of this already exist and compile in ArkLib PR #383, so steps 1–3 are largely a
move rather than new work. The one piece of genuine proof work is re-basing the spec↔computable
bridges onto the new signatures: computableAdditiveNTT_eq_additiveNTT,
computableAdditiveNTTFast_eq_additiveNTT, computableNTTStage_eq_NTTStage,
computableTwiddleFactor_eq_twiddleFactor.

Impact if not fixed

ArkLib carries a 3,090-line duplicate of this module, in the same namespace AdditiveNTT, with 62
same-qualified-name declarations that differ in signature. The two cannot be imported together,
and additiveNTT_correctness has two divergent proofs to maintain.

cc @chung-thai-nguyen (author of the ArkLib-side work)

[chung-thai-nguyen]

Thanks for creating this issue, Alex. I can do it within a few days.

[dhsorens]

great, thanks @chung-thai-nguyen ! happy to support as well