Uniform polynomial-time binary modular Frobenius

The single evaluator takes a dividend, modulus, and count through nested pairing. It performs one guarded modular square per count bit using runtime multiplication and remainder. Every state is bounded by the modulus length; a zero modulus gives the empty output. The registered certificate supports composition in subsequent finite-field and condenser programs.

theorem Complexity.BitPolynomial.frobeniusEval_mem_FP : frobeniusEval ∈ FP

Bounded modular Frobenius with three runtime inputs is uniformly polynomial-time.