Batched FRI soundness#273

Draft

Julek wants to merge 225 commits intomainfrom

Ferinko/ElijahVlasov/fri-soundness

Commits on Jun 16, 2025

small improvement to statement of h_le_1 assumption of Polishchuk_Spielman lemma
Julek
committed
Update ArkLib/Data/CodingTheory/BivariatePoly.lean

quangvdao
and
BoltonBailey
authored

Commits on Jun 24, 2025

WIP
Julek
committed
degreeX_mul done
Julek
committed

Commits on Jul 4, 2025

Commits on Jul 8, 2025

Add proximity gap paper guruswami-sudan
ElijahVlasov
committed

Commits on Jul 9, 2025

Add non-zero condition into GS
ElijahVlasov
committed

Commits on Jul 11, 2025

Lemma 5.4
ElijahVlasov
committed

Commits on Jul 15, 2025

split filest

katyhr
authored and
Julek
committed
PS lemma second draft

katyhr
authored and
Julek
committed
some changes

katyhr
authored and
Julek
committed
edited dependency

katyhr
authored and
Julek
committed
new degreeX def

katyhr
authored and
Julek
committed
building the lemmas database

katyhr
authored and
Julek
committed
division condition fixed, moved defs, some cleanup

katyhr
authored and
Julek
committed
major cleanup and reorg, still some sorries left

katyhr
authored and
Julek
committed
Removed some unneeded assumptions, fixed definitions with missing arguments, did a bit of linting, and fixing breaks due to rename of evalX and evalY
Julek
committed
simplified proof of quotient_nezero
Julek
committed
Filled in sorrys in monomial_xy definition
Julek
committed
Added monomial_xy_def, a simple equality that acts as an effective definition, allowing lemmas from Mathlib about monomial to be leveraged, completed proof of monomial_xy_degree and added missing n…
Julek
committed
Rebased FRI implementation

ElijahVlasov
authored and
Julek
committed
Fixes to the FRI implementation
Julek
committed
Rebased FRI implementation

ElijahVlasov
authored and
Julek
committed
Fixed imports
Julek
committed
quick type fix
Julek
committed

Commits on Jul 16, 2025

WIP
ElijahVlasov
committed

Commits on Jul 21, 2025

WIp
ElijahVlasov
committed

Commits on Jul 24, 2025

Lemma 5.7
ElijahVlasov
committed

Commits on Jul 27, 2025

Commits on Jul 28, 2025

Commits on Jul 29, 2025

Theorem 6.1
ElijahVlasov
committed
Bivariate.lean
Ferinko
committed
Theorem 6.2
ElijahVlasov
committed
EvenAndOdd.lean - remove _def, use .eq_def
Ferinko
committed
Impl.lean - simplify query
Ferinko
committed
Domain.lean - ascencion
Ferinko
committed
Domain.lean
Ferinko
committed
refactor Q to Q>=0, fix proofs

Ferinko
authored and
Julek
committed
relHamming dist proofs

katyhr
authored and
Julek
committed
minor cleanup

Ferinko
authored and
Julek
committed
more cleanups

katyhr
authored and
Julek
committed
final minor cleanups

katyhr
authored and
Julek
committed
ProximityGaps draft1

katyhr
authored and
Julek
committed
some stuff

katyhr
authored and
Julek
committed
proximity wip

katyhr
authored and
Julek
committed
line 257

katyhr
authored and
Julek
committed
WIP - thing3 + nonempty explicitly given

Ferinko
authored and
Julek
committed
fix decidable equality

Ferinko
authored and
Julek
committed
def generalProximityGap

katyhr
authored and
Julek
committed
fix generalProximityGap

Ferinko
authored and
Julek
committed
or something like this

Ferinko
authored and
Julek
committed
latest WIP

katyhr
authored and
Julek
committed
proximityGaps results

katyhr
authored and
Julek
committed

Commits on Jul 30, 2025

Commits on Jul 31, 2025

Merge pull request #30 from NethermindEth/Ferinko/Katy/ProximityWIP
katyhr
authored

Commits on Aug 4, 2025

Commits on Aug 5, 2025

Lemma 6.3
ElijahVlasov
committed

Commits on Aug 11, 2025

Commits on Aug 12, 2025

Commits on Aug 13, 2025

Commits on Aug 20, 2025

more weighted degrees, remove redundant variables
katyhr
committed

Commits on Aug 26, 2025

weighted degree and monomial degree lemmas and proofs
katyhr
committed

Commits on Aug 29, 2025

Commits on Sep 4, 2025

WIP - Hmonic
Ferinko
committed

Commits on Sep 15, 2025

Sketch of L function field and its ring of integers
Julek
committed

Commits on Sep 16, 2025

Preliminary lemmas and defs for polynomials
katyhr
committed
added Polynomial prelims
katyhr
committed
initial cleanup after new defs
katyhr
committed
`UniPoly` equivalence relation and quotient operations (#106)

dhsorens
authored and
katyhr
committed
feat: Inductive Merkle Trees with completeness theorem (#44)

BoltonBailey
authored and
katyhr
committed
Blueprint for Guruswami-Sudan (#81)

authored and
katyhr
committed
[DRAFT] Fix: WHIR/STIR (#85)

alexanderlhicks
authored and
katyhr
committed
Add comprehensive dependency analysis toolkit (#133)

quangvdao
authored and
katyhr
committed
feat: rename `oracle` => `answer` in OracleInterface (#134)

quangvdao
authored and
katyhr
committed
feat: reorganize workflows (#135)

quangvdao
authored and
katyhr
committed
feat: change lakefile.lean to lakefile.toml (#136)

quangvdao
authored and
katyhr
committed
chore: Renaming of oracle interface instances (#139)

quangvdao
authored and
katyhr
committed
lemma decoded_polynomial_lt_deg [ArkLib/Data/CodingTheory/ReedSolomon.lean] #121

winger
authored and
katyhr
committed
theorem singleton_bound_linear [ArkLib/Data/CodingTheory/Basic.lean] #110

winger
authored and
katyhr
committed
theorem dist'_eq_dist [ArkLib/Data/CodingTheory/Basic.lean] #107

winger
authored and
katyhr
committed
Add missing lemma

winger
authored and
katyhr
committed
instance {s} : LawfulFunctor (fun α => FullData α s) [ArkLib/ToMathlib/Data/IndexedBinaryTree/Lemmas.lean] #132

winger
authored and
katyhr
committed
Revert theorem def to original

winger
authored and
katyhr
committed
feat: Define BN254 curve (#138)

quangvdao
authored and
katyhr
committed
define KoalaBear field, change name of `fieldSize`

quangvdao
authored and
katyhr
committed
feat: define Koala Bear field & Poseidon2 spec (#204)

quangvdao
authored and
katyhr
committed
feat: add PR summary workflow

alexanderlhicks
authored and
katyhr
committed
accidently pointed to old model

alexanderlhicks
authored and
katyhr
committed
fix: correct diff command in pr-summary workflow

alexanderlhicks
authored and
katyhr
committed
fix: use single quotes in pr-summary workflow

alexanderlhicks
authored and
katyhr
committed
fix: use diff_url in pr-summary workflow

alexanderlhicks
authored and
katyhr
committed
feat: adopt mathlib4 diff strategy for pr-summary

alexanderlhicks
authored and
katyhr
committed
fix: pass diff as env var in pr-summary workflow

alexanderlhicks
authored and
katyhr
committed
revert: use pull_request trigger

alexanderlhicks
authored and
katyhr
committed
rebase
katyhr
committed

Commits on Sep 18, 2025

Commits on Sep 19, 2025

Commits on Sep 22, 2025

draft of everything but claim A_2
katyhr
committed

Commits on Sep 26, 2025

Defined Hensel lemma coefficients
Julek
committed

Commits on Sep 30, 2025

latest wip
katyhr
committed
Appendix A done?
Julek
committed

Commits on Oct 1, 2025

Commits on Oct 2, 2025

Commits on Oct 3, 2025

Commits on Oct 9, 2025

Some comments
ElijahVlasov
committed

Commits on Oct 10, 2025

Commits on Oct 13, 2025

Commits on Oct 17, 2025

Commits on Oct 28, 2025

Section 6 of Proximity Gaps

ElijahVlasov
authored and
Julek
committed
Section 7

ElijahVlasov
authored and
Julek
committed

Commits on Oct 29, 2025

Commits on Oct 30, 2025

Commits on Oct 31, 2025

Commits on Nov 1, 2025

Fixed typeclass issue
Julek
committed

Commits on Nov 5, 2025

WIP
ElijahVlasov
committed
Renaming
ElijahVlasov
committed

Commits on Nov 6, 2025

Commits on Nov 7, 2025

Commits on Nov 15, 2025

Fix to mu_set + better docstrings for 6.3, 7.5 and 7.6
Julek
committed
Added Fintype proof for coeffs_of_close_proximity_curve
Julek
committed
WIP

ElijahVlasov
authored and
Julek
committed
Claim 8.1

ElijahVlasov
authored and
Julek
committed
WIP

ElijahVlasov
authored and
Julek
committed
WIP

ElijahVlasov
authored and
Julek
committed
WIP

ElijahVlasov
authored and
Julek
committed
WIP
Julek
committed
WIP
Julek
committed
WIP
Julek
committed
8.2 done?
Julek
committed
Initial 8.1 cleanup
Julek
committed
fix of 8.1 to use CosetDomain instead of Domain
Julek
committed
A bit more cleanup of 8.2
Julek
committed
8.1 WIP
Julek
committed

Commits on Nov 17, 2025

Commits on Nov 18, 2025

cleanup Soundness, SingleRound and Basic
Ferinko
committed

Commits on Nov 19, 2025

Commits on Nov 20, 2025

cleanup the instance issues, document what's happening
Ferinko
committed

Commits on Nov 21, 2025

Commits on Dec 4, 2025

WIP
Julek
committed