[aliromman]

Prove polynomial rational size and bit cost for the complete inverse-circuit certificate producer and its separately transcribed checker. The source already bounds field operations; this result also bounds the numerators, denominators and elimination coordinates. Both equality certificates and shortest nonzero coefficient words have polynomial encoding size. This closes the producer-size gap before the orthogonal-witness and funded-detector interfaces. The complete kappa calculation and selected frontier remain unchanged.

The proof, budget calculator and exact audit, receipt, and source pins define the result.

The contract retains all independent inputs and returned roles, old values on aliased queries, and true named-generator inverses. Inputs use explicit integers or integer/fraction strings; unreduced operands are charged. The new budget interface rejects compressed decimal/exponent syntax before expansion. The upstream parser is unchanged. The theorem covers this explicit rational encoding, with Python's integer-string limit disabled by the standard per-process option below.

For D=r+q, a common denominator and scalar-gain bound control the compiled matrices. Scale every candidate path row to one integer lattice. Pivot minors then bound the normalized echelon rows, their original-row coordinates and every closure coefficient. A separate bound includes unreduced arithmetic temporaries. These steps convert the existing field-operation count into a polynomial bit-time and space bound. The bounds are conservative; this is neither a practical speedup nor an optimal-size result.

@krzysztofwojt supplied the compiler, reachable-basis search, independent checker, exact oracles and shortest-word theorem in PR #5262, consumed at 6f92ccf1e61c4668c8ee687bd1df8b42932b8759. Those files are unchanged. The retained source proof preserves @zxv's PR #5235, the dirty-echo/tensor/phase lineage and classical Magnus, rational-series and weighted-automata credit. Cramer's rule, determinant height bounds and polynomial exact linear algebra are classical. No new general equivalence algorithm or global literature priority is claimed.

Ali Romman's PR #5315, head 9bebc267c4608e51fcc94a543b8e0d66077cdfbb, supplies the orthogonal construction; PR #5339, head 26fe40cbca6972a0e392e9248a9cb8a84368530b, supplies the detector bound after the word is given. Their orthogonal proof and precision proof are retained for the composition corollary. Their full replays were not rerun in this package. Prepared by Ali Romman with substantial OpenAI Codex assistance; Apache-2.0.

Base: current main ff3cc58e370d0f678e529246f8c73e8094e18fcf, priority revision 7. Eleven consumed files are retained byte-exact at ancestor 5fb9c3ee9a4073b7085d7b5b8e7d8f524e1e520c. The replay does not need unmerged upstream Git objects.

Python 3.12 and the standard library:

python3.12 -B scripts/research_package.py --package research/inverse-certificate-bit-bounds

The registered normal and optimized commands include -X int_max_str_digits=0 and both pass with PASS_INVERSE_CERTIFICATE_BIT_BOUNDS. All 99 programs pass: 36 equality certificates, 63 nonzero words, 98 independent reduced-word comparisons and 63 exact matrix witnesses. Cases include a 16,001-bit scalar, large unreduced fractions, coprime denominators, near dependencies, delayed inverse tails, dirty returns and aliases. The weighted 2^64-word case uses 260 states and 64 invariant rows; its certificate coefficients need at most 254 bits. Nine controls and three separate edge audits pass. Four actual code mutations fail in both modes for mathematical reasons.

Committed bytes, every declared source pin's direct ancestry, official export integrity and both read-only Git-free replays pass; all 21 exported files remain unchanged. The full-history wrapper is unpassed in this shallow checkout. No independent human/proof-kernel review, selected cold replay, Lean, Docker, native tape or complete compiler/kappa calculation was run. A native adapter still needs one pinned caller with all extra operator relations, types, phases, storage and paid-call costs. Polynomial certificate size does not supply that admission.

Hosted run 40002911314 passed planning and the registered Linux replay for published head b6a8111fe26b2ab4eb24d56f46ae0da3ec7182e4. Hosted execution is separate from independent scientific review.

[jwr404]

Independent review (James Reed, with Claude Code). Head b6a8111fe26b2ab4eb24d56f46ae0da3ec7182e4.

Verdict: the height bounds are correct as written, and the receipt is consistent with them.

Proof check

• §3. If entries of E are at most G with denominators dividing Q, then (E^j) entries are at most D^(j−1) G^j ≤ (DG)^j. So H = Σ_{j<D} E^j has entries at most Σ(DG)^j ≤ (1+DG)^D = K, with denominators dividing Q^(D−1). T_a = H A_a then has entries at most DKG with denominator dividing Q^D = R, so R·|T|, R·|U|, R·|V| ≤ 2DGKR = M. ✓
• §4. A length-k row is a product of k+1 matrices with entries at most M/R. Scaled by Z = R^(D+1) it is at most R^(D−k) D^k M^(k+1) ≤ D^D M^(D+1) = N, using R ≤ M, and Z ≤ N. ✓ The projected coefficient adds one factor, matching bCoeff = (D+1)bD + (D+2)bM + 1. ✓
• §5. Cramer and bordered minors of the integer Z-scaled rows are at most j! N^j ≤ D! N^D = Δ. The normalized-row inequality Z j! N^j ≤ (j+1)! N^(j+1) holds since Z ≤ N. ✓ The amplification example is right: for rows (1,1) and (1,1+1/L), the coordinates of (0,1) are (−L, L).
• (2) dominates its logarithms.
  • log₂(1+DG) ≤ bD + bG, since 1 + DG ≤ 2^(bD+bG), so bM has slack.
  • log₂ N ≤ D·bD + (D+1)·bM and log₂ Δ ≤ D(bD + bN). ✓

One suggestion: §3's claim that every entry of E is at most G in magnitude carries the whole chain. A short displayed induction (row sum at most the product of β over the instructions so far, and a coefficient occurrence used at most once per dependency path) would make that step as explicit as §4–§5.

Receipt

The registered replay passes locally (PASS_REGISTERED_RESEARCH_PACKAGE, 141 s). I checked RESULT.json independently: across all 99 cases, every observed height (model, path, residual, echelon, coordinate, projection) is within its stated bound, with 0 violations. The maximum observed/bound ratios are 0.5 (model), 0.25 (path, coordinate, residual), 0.17 (projection) and 0.06 (echelon), so the bounds are conservative as advertised. The largest case, explicit-16001-bit-scalar, observes 16,001-bit coordinates against a minor bound of 64,018 bits. The minor_amplification_bits = 1025 control matches the L = 2^1024 + 1 example.