feat: Define BN254 curve - #138
Merged
Merged
Conversation
katyhr
pushed a commit
to NethermindEth/ArkLibFri
that referenced
this pull request
Sep 16, 2025
* add base prime field for BN254 * lint whitespace * more definitions * wip * remove hand-rolled point addition (already exists in mathlib) * add warning
SYMBaiEX
pushed a commit
to SYMBaiEX/ArkLib
that referenced
this pull request
Jun 7, 2026
SYMBaiEX
pushed a commit
to SYMBaiEX/ArkLib
that referenced
this pull request
Jun 7, 2026
SYMBaiEX
pushed a commit
to SYMBaiEX/ArkLib
that referenced
this pull request
Jun 7, 2026
SYMBaiEX
pushed a commit
to SYMBaiEX/ArkLib
that referenced
this pull request
Jun 7, 2026
SYMBaiEX
pushed a commit
to SYMBaiEX/ArkLib
that referenced
this pull request
Jun 7, 2026
SYMBaiEX
pushed a commit
to SYMBaiEX/ArkLib
that referenced
this pull request
Jun 7, 2026
SYMBaiEX
pushed a commit
to SYMBaiEX/ArkLib
that referenced
this pull request
Jun 7, 2026
SYMBaiEX
pushed a commit
to SYMBaiEX/ArkLib
that referenced
this pull request
Jun 7, 2026
SYMBaiEX
pushed a commit
to SYMBaiEX/ArkLib
that referenced
this pull request
Jun 7, 2026
SYMBaiEX
pushed a commit
to SYMBaiEX/ArkLib
that referenced
this pull request
Jun 7, 2026
SYMBaiEX
pushed a commit
to SYMBaiEX/ArkLib
that referenced
this pull request
Jun 7, 2026
SYMBaiEX
pushed a commit
to SYMBaiEX/ArkLib
that referenced
this pull request
Jun 7, 2026
SYMBaiEX
pushed a commit
to SYMBaiEX/ArkLib
that referenced
this pull request
Jun 7, 2026
…t to its successor weight core (axiom-clean) The P1 analogue of the now-proven monic P2 match (Verified-zkEVM#139, `restrictedFaaDiBrunoMatch_of_monic`). For monic `H` three of the four inputs to `of_normalized_divWeight_cases_succLift` are discharged axiom-clean — the successor lift identity (`P2_closed_of_leadingCoeff_one`), the base (`βHensel_zero_weight_le_one` + `W𝒪 = 1`), and the `W`-factor collapse — so the full `AlphaGenuineRegularWeightLe` follows from a single explicit hypothesis `SuccDivWeightLe_of_monic`: each `βHensel (t+1)` is `ξ^{2t+1}`-divisible in `𝒪 H` with a quotient of `Λ_𝒪`-weight `≤ 1`. This pins the open Verified-zkEVM#138 obligation (monic WLOG case) to exactly the BCIKS20 Newton ξ-order-gain / weight-1 regularity core, carried as a `Prop` hypothesis — no `axiom`, no `sorry`. Verified `#print axioms`: [propext, Classical.choice, Quot.sound]. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
SYMBaiEX
pushed a commit
to SYMBaiEX/ArkLib
that referenced
this pull request
Jun 7, 2026
Add `ArkLib/ToMathlib/LinearizedKernel.lean`: the kernel identities for
linearized / q-additive polynomials and BKR06 subspace polynomials, absent
from mathlib. For a finite field `F` with `q = |F|`:
* `prod_X_sub_C_univ_eq_pow_card_sub`: base-field subspace polynomial
`∏_{c∈F} (X - C c) = X^q - X`.
* `prod_X_sub_C_algebraMap_eq_pow_card_sub`: its image in an extension `K`.
* `prod_X_sub_C_smul_eq`: the scaled linearized kernel
`∏_{c∈F} (X - C (a·ι c)) = X^q - C(a^{q-1})·X` for `a ≠ 0`,
the engine of the q-linearized recursion
`s_{V'⊕F·u}(X) = s_{V'}(X)^q - s_{V'}(u)^{q-1}·s_{V'}(X)`.
All declarations are `sorry`/`axiom`-free; `#print axioms` shows only
`[propext, Classical.choice, Quot.sound]`. The file imports only Mathlib
(no ArkLib dependencies). Feeds the BKR06 list-size argument (Verified-zkEVM#138/proximity).
Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
SYMBaiEX
pushed a commit
to SYMBaiEX/ArkLib
that referenced
this pull request
Jun 7, 2026
…_le axiom — prove the BCIKS20 B_coeff weight bound
Replace `axiom B_coeff_weight_le` with a kernel-clean `theorem`, assembled from the
existing proven ingredients via the degree-decomposition route:
B_coeff_weight_le_hasse ▸ weight_Λ_over_𝒪_le_of_mk_eq ▸
weight_Λ_le_natDegreeY_mul_add_degreeX ▸ hasseCoeffRepr𝒪_natDegreeY_le.
Verified `#print axioms` ⊆ {propext, Classical.choice, Quot.sound} (no sorryAx, no custom
axiom); the full file recompiles clean. Remove its scripts/residual_axioms.txt entry.
Co-authored-by: Eliza <elizamakesmagic@gmail.com>
SYMBaiEX
pushed a commit
to SYMBaiEX/ArkLib
that referenced
this pull request
Jun 7, 2026
…cleared base
Add the cleared *successor* target to AlphaWeight.lean, mirroring the
landed cleared base witness alphaWeight_zero_cleared_fixed. Clearing the
full W^{t+2}*xi^{2t+1} denominator off alphaGenuine (t+1) makes betaHensel
(t+1) itself the O-preimage (supplied by the lift identity) -- so no
W-divisibility obstruction survives clearing. The genuine residual
separates to ONLY the weight bound on betaHensel (t+1) (the per-term WALL
for t>=1).
New declarations (axiom-clean, [propext, Classical.choice, Quot.sound]):
- AlphaGenuineRegularWeightLe_succ_cleared (predicate)
- AlphaGenuineRegularWeightLe_succ_cleared.of_lift
- DivWeightLe_succ_cleared (predicate) + of_betaWeight / betaWeight
- divWeight_succ_cleared_iff_betaWeight_succ
- AlphaGenuineRegularWeightLe_succ_cleared.of_divWeight_succ_cleared
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
SYMBaiEX
pushed a commit
to SYMBaiEX/ArkLib
that referenced
this pull request
Jun 7, 2026
…Of…cleared_uniform residual axiom with proven lemma The residual axiom embeddingOf_hasseCoeffReprO_cleared_uniform_residual asserted the W-clearing identity at clearing power k₀ = R.natDegree - deltaSave i1 - m. For i1 = 0 (deltaSave = 1) that demands natDegreeY p ≤ R.natDegree - 1 - m, strictly sharper than the true bound natDegreeY p ≤ R.natDegree - m (the iterated-Hasse representative p has Y-degree exactly R.natDegree - m generically — neither evalX (C x₀) nor Δ_X^0 removes the top power). So the axiom was unsound on that branch; it was consumed only by a dead wrapper. Replace it with a correct, kernel-clean lemma at the natural clearing power k = natDegreeY p, proven from the existing conditional identity embeddingOf𝒪Into𝕃_hasseCoeffRepr𝒪_cleared (hypothesis natDegreeY p ≤ natDegreeY p is reflexive). Empirically verified: i1≠0 branch of the old bound is provable, i1=0 branch is not (omega counterexample). Remove residual_axioms.txt entry. Co-authored-by: Eliza <elizamakesmagic@gmail.com>
SYMBaiEX
pushed a commit
to SYMBaiEX/ArkLib
that referenced
this pull request
Jun 7, 2026
…ndary per issue) Records the exact remaining mathematical content of every open ArkLib issue and whether it is closable from in-tree+mathlib facts vs. external-paper formalization vs. open research conjecture. Documents the 2 axioms discharged this session (Verified-zkEVM#138/Verified-zkEVM#139) and the FS Verified-zkEVM#116 best-progress route. Co-authored-by: Eliza <elizamakesmagic@gmail.com>
SYMBaiEX
pushed a commit
to SYMBaiEX/ArkLib
that referenced
this pull request
Jun 7, 2026
SYMBaiEX
pushed a commit
to SYMBaiEX/ArkLib
that referenced
this pull request
Jun 8, 2026
…e Hensel numerator First genuinely-provable verified brick of the BCIKS20 App-A.4 (P1) divisibility half (Verified-zkEVM#138). New file P1XiOrderExtraction.lean (imports only HenselNumerator), added to the ArkLib umbrella. - betaHensel_succ_xi_pow_extraction: for ANY irreducible H, assuming the lower-order ξ-divisibility βHensel l = a l · ξ^(2l-1) for all l ≤ k, the BCIKS20 (A.1) recursion gives βHensel (k+1) = c · ξ^(2k) constructively — pure ring algebra, NO Faà-di-Bruno cancellation. Every surviving summand carries ξ-order exactly (2·i1+Σλ-2)+(2·(k+1-i1)-Σλ) = 2k, so ξ^(2k) factors out of the whole double sum. - partitionProd_xi_factor, prod_map_pow_eq_pow_sum, sum_map_two_mul_pred: reusable ξ-order accounting helpers. Pins the open Verified-zkEVM#138 core to exactly the ONE extra ξ (Newton order-gain 2k → 2k+1 = vanishing of the leading ξ^(2k) coefficient, the cancellation) plus the weight-≤1 bound on the quotient. Axiom-clean ([propext, Classical.choice, Quot.sound]); module olean builds (2147 jobs). Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
This was referenced Jun 8, 2026
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
This PR introduces more parameters to the BN254 curve, like the base field (and more as added)
It also introduces a whitespace linter script (copied from batteries). we fixed some whitespace linting issue this way (ofc if you go to the individual files, the linter will also flag these).