Function prove 

pub fn prove<'a, A, F, P>(
    alloc: &A,
    gamma: F,
    tables: impl IntoIterator<Item = TableLookup<'a, P>>,
    channel: &mut impl IPProverChannel<F>,
) -> LogupOutput<F>
where
    A: Allocator,
    F: BinaryField<Underlier: Divisible<u64>>,
    P: PackedField<Scalar = F> + 'a,

Prove a logUp* indexed-lookup reduction.

This is the prover for binius_ip::logup_star::verify_reduction. It produces the transcript the verifier consumes and returns the same reduced claims.

The reduction proves the indexed lookups (I_j^* T_{t(j)})(r_j) = e_j for one or more lookers reading one or more tables. The lookers batch by a random linear combination: a challenge gamma scales looker j’s equality-indicator numerator by gamma^j across the whole batch, and table t’s pushforward is the gamma-weighted sum of the pushforwards of the lookers that read it, still with only 2^m_t entries. The looked-up vectors are never committed. Every fractional-addition circuit — looker j’s over n_j variables and table t’s over m_t — is an instance of one GKR of ceil(log2(#lookers + #tables)) + max(max_j n_j, max_t m_t) layers, with every shallower instance padded by zero fractions. Neither the lookers nor the tables need agree on a length.

Each table is randomized by its own logUp challenge c_t, which is what makes the single root check certify every table separately; see binius_ip::logup_star::verify_reduction. See Soukhanov25 for the construction.

Arguments

• tables - The table multilinears T_t, each over its own m_t variables.
• lookers - The looker columns and claims; each names the table it reads, evaluation points may differ in length, looker j’s index column must have 2^n_j entries, and every index entry must be less than the size of the table it reads.
• channel - The prover channel for sending messages and sampling challenges.

The logUp challenges are sampled against the committed I_j, T_t, and pushforwards Y_t. So the caller must absorb those commitments into the transcript before calling this routine.

Preconditions

• tables is non-empty and each has at least one variable, so every table-side GKR has a variable to split on.
• Every eval_claim must equal (I_j^* T_{t(j)})(r_j), or the proof will not verify.

Returns

The reduced claims on the tables, the pushforwards, and the per-looker index multilinears. The index claims are drawn from one point spanning the deepest looker; looker j is claimed at its last n_j coordinates. The table claims are drawn from one point spanning the widest table; table t is claimed at its first m_t coordinates. The caller verifies those claims, which is out of scope here.