chore: bump Lean stack to v4.31.0

[quangvdao]

Summary

Migrates ArkLib and its dependency stack from Lean 4.30 to Lean 4.31, ahead of the interaction PR stack (#532, #570, #580).

Dependency updates

• Lean toolchain: v4.30.0 → v4.31.0
• VCVio: v4.30.0 → v4.31.0 (cbd4144, the merged release of chore: complete Lean 4.31 migration VCVio#477)
• CompPoly: v4.30.0 → v4.31.0
• doc-gen4: v4.30.0 → v4.31.0
• refreshed the full Lake manifest, including compatible Mathlib, PolyFun, and Loom2 revisions

VCVio #477 has landed and was released as v4.31.0, so ArkLib now uses the stable tag rather than the temporary PR-head pin used during development.

ArkLib adaptations

• Updated renamed Lean/Mathlib and dependency APIs.
• Removed compatibility lemmas that now live upstream in VCVio or CompPoly.
• Repaired proof elaboration and definitional-equality regressions exposed by Lean 4.31.
• Replaced invalid parameterized instances with explicit definitions where typeclass synthesis cannot infer their construction arguments.

No new sorry or admit declarations were introduced.

Validation

• lake build succeeds: all 4,094 jobs.
• git diff --check succeeds.
• PR documentation-integrity, library-import, and trailing-whitespace checks succeed.

[github-actions]

🤖 PR Summary

This PR migrates the project from Lean 4.30 to Lean 4.31, updating the toolchain, all dependency tags (VCVio, CompPoly, doc-gen4), and the Lake manifest. The bulk of the changes are mechanical adaptations to upstream API changes, including renamed typeclass fields, replaced lemmas, and proof refinements for elaboration and definitional equality. No new sorry or admit are introduced; pre‑existing sorry placeholders in two files remain untouched. The PR also removes several lemmas that now live in the upstream VCVio/CompPoly libraries and converts a few instance declarations to def to reduce typeclass footprint. Several linter warnings are suppressed with set_option. Infrastructure changes include an addition to AGENTS.md and minor lakefile.toml revision updates.

---

Statistics

Metric	Count
📝 Files Changed	80
✅ Lines Added	559
❌ Lines Removed	606

---

Lean Declarations

✏️ Removed: 14 declaration(s)

ArkLib/ToCompPoly/Univariate/Basic.lean (1)

• theorem coeff_eq_zero_of_size_le [Zero R] (p : CPolynomial R) {pos : ℕ} (h : p.size ≤ pos) :

ArkLib/ToVCVio/EvalDist/Defs/Support.lean (2)

• lemma eq_of_mem_support_pure {m : Type → Type} [Monad m] [LawfulMonad m]
• lemma support_bind_exists {m : Type → Type} [Monad m] [LawfulMonad m]

ArkLib/ToVCVio/EvalDist/Instances/OptionT.lean (1)

• lemma OptionT.probEvent_eq_of_run_map_eq {α β : Type}

ArkLib/ToVCVio/OracleComp/Coercions/SubSpec.lean (2)

• lemma liftComp_bind_pure
• lemma mem_support_of_mem_support_liftComp

ArkLib/ToVCVio/OracleComp/EvalDist.lean (1)

• lemma support_ofFn_mapM_index

ArkLib/ToVCVio/OracleComp/SimSemantics/SimulateQ.lean (7)

• lemma OptionT.aux_mem_support_simulateQ_run'
• lemma OptionT.probEvent_eq_one_of_simulateQ_support
• lemma StateT.run'_simulateQ_bind_map_eq_of_body
• lemma map_mk_bind_eq_of_body
• lemma map_run'_eq_of_map_eq {m : Type → Type} {σ α β γ : Type}
• lemma mem_support_bind_mk
• lemma simulateQ_bind_map_eq_of_body

✏️ Affected: 7 declaration(s) (line number changed)

• def projectedCode (C : Set (ι → F)) (T : Finset ι) : Set (T → F) in ArkLib/Data/CodingTheory/Basic/LinearCode.lean moved from L267 to L267
• def projectedWord (c : ι → F) (T : Finset ι) : T → F in ArkLib/Data/CodingTheory/Basic/LinearCode.lean moved from L260 to L260
• def ModuleCode.codewordStackSubmodule : Submodule F (WordStack A κ ι) in ArkLib/Data/CodingTheory/InterleavedCode.lean moved from L173 to L173
• def ModuleCode.moduleInterleavedCode : ModuleCode ι F (InterleavedSymbol A κ) in ArkLib/Data/CodingTheory/InterleavedCode.lean moved from L149 to L149
• @[reducible] private def card_ne_zero (hs' : s'.Nonempty) : NeZero (Finset.card s') where in ArkLib/Data/CodingTheory/ProximityGap/Folding.lean moved from L412 to L412
• def instSDomain {i : Fin r} (h_i : i < ℓ + 𝓡) : in ArkLib/ProofSystem/Binius/BinaryBasefold/Spec.lean moved from L406 to L406
• def booleanHypercubeBasis : Basis (Fin κ → Fin 2) K L in ArkLib/ProofSystem/Binius/FRIBinius/Prelude.lean moved from L43 to L43

---

sorry Tracking

• No sorrys were added, removed, or affected.

---

📋 **Additional Analysis**

The diff consists primarily of version-bump compatibility fixes, mechanical renames, and proof adjustments required by the switch to Lean 4.31.0. No new definitions or substantial contributions that would be evaluated against the project's style and naming guidelines are introduced. Therefore, no findings are reported under the supplied review instructions.

---

📄 **Per-File Summaries**

• AGENTS.md: Added a sentence to the 'Fast Start' section instructing users to run ./scripts/validate.sh in full before committing or pushing, and clarifying that it enforces a zero-warning gate for the ArkLib/Data directory.
• ArkLib/Commitments/Functional/KZG/Binding.lean: The diff restructures the proofs of binding_cond_le_t_sdh_cond, t_sdh_game_eq, and binding without adding or removing any theorems, definitions, or sorrys. In binding_cond_le_t_sdh_cond, the final simpa is replaced with a change that makes the probability inequality explicit, followed by exact hmono. In t_sdh_game_eq, the original simpa is replaced with a dsimp + convert ... using 1 <;> rfl, and the call StateT.map_run'_eq_of_map_eq is simplified by providing the cache argument explicitly. In binding, the concluding convert block is replaced with a change to the target inequality bound and then exact on the same calc chain.
• ArkLib/Commitments/Functional/KZG/Correctness.lean: The correctness theorem was updated: calls to OracleComp.mem_support_of_mem_support_liftComp now include explicit named arguments (superSpec, oa, x), and the inner proof of verifyOpening equality was refactored to use change and simpa only [CPolynomial.ofFn] with KZG.correctness instead of simpa [OracleInterface.answer].
• ArkLib/Commitments/Functional/KZG/FunctionBinding/Basic.lean: The diff modifies proofs in Basic.lean for the FunctionBinding module. In function_binding_game_ext_support_srs and function_binding_game_ext_support_verify_all, simpa using mem_support_pure_iff is replaced by exact (mem_support_pure_iff _ _).mp hx. In the latter lemma, the tuple construction is also changed from using cm_v, queryOf_v, responseOf_v to claim_v.1, claim_v.2.fst, claim_v.2.2.1, reflecting a shift to a claim_v-based representation. In arsdh_game_eq, the StateT.map_run'_eq_of_map_eq call is simplified by removing extraneous implicit arguments. Finally, the proof of theorem function_binding is refactored: convert is replaced by change followed by exact on the same calc block, removing the surrounding parentheses. No sorry or admit are introduced.
• ArkLib/Data/Classes/FunEquiv.lean: In the DFunLike instance, the field coe_injective' was renamed to coe_injective, aligning with a naming update in the DFunLike typeclass.
• ArkLib/Data/CodingTheory/Basic/Distance.lean: In Distance.lean, two proof adjustments were made: (1) In the theorem dist'_eq_dist, the step have h_le now uses exact Finset.min_le hmem_min' instead of simpa with the same lemma, tightening the proof. (2) In the lemma possibleDistsToCode_nonempty_iff, the simp step for the set difference was changed from Set.mem_diff to Set.mem_sdiff, presumably to align with a renamed lemma or to fix a broken simp. No sorry or admit were introduced.
• ArkLib/Data/CodingTheory/Basic/LinearCode.lean: Removed the [Fintype ι] typeclass argument from projectedWord and projectedCode, making them generic over any ι. In projectedCode_linearCombination, replaced a simpa with an explicit change to clarify the equality being proven. In dim_fromRowGenMat, replaced a multi-step convert/simp/rfl proof with a two-line unfold/rw using range_vecMulLinear and Matrix.rank_eq_finrank_span_row. In singletonBound, replaced a simpa with an explicit change/exact to rewrite a hypothesis. No sorry or admit were added.
• ArkLib/Data/CodingTheory/Basic/MDSCode.lean: The proof of lemma IsMDS_of_matrix_IsMDS was simplified: the previous convert block that used Finset.filter_congr and congr_arg to rewrite hammingDist (u - v) into hammingNorm (u - v) was replaced by a single simpa call using hammingNorm, hammingDist, Pi.sub_apply, and sub_ne_zero. The statement of the lemma is unchanged.
• ArkLib/Data/CodingTheory/Basic/RelativeDistance.lean: The diff removes two uses of simp (one inactive simp only at h_dist_le_e and one block converting ENNReal inequalities) and replaces the forward direction of relDistFromCode_le_iff_distFromCode_toENNReal_le with a new proof that uses ENat.toENNReal_le.mpr and Nat.floor_le instead of the earlier ENNReal.ofReal-based calculation. Additionally, the any_goals and case patterns handling distFromCode u C have been eliminated, simplifying the reasoning. No sorry or admit is introduced.
• ArkLib/Data/CodingTheory/DivergenceOfSets.lean: The diff makes several proof simplifications and explicit rewrite adjustments across multiple theorems in DivergenceOfSets.lean. In Pr_uniform_eq_one_imp_forall, the proof of hqTrue is rewritten to avoid a simpa by converting the hypothesis via change and explicitly rewriting PMF.monad_map_eq_map. In proximity_gap_affineSubspace, two proofs are refactored: hx_mem_S replaces a simpa with an explicit change and direct use of hx_mem_affineSpan; h_AffSpanSet is changed from a rw/rfl block to congrArg applied to h_affineSpan; and hUS is adjusted accordingly to use .symm chaining. In reedSolomon_dim_le_deg, the final simpa is replaced by a separate rw of Polynomial.finrank_degreeLT_n at hle and then using hle directly. Across concentration_bounds, the cast_ennreal_eq_iff and cast_ennreal_le_iff lemmas are strengthened to express the equality/inequality at the ℝ≥0 layer explicitly, and multiple uses of simpa and change are rewritten to apply these lemmas with explicit casts. No new declarations or sorry/admit are introduced.
• ArkLib/Data/CodingTheory/GuruswamiSudan/Basic.lean: The diff updates ArkLib/Data/CodingTheory/GuruswamiSudan/Basic.lean by replacing the import Mathlib.Data.Real.Sqrt with Mathlib.Analysis.Real.Sqrt, and restructures several proofs for clarity and correctness. In numVars_eq_of_gt_one, the proof is rewritten to use explicit rw and h_simp instead of simp_all. In numVars_gt_numConstraints_of_gt_one and gs_numVars_gt_numConstraints_of_gt_one, the convert block is split into two separate goals (rfl and the arithmetic step). In linearIndependent_monomials, the proof uses congr_arg with rw and simpa in place of convert. In polySol_ne_zero, simpa now includes polySol. In natWeightedDegree_monomial, the proof is simplified to a single le_antisymm with norm_num. In rootMultiplicity_ge_of_shift_zero, the proof is rewritten to explicitly bind hmem and hdeg'. In toPolynomial_degree_le, simpa replaces a convert to directly apply interpolate_eq_of_degree_lt. No new definitions, theorems, or sorry/admit are introduced.
• ArkLib/Data/CodingTheory/GuruswamiSudan/GuruswamiSudan.lean: Changed the import of Real.Sqrt from Mathlib.Data.Real.Sqrt to Mathlib.Analysis.Real.Sqrt to reflect a path update in Mathlib4, ensuring continued access to the square root API without altering the file's mathematical content.
• ArkLib/Data/CodingTheory/InterleavedCode.lean: The file ArkLib/Data/CodingTheory/InterleavedCode.lean was updated to change instance declarations to def for ModuleCode.moduleInterleavedCode and ModuleCode.codewordStackSubmodule, adjusting their status from typeclass instances to explicit definitions. The import Mathlib.Data.Real.Sqrt was replaced with Mathlib.Analysis.Real.Sqrt. Additionally, the proofs of eq_iff_all_rows_eq, eq_iff_all_symbols_eq, and eq_iff_all_cells_eq in the InterleavedStructure instance for WordStack (and the analogous proof for eq_iff_all_symbols_eq in the InterleavedWord instance) were simplified by removing intermediate local definitions and simp invocations, instead using direct function application and congrArg/congrFun to derive equality.
• ArkLib/Data/CodingTheory/JohnsonBound/Lemmas.lean: Added set_option warning.simp.varHead false before Fis_cover_B to suppress a simp warning. Renamed the lemma sum_eq_sum_diff_singleton_add to sum_eq_sum_sdiff_singleton_add in the proofs of sum_choose_K' and le_sum_choose_K. Refactored the proof of johnson_unrefined, replacing a simpa block with a field_simp using h_n.ne'. Rewrote the equality h_sqrt_eq in johnson_e_div_ne_J to directly express 1 - √(1 - δ) as (e : ℚ) / n via h_muln, h_J_bound, and h_eq.
• ArkLib/Data/CodingTheory/PolishchukSpielman/Degrees.lean: Fixed two convert proof blocks in ps_degree_x_swap_le and ps_degree_x_swap_ge by adding <;> rfl to close trivial subgoals, and added an all_goals rfl to a convert block in ps_exists_x_preserve_nat_degree_y. These changes make the proofs robust to changes in definitional equality for the ps_swap_coeff lemma and the hx.2 term.
• ArkLib/Data/CodingTheory/PolishchukSpielman/Resultant.lean: In ps_resultant_dvd_pow_eval_x, two proof refinements were made: (1) a change tactic was added to rewrite hx0 as eval x (M1 i (.natAdd n j')) = 0, enabling simpa with IsRoot; (2) in the derivation of hdivM1, a simpa [hM1_scale] using det_mul_row v q_mat block was replaced by an explicit rw [hM1_scale] followed by exact det_mul_row v q_mat. No new theorems, definitions, or sorry/admit were introduced.
• ArkLib/Data/CodingTheory/Prelims.lean: The diff makes three changes to ArkLib/Data/CodingTheory/Prelims.lean. First, it adds set_option linter.overlappingInstances false before the lemma rank_eq_if_det_ne_zero to suppress a linter warning about overlapping instances there. Second, it removes the attribute [instance] AffSpanSet.instFinite line, meaning AffSpanSet.instFinite is no longer globally declared as an instance. Third, it fixes a typo in the proof of card_univ_filter_eq by replacing the lemma Finset.card_univ_diff with Finset.card_univ_sdiff.
• ArkLib/Data/CodingTheory/ProximityGap/AHIV22Support.lean: Replaced Finset.card_univ_diff with Finset.card_univ_sdiff in the proof of exists_common_support_of_wt_le (line 157), updating the lemma name after a likely rename in Finset. Refactored the hammingDist_comp calls in the proof of dist_interleaved_code_to_code_lb (lines 270–286) by replacing simpa [Pi.add_apply] with explicit change and direct exact proofs, while keeping the same underlying argument. No new declarations are added; both changes are internal proof adjustments.
• ArkLib/Data/CodingTheory/ProximityGap/BCIKS20/AffineLines/BWMatrix.lean: Summary unavailable — error: 1 validation error for _ProseSummary
  Invalid JSON: expected value at line 1 column 1 [type=json_invalid, input_value='The theorem `RS_exists_n... or sorries were added.', input_type=str]
  For further information visit https://errors.pydantic.dev/2.13/v/json_invalid
• ArkLib/Data/CodingTheory/ProximityGap/BCIKS20/AffineLines/GoodCoeffs.lean: This diff makes two simpa proofs more robust by rewriting them as explicit change/have/rw chains, avoiding reliance on rewriting e and D which are local let definitions.

1. In RS_exists_Pz_of_mem_goodCoeffs, the simpa that closed the goal after hvdist is replaced: it first changes the inequality being proved to the same expressions as in hvdist (avoiding the implicit let e), then simpa using hvdist.\n2. In RS_exists_nonzero_kernelVec_BW_homMatrix_of_goodCoeffs_card_gt, the simpa that derived a zero determinant from the Schur complement condition is replaced with an explicit have hmatrix that factors the submatrix of L - R * (⅟D * A21) as a difference of submatrices, then rws hmatrix and simpas using hdetSchur — this removes the dependency on rewriting the let D in hdetSchur.

• ArkLib/Data/CodingTheory/ProximityGap/BCIKS20/AffineSpaces.lean: Modified the proof of bucket_exists_common_codeword: replaced a convert tactic with simpa using finMapTwoWords and h_dirs_zero j₀ for a clearer and more direct reasoning step.
• ArkLib/Data/CodingTheory/ProximityGap/BCIKS20/ListDecoding/Guruswami.lean: In exists_Pz_of_coeffs_of_close_proximity, the proof step that extracts p from the membership hypothesis hS was refactored: the original simpa using hS is replaced by an explicit change statement that rewrites the type of hS to match the target, followed by exact hS. This is a minor proof-level adjustment with no new definitions, theorems, or added sorry/admit.
• ArkLib/Data/CodingTheory/ProximityGap/BCIKS20/ReedSolomonGap.lean: Fixed two simp-based proofs that broke after upstream changes. In the first change (around line 137), absurd (by convert hclose using 2; simp [ReedSolomon.toFinset]) is replaced by an explicit equality hcoe : (↑(ReedSolomon.toFinset domain deg) : Set (ι → F)) = ReedSolomon.code domain deg, which is then used to rewrite hclose before applying absurd. The second change (around line 232) rewrites simpa using ha and simpa using hb to explicitly rewrite with e and Equiv.setCongr_apply inside a Finset.card_bij block. The original simp at line 140 (simp) is replaced by exact ENNReal.zero_div. No new theorems, definitions, or sorry/admit statements are introduced.
• ArkLib/Data/CodingTheory/ProximityGap/Basic.lean: Added set_option linter.overlappingInstances false in before the definition of multilinear correlated agreement (marked as [Definition 2.3, DG25]) to suppress an overlapping‑instances linter warning for that definition.
• ArkLib/Data/CodingTheory/ProximityGap/DG25/Basic.lean: The diff changes an import from Mathlib.Data.Real.Sqrt to Mathlib.Analysis.Real.Sqrt (likely a Mathlib API restructuring update). It adds set_option linter.overlappingInstances false in before Definition 2.1 (affineLineProximityGaps) and before the definition δ_ε_multilinearCorrelatedAgreement_Nat, suppressing the overlapping instances linter for these declarations.
• ArkLib/Data/CodingTheory/ProximityGap/DG25/MainResults.lean: The diff modifies MainResults.lean by removing several omit-ed typeclass arguments (DecidableEq ι, DecidableEq κ, DecidableEq F, Fintype A, AddCommGroup A, Nonempty ι) from two lemmas (dist_row_le_dist_ToInterleavedWord, dist_row_le_dist_ToInterleavedCode) and instead selectively adding needed instances ([DecidableEq (κ → A)] to the former) and suppressing unused-section-variable and unused-decidable/Fintype-in-type linter warnings via set_option. The proof of dist_row_le_dist_ToInterleavedCode is simplified: the block defining h_dist_row_le_dist_interleaved now uses change and a direct exact call to dist_row_le_dist_ToInterleavedWord U M i instead of simp on the definitions and convert. The proof of affineWord_close_to_affineInterleavedCodeword replaces a apply-convert pair with a single exact le_trans. Two simp only calls and one simp only [ge_iff_le] are removed from the proofs of D_card_le_e_implies_interleaved_correlatedAgreement₂ and R_star_star_upper_bound respectively, and the omit block for D_card_le_e_implies_interleaved_correlatedAgreement₂ is reformatted to put the last argument on the next line. No sorry or admit remain.
• ArkLib/Data/CodingTheory/ProximityGap/Folding.lean: Changed a private instance to a @[reducible] private def for card_ne_zero, which now provides the NeZero instance via aesop rather than being an inline instance. In the proof of folding_preserves_distance, made the simp set explicit by changing simp only [sum_apply] to simp only [Finset.sum_apply], and inserted an explicit change statement showing the goal before applying Fintype.sum_bijective, which reveals the sum index set is Fin (2 ^ k - 1 + 1) and clarifies the use of bijective_cast.
• ArkLib/Data/CodingTheory/ProximityGap/MCAGenerator.lean: Fixed a simp proof block in IsMCA (generatorByRightMul G A) LC x U γ → IsMCA G LC x (matrixMulCodewords A U) γ by replacing a simp block (simp [matrixMulCodewords, ← Matrix.mul_apply, ← Matrix.mul_assoc, hB]) with a more explicit rewrite using Matrix.mulVec_mulVec, hB, and Matrix.one_mulVec. The proof also adds two apply steps (rfl and apply congrArg) to make the term structurally match. No sorry or admit were introduced.
• ArkLib/Data/CodingTheory/ProximityGap/ProximityGenerators.lean: The proof of poly_gen_is_zero_evading was restructured: the convert block with any_goals was replaced by a change to rewrite the goal, a rw to rewrite the function equality, and a refine that directly applies prob_eval_zero_le_div with explicit arguments, followed by a trans_eq to handle the ENNReal.ofReal_div_of_pos step. This makes the proof more explicit and less reliant on automation, but does not alter the logical content.
• ArkLib/Data/CodingTheory/ReedSolomon.lean: In ArkLib/Data/CodingTheory/ReedSolomon.lean, two simpa calls are replaced: the first replaces simpa with simpa only [LinearCode.length] in minDist' (likely a style or performance refinement), and the second replaces simpa with exact in toPolynomial_mem_lt_deg, directly using the equality from hp_eval without rewriting. No new definitions, theorems, or APIs are introduced, and no sorry or admit are added.
• ArkLib/Data/Domain/CosetFftDomain/Defs.lean: The diff modifies CosetFftDomain/Defs.lean. In the FunLike instance, the coe_injective' field is renamed to coe_injective, aligning with a Lean 4 API update. In the private lemma mkSubgroupUnit_injective, the proof step convert congr_arg Units.val hab using 1 is simplified to exact congr_arg Units.val hab, removing an unnecessary convert. No sorrys or admits are added.
• ArkLib/Data/Domain/CosetFftDomain/Log.lean: The proof of log_right_inverse' was rewritten: it no longer uses simp / grind, instead employing a by_cases on fuel < 2 ^ n and a by_cases on the equality of ω at a candidate index to x, with omega for arithmetic reasoning. A set_option linter.flexible false was added before the lemma to suppress a linter warning.
• ArkLib/Data/Domain/CosetFftDomain/Subdomain.lean: In the private lemma subdomain_eval_pow', the proof step convert Iff.rfl was replaced with exact Iff.rfl, simplifying the proof by removing an unnecessary use of convert. No other changes occur in this file.
• ArkLib/Data/Domain/FftDomain/Defs.lean: Renamed the coe_injective' field of the FunLike (FftDomain ι F) ι F instance to coe_injective, aligning it with the standard FunLike naming convention used elsewhere in the codebase or Mathlib. The implementation (the simp and ext block) is unchanged.
• ArkLib/Data/Fin/Tuple/Lemmas.lean: The proof of singleton_append has been refactored to use vappend_left_eq_cons instead of vappend_eq_append, append_left_eq_cons, and fin_cases, and now uses vcons_zero to simplify the rewriting process.
• ArkLib/Data/Hash/DuplexSponge.lean: Two instance declarations were simplified by removing redundant or explicit binder arguments. The NeZero instance for sz.C had its explicit [sz : SpongeSize] binder removed (it is already available as a variable binder). The SpongeState instance for Vector U SpongeSize.N had its explicit {U : Type} [SpongeUnit U] [SpongeSize] binders removed, making them implicit. No semantic changes or new theorems were introduced.
• ArkLib/Data/Lattices/CyclotomicRing/NormBounds/LyubashevskySeiler.lean: The change in LyubashevskySeiler.lean modifies the block inside q_dvd_l2NormSq_of_not_isUnit that derives a non‑unit condition in the quotient ring. Instead of using simpa only [...] to directly rewrite with Rq.toQuotient and quotientHom_apply, the new code first injects an explicit change statement that unfolds the representation of ¬ IsUnit in terms of Ideal.Quotient.mk and the polynomial (powTwoCyclotomic ...).φ.toPoly. This makes the intermediate goal’s structure visible before the subsequent simpa uses hct. No new theorems or definitions are added, no sorry or admit is introduced, and the observable behavior of the theorem remains unchanged. The change is internal: it clarifies the type of hh so that later rewriting succeeds, likely in response to a change in type‑synonym reduction or simpa behaviour in the underlying mathlib4 infrastructure.
• ArkLib/Data/Lattices/CyclotomicRing/NormBounds/MicciancioYoung.lean: The diff removes two change tactic invocations from the private lemma negacyc_reindex in MicciancioYoung.lean. These lines were rewriting the goal to the equivalent forms ((a + n - i) % n + i) % n = a and ((a + i) % n + n - i) % n = a respectively; their removal simplifies the proof script without affecting the lemma's statement or proof.
• ArkLib/Data/Lattices/CyclotomicRing/Subfield/NormBound.lean: 在定理 coeff_psi_abs_le_two_vecCInfNorm 的证明中，一处使用 omega 自动证明的调用被替换为显式使用 Nat.le_of_not_gt hpos，其中 hpos 是同一分支中 by_cases 得到的假设。该改动不改变逻辑，仅调整了证明风格。
• ArkLib/Data/Lattices/CyclotomicRing/Subfield/TraceVanishing.lean: Removed several dsimp only calls (lines 151, 276, 304, 307) that were unnecessary, streamlining the proof without affecting the logical content.
• ArkLib/Data/MvPolynomial/Interpolation.lean: Summary unavailable — error: 1 validation error for _ProseSummary
  Invalid JSON: expected value at line 1 column 1 [type=json_invalid, input_value="The diff rewrites two pr...ze of the target field.", input_type=str]
  For further information visit https://errors.pydantic.dev/2.13/v/json_invalid
• ArkLib/Data/MvPolynomial/LinearMvExtension.lean: In linearMvExtension_degreeOf_lt, the calc block's inner step was refactored from a convert to an explicit change + exact MvPolynomial.degreeOf_sum_le, making the proof more direct. The main change is in powContraction_is_right_inverse_to_linearMvExtension: the proof was rewritten to extract a key inequality hnat : (p : Polynomial F).natDegree < 2 ^ m by using Polynomial.mem_degreeLT.mp and Polynomial.natDegree_lt_iff_degree_lt, then using this lemma to simplify the call to Polynomial.sum_over_range' (removing the manual case split) and to replace the final convert + second convert block with a single rw and convert (Polynomial.as_sum_range' p.val (2 ^ m) hnat).symm, followed by a simp. No new theorems were added and the statement remains unchanged; the proof is cleaned up by factoring out hnat and uniformly applying it.
• ArkLib/Data/MvPolynomial/Multilinear.lean: The proof of singleEqPolynomial_degreeOf was modified by replacing two simpa only [h] invocations with simpa [h]. This removes the only modifier, allowing simpa to use the full set of lemmas in the context rather than restricting to the explicitly listed ones.
• ArkLib/Data/Polynomial/Bivariate.lean: Updated the proof of natDeg_sum_eq_of_unique in Bivariate.lean to replace the deprecated lemma Finset.sum_eq_sum_diff_singleton_add with its renamed counterpart Finset.sum_eq_sum_sdiff_singleton_add, reflecting an upstream renaming in the Finset API.
• ArkLib/Data/Polynomial/FoldingPolynomial.lean: In ArkLib/Data/Polynomial/FoldingPolynomial.lean, two proof blocks were cleaned up. In folding_polynomial_is_unique, the convert tactic was replaced with unfold natDegreeY followed by exact Polynomial.natDegree_sub_le _ _. In folded_poly_degree_bound, a simp +decide only that was not needed (likely a simp call whose conclusion was already subsumed by the subsequent step) was removed.
• ArkLib/Data/Polynomial/RationalFunctions.lean: The proof of regularElms_set_liftToFunctionField was refactored: the original simpa was replaced with an explicit change followed by exact, both invoking regularElms_set_liftBivariate H (Polynomial.C p). This is a purely stylistic refactor — the lemma's statement and semantics remain identical.
• ArkLib/OracleReduction/Basic.lean: Removed two by simpa only using resp wrappers in the toOracleVerifier function, replacing them with just resp because the type now matches directly, simplifying the construction of queryResponsesOStmt and queryResponsesOMsg.
• ArkLib/OracleReduction/Composition/Sequential/Append.lean: The StateFunction.append definition is refactored: the second-case branch now uses an intermediate lemma hm and a local definition transcript₁ to simplify the conjunct, and the toFun_empty case is rewritten using explicit heq_of_eq and Fin.elim0 instead of funext. The theorem append_perfectCompleteness is simplified to avoid unfold/convert, using change and simpa with zero_add. The definition still contains sorry placeholders for the toFun_next and toFun_full proofs.
• ArkLib/OracleReduction/Composition/Sequential/General.lean: The seqCompose_rbrSoundness and seqCompose_rbrKnowledgeSoundness theorems now use Subsingleton.elim and heq_of_eq with explicit Fin.elim0 calls to handle the empty index case, replacing the prior direct funext over Fin in the base case of their induction. The seqCompose_perfectCompleteness theorem was refactored: it no longer uses unfold and convert but instead changes its statement to express the result as a completeness claim (with the additional parameter 0), then deduces the original conclusion via simpa using seqCompose_completeness. These adjustments improve type‑level compatibility and proof structuring without altering the logical content.
• ArkLib/OracleReduction/LiftContext/Reduction.lean: Removed a simp at hR tactic invocation that was redundant with the subsequent simp line in the proof of liftContext_knowledgeSoundness. No new theorems, definitions, or sorries were introduced.
• ArkLib/OracleReduction/OracleInterface.lean: Renamed the fields decidableEq_A, decidableEq_B, fintype_B, and inhabited_B to decidableEqA, decidableEqB, fintypeB, and inhabitedB respectively in the DecidableEq, Fintype, and Inhabited instances for the indexed oracle type [v]ₒ. This change adjusts the field names to match updated Lean 4 naming conventions (stripping underscores). No definitions were added or removed, and the instances' logic remains identical.
• ArkLib/OracleReduction/ProtocolSpec/Basic.lean: Renamed fields in three refine blocks within OracleSpec instance implementations: changed decidableEq_A and decidableEq_B to decidableEqA and decidableEqB in the OracleSpec.DecidableEq instance for srChallengeOracle, and changed fintype_B to fintypeB in the two OracleSpec.Fintype instances for srChallengeOracle and fsChallengeOracle. This aligns the field names with the current structure definitions (removing underscores for consistency).
• ArkLib/OracleReduction/Salt.lean: In ArkLib/OracleReduction/Salt.lean, the return type of Transcript.extractSalt was refined: its proof component, previously by simpa using i.property, is now an explicit have block that uses Fin.take and Direction.P_to_V to construct the equality. This tightens the specification of the salt extraction mapping, ensuring the direction constraint is expressed in terms of Fin.take rather than relying on a more generic simpa. No other changes appear in the file.
• ArkLib/OracleReduction/Security/RoundByRound.lean: Changed the proof of OracleVerifier.id_rbrKnowledgeSoundness from convert Verifier.id_rbrKnowledgeSoundness ... to exact Verifier.id_rbrKnowledgeSoundness ..., eliminating a type conversion and making the proof a direct application of the non-oracle version.
• ArkLib/OracleReduction/Security/TranscriptTree/Composition.lean: The proofs of RightProj.tree_isStructured, SplitData.fst_isStructured, and SplitData.sndAt_isStructured were refactored: each case that previously used simpa with IsStructured now introduces explicit hround lemmas (using Fin.ext and omega) to equate round indices (e.g., Fin.natAdd and rightRound, Fin.castAdd and leftRound), then applies convert with the symmetry of that equality. This makes the index arithmetic used in the IsStructured condition explicit, avoiding reliance on simpa and improving proof robustness.
• ArkLib/ProofSystem/BatchedFri/Security.lean: Renamed Finset.sum_eq_sum_diff_singleton_add to Finset.sum_eq_sum_sdiff_singleton_add in the proof of cosetEnum; removed a redundant congr_arg Subtype.val h line in fin_equiv_coset; renamed instance fields inhabited_B to inhabitedB and fintype_B to fintypeB in multiple Inhabited and Fintype instances; and replaced simpa with change + explicit inferInstance in the Inhabited and Fintype instances for the combined challenge protocol.
• ArkLib/ProofSystem/BatchedFri/Spec/SingleRound.lean: In the batchVerifier definition, the proof of the hEq field was changed from by simp to by intro i; rfl, making the equality hold by reflexivity for each index i instead of relying on simplification.
• ArkLib/ProofSystem/Binius/BinaryBasefold/CoreInteractionPhase.lean: Summary unavailable — error: 1 validation error for _ProseSummary
  Invalid JSON: expected value at line 1 column 1 [type=json_invalid, input_value='The proofs in foldRelay...admit were introduced.', input_type=str]
  For further information visit https://errors.pydantic.dev/2.13/v/json_invalid
• ArkLib/ProofSystem/Binius/BinaryBasefold/General.lean: In General.lean, the instance declaration for OracleInterface was changed from a globally scoped instance with an explicit Empty binder to a local instance on OracleInterface Unit. This restricts the instance’s visibility to the current section or file, preventing it from leaking into other contexts where it might cause unwanted instance resolution or conflicts.
• ArkLib/ProofSystem/Binius/BinaryBasefold/QueryPhase.lean: The diff removes two unused simp lines (one in proximityChecksSpec and one in queryOracleVerifier) that were rewriting the same fiber_point_num_repr hypothesis, and replaces a simpa using OracleSpec.query ... with a direct exact OracleSpec.query ... in queryCodeword, eliminating a redundant simpa call. No new definitions, theorems, or structures are introduced, and no sorry or admit appears in the changed code.
• ArkLib/ProofSystem/Binius/BinaryBasefold/Spec.lean: Changed the instSDomain declaration for SampleableType on sDomain from an instance to a def. This is a significant signature change that will affect how instances are synthesized: previously it was an automatically-used instance, now it must be explicitly requested. The modification impacts all downstream code that relies on instSDomain being available as an instance for typeclass resolution.
• ArkLib/ProofSystem/Binius/BinaryBasefold/Steps.lean: The diff changes the hEq field of the relayOracleVerifier term from by simp only to by rfl. This is likely a semantic correctness or performance improvement: simp might have been unnecessarily complex or may not hold in certain contexts, while rfl trivially establishes definitional equality for the dependent function fun oracleIdx => ....
• ArkLib/ProofSystem/Binius/FRIBinius/Prelude.lean: Changed the booleanHypercubeBasis declaration from an instance to a def in ArkLib/ProofSystem/Binius/FRIBinius/Prelude.lean. This modifies how the basis is exported and available for typeclass search; previously it was an instance, meaning it could be automatically found, and now it is a plain definition that must be explicitly invoked. No other definitions, lemmas, or signatures were changed; the card_bool_hypercube_eq, hypercubeEquivFin, and linearIndependentBooleanHypercubeBasis declarations remain unchanged.
• ArkLib/ProofSystem/Component/RandomQuery.lean: In RandomQuery.lean, the stateFunction and knowledgeStateFunction definitions were modified at the case for index 1: previously each used simpa [pSpec] to coerce the challenge into a Query OStatement; now they replace that pattern with a let q := chal ... followed by a change Query OStatement at q tactic to adjust the type directly, avoiding the explicit use of pSpec in that step. No other changes, new definitions, or sorrys were introduced.
• ArkLib/ProofSystem/Component/SendClaim.lean: In ArkLib/ProofSystem/Component/SendClaim.lean, the proof of completeness (theorem with [Nonempty σ]) was modified at a single refine statement: the first component of the provided tuple was changed from trivial to rfl. No other changes were made, and no sorry or admit were introduced.
• ArkLib/ProofSystem/Fri/Spec/SingleRound.lean: The diff modifies several proofs in SingleRound.lean without changing the external API. In witness_lift, the rewrite block is replaced with explicit change and rw using Nat.div_lt_iff_lt_mul and mul_comm, and a have for Nat.instPreorder.toLT equality is added. In finalFoldProver, two simpas are replaced: one with change and exact for the witness_lift application, and another with rw [if_neg h] and exact for the else branch of an if. In getConst, simpa using () is replaced with change Unit; exact (). In queryCodeword, the simp cast and simpa are replaced with simp only [range_lem₁] and a cast block that unfolds OracleInterface.Query and finalOracleStatementInterface and uses congr 3. In queryVerifier, three simpa calls are replaced with exact using FftDomain.mem_toFinset_iff_mem.mp and CosetFftDomain.mem_toFinset_iff_mem.mp for membership proofs. No sorry or admit are introduced.
• ArkLib/ProofSystem/RingSwitching/General.lean: Added a second bullet case to the proof of fullOracleVerifier_rbrKnowledgeSoundness in ArkLib/ProofSystem/RingSwitching/General.lean, using rfl to close a new subgoal introduced by the convert tactic. The first bullet (starting with simp only) remains unfinished and still contains a sorry.
• ArkLib/ProofSystem/Stir/Combine.lean: In lemma combine_eq_flat, added omega to close an arithmetic goal. In lemma degreeCor_eq, restructured the proof into two branches: the first uses rfl, and the second uses rw with Nat.cast_add, Nat.cast_sub hd, Nat.cast_one followed by split_ifs and ring, likely to refine the use of geom_sum_cases and improve proof robustness.
• ArkLib/ProofSystem/Sumcheck/Domain.lean: The proof of sum_cube_succ was refactored: a new local lemma htail was introduced equating D.tail.cube to Fintype.piFinset (Fin.tail D.points), and then used to simplify the simpa that establishes the hcube equality, replacing the previous use of tail and points in the simpa with just cube after rewriting. The theorem statement and its overall logical content remain unchanged.
• ArkLib/ProofSystem/Sumcheck/Structured.lean: The function projectToNextSumcheckPolyWithDegree is modified to add a dimension-simplification step (hdim) that rewrites ℓ - i.succ to ℓ - i - 1 using omega, and then rewrites with hdim before constructing the projected polynomial. The simpa call is updated to simpa only [projectedH] to explicitly expose the local binding when applying the fixFirstVariablesOfMQP_degreeLE lemma. No new definitions or theorems are introduced; no sorry or admit are added.
• ArkLib/ProofSystem/Sumcheck/Structured/SingleRound.lean: In getRoundProverFinalOutput, the construction of the projected polynomial projectedH is refactored: a new lemma hvars establishing ℓ - i - 1 = ℓ - i.succ is added, the result of fixFirstVariablesOfMQP is stored as rawProjectedH, and projectedH is obtained by cast using this equality. The degree-bound proof is updated accordingly, replacing a simpa with dsimp and cases hvars before applying fixFirstVariablesOfMQP_degreeLE. This change clarifies the type conversion that was previously implicit.
• ArkLib/ToCompPoly/Univariate/Basic.lean: The diff removes the theorem coeff_eq_zero_of_size_le (which stated that p.coeff pos = 0 whenever p.size ≤ pos) and refactors the proofs of two private lemmas: Raw.toPoly_ne_zero_of_size_pos (now uses change and congrArg instead of simpa [cp]) and divModByMonicAux_step_degree_lt (now uses an explicit rw block with ring instead of convert ... using 2; ring). No new sorry or admit are introduced.
• ArkLib/ToVCVio/EvalDist/Defs/Support.lean: Removed the lemmas support_bind_exists and eq_of_mem_support_pure (which previously stated that membership in the support of a bind implies existence of an element in support of the first component, and that membership in the support of a pure forces equality). They are now provided directly by VCVio, so the file is reduced to a compatibility comment.
• ArkLib/ToVCVio/EvalDist/Instances/OptionT.lean: The file ArkLib/ToVCVio/EvalDist/Instances/OptionT.lean was reduced to a compatibility import stub: the lemma OptionT.probEvent_eq_of_run_map_eq (which related probabilities of events under an OptionT ProbComp when runs are related by Option.map) and its supporting imports (VCVio.EvalDist.Monad.Map, VCVio.OracleComp.ProbComp) were removed, and the documentation block was replaced with a single comment indicating that the additions now live in VCVio. The remaining import VCVio.EvalDist.Instances.OptionT ensures backward compatibility.
• ArkLib/ToVCVio/OracleComp/Coercions/SubSpec.lean: This diff removes the lemmas mem_support_of_mem_support_liftComp and liftComp_bind_pure from SubSpec.lean. These lemmas were previously defined in this file but are now apparently provided elsewhere (presumably in the upstream VCVio library being imported); their removal here avoids duplication and potential conflicts. The file now retains only the bind_liftComp_map lemma, which continues to exist in the same location.
• ArkLib/ToVCVio/OracleComp/EvalDist.lean: The diff removes the lemma support_ofFn_mapM_index (in the OracleComp namespace) and its enclosing namespace OracleComp block. This lemma previously asserted that for (Vector.ofFn id).mapM f, any element in the support of the monadic mapM has each component lying in the support of the corresponding inner computation, using Vector.support_mapM_index. Its deletion means that callers relying on this lemma must now obtain it from another source or adjust their proofs.
• ArkLib/ToVCVio/OracleComp/SimSemantics/SimulateQ.lean: The diff removes three imports (ArkLib.ToVCVio.EvalDist.Instances.OptionT, ArkLib.ToVCVio.OracleComp.Coercions.SubSpec, VCVio.EvalDist.Defs.NeverFails), adds import ArkLib.ToVCVio.ToMathlib.Control.StateT, and corrects a typo in the module docstring (VCV-io → VCVio). It deletes the entire block of code after simulateQ_randomOracle_map_uniformFin, which consisted of the lemmas OptionT.probEvent_eq_one_of_simulateQ_support, OptionT.aux_mem_support_simulateQ_run', OptionT.mem_support_bind_mk, OptionT.map_mk_bind_eq_of_body, StateT.map_run'_eq_of_map_eq, simulateQ_bind_map_eq_of_body, and StateT.run'_simulateQ_bind_map_eq_of_body, along with the OptionT and StateT namespaces. The only remaining content in the file is the lemma simulateQ_randomOracle_map_uniformFin (which was already present).
• lakefile.toml: Updated three dependency revisions in lakefile.toml to v4.31.0: VCVio, doc-gen4, and CompPoly each now point to the newer tag. The checkdecls dependency remains at lean4.18.0.
• lean-toolchain: (minor changes, +1/-1)
• 1 file(s) filtered as noise (lockfiles, generated, or trivial): lake-manifest.json

---

Last updated: 2026-07-12 13:35 UTC.

[chatgpt-codex-connector]

💡 Codex Review

Here are some automated review suggestions for this pull request.

Reviewed commit: 271b36abf7

ℹ️ About Codex in GitHub

Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you

• Open a pull request for review
• Mark a draft as ready
• Comment "@codex review".

If Codex has suggestions, it will comment; otherwise it will react with 👍.

Codex can also answer questions or update the PR. Try commenting "@codex address that feedback".