Skip to content

Commit 25f060e

Browse files
lalalunelalalune
committed
feat(Verified-zkEVM#140): expose repaired adjacent frontier specs
1 parent 2b9b7d3 commit 25f060e

1 file changed

Lines changed: 149 additions & 0 deletions

File tree

‎ArkLib/Data/CodingTheory/ProximityGap/LineDecodingGrandChallengesPrizeSpec.lean‎

Lines changed: 149 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -345,6 +345,147 @@ theorem mcaPrizeLatticeResolved_of_forall_not_mcaEventAdjacentFrontier
345345
(mcaPrizeAdjacentWitnessFrontier_of_forall_not_mcaEvent_and_upperWitnesses
346346
domain δ hδ_le_one hno whi hδhi hadj)
347347

348+
/-- Repaired double-cover adjacent frontiers resolve the four-rate MCA prize through the generic
349+
adjacent-frontier API and expose the satisfy/maximality specification for those concrete
350+
thresholds. -/
351+
theorem mcaPrizeLatticeResolved_with_spec_ofDoubleCoverAdjacentFrontier
352+
(domain : ι ↪ F) (δ : Fin 4 → ℝ≥0)
353+
(hδ_le_one : ∀ j : Fin 4, δ j ≤ 1)
354+
(hcov : ∀ j : Fin 4, MCAForallDoubleCover (F := F) (A := F)
355+
(ReedSolomon.code domain ⌊prizeRates j * (Fintype.card ι : ℝ≥0)⌋₊ : Set (ι → F))
356+
(δ j))
357+
(whi : ∀ j : Fin 4,
358+
GrandChallenges.MCAUpperWitness
359+
(ReedSolomon.code domain
360+
⌊prizeRates j * (Fintype.card ι : ℝ≥0)⌋₊ : Set (ι → F))
361+
epsStar)
362+
(hδhi : ∀ j : Fin 4, (whi j).δ ≤ 1)
363+
(hadj : ∀ j : Fin 4,
364+
(latticeIndexOf (ι := ι) (whi j).δ (hδhi j)).val =
365+
(latticeIndexOf (ι := ι) (δ j) (hδ_le_one j)).val + 1) :
366+
let τ : Fin 4 → Fin (Fintype.card ι + 1) :=
367+
fun j => latticeIndexOf (ι := ι) (δ j) (hδ_le_one j)
368+
mcaPrizeLatticeResolved domain τ ∧
369+
∀ j : Fin 4,
370+
let C : Set (ι → F) :=
371+
ReedSolomon.code domain ⌊prizeRates j * (Fintype.card ι : ℝ≥0)⌋₊
372+
∃ _ : mcaThresholdExists C epsStar,
373+
mcaSatisfies C epsStar (τ j) ∧
374+
∀ i : Fin (Fintype.card ι + 1), mcaSatisfies C epsStar i → i ≤ τ j := by
375+
let τ : Fin 4 → Fin (Fintype.card ι + 1) :=
376+
fun j => latticeIndexOf (ι := ι) (δ j) (hδ_le_one j)
377+
have hτ : mcaPrizeLatticeResolved domain τ :=
378+
mcaPrizeLatticeResolved_ofDoubleCoverAdjacentFrontier
379+
domain δ hδ_le_one hcov whi hδhi hadj
380+
exact ⟨hτ, (mcaPrizeLatticeResolved_iff domain τ).mp hτ⟩
381+
382+
/-- Named bad-scalar double-cover adjacent frontiers resolve the four-rate MCA prize through the
383+
generic adjacent-frontier API and expose the satisfy/maximality specification for those concrete
384+
thresholds. -/
385+
theorem mcaPrizeLatticeResolved_with_spec_ofBadScalarDoubleCoverAdjacentFrontier
386+
(domain : ι ↪ F) (δ : Fin 4 → ℝ≥0)
387+
(hδ_le_one : ∀ j : Fin 4, δ j ≤ 1)
388+
(hcov : ∀ j : Fin 4, ∀ (u : Code.WordStack F (Fin 2) ι) (γ : F),
389+
MCABadScalarDoubleCover (F := F) (A := F)
390+
(ReedSolomon.code domain ⌊prizeRates j * (Fintype.card ι : ℝ≥0)⌋₊ : Set (ι → F))
391+
(δ j) (u 0) (u 1) γ)
392+
(whi : ∀ j : Fin 4,
393+
GrandChallenges.MCAUpperWitness
394+
(ReedSolomon.code domain
395+
⌊prizeRates j * (Fintype.card ι : ℝ≥0)⌋₊ : Set (ι → F))
396+
epsStar)
397+
(hδhi : ∀ j : Fin 4, (whi j).δ ≤ 1)
398+
(hadj : ∀ j : Fin 4,
399+
(latticeIndexOf (ι := ι) (whi j).δ (hδhi j)).val =
400+
(latticeIndexOf (ι := ι) (δ j) (hδ_le_one j)).val + 1) :
401+
let τ : Fin 4 → Fin (Fintype.card ι + 1) :=
402+
fun j => latticeIndexOf (ι := ι) (δ j) (hδ_le_one j)
403+
mcaPrizeLatticeResolved domain τ ∧
404+
∀ j : Fin 4,
405+
let C : Set (ι → F) :=
406+
ReedSolomon.code domain ⌊prizeRates j * (Fintype.card ι : ℝ≥0)⌋₊
407+
∃ _ : mcaThresholdExists C epsStar,
408+
mcaSatisfies C epsStar (τ j) ∧
409+
∀ i : Fin (Fintype.card ι + 1), mcaSatisfies C epsStar i → i ≤ τ j := by
410+
let τ : Fin 4 → Fin (Fintype.card ι + 1) :=
411+
fun j => latticeIndexOf (ι := ι) (δ j) (hδ_le_one j)
412+
have hτ : mcaPrizeLatticeResolved domain τ :=
413+
mcaPrizeLatticeResolved_ofBadScalarDoubleCoverAdjacentFrontier
414+
domain δ hδ_le_one hcov whi hδhi hadj
415+
exact ⟨hτ, (mcaPrizeLatticeResolved_iff domain τ).mp hτ⟩
416+
417+
/-- Zero bad-scalar count adjacent frontiers resolve the four-rate MCA prize through the generic
418+
adjacent-frontier API and expose the satisfy/maximality specification for those concrete
419+
thresholds. -/
420+
theorem mcaPrizeLatticeResolved_with_spec_of_mcaBadCount_zeroAdjacentFrontier
421+
(domain : ι ↪ F) (δ : Fin 4 → ℝ≥0)
422+
(hδ_le_one : ∀ j : Fin 4, δ j ≤ 1)
423+
(hzero : ∀ j : Fin 4, ∀ u : Code.WordStack F (Fin 2) ι,
424+
mcaBadCount (F := F)
425+
(ReedSolomon.code domain
426+
⌊prizeRates j * (Fintype.card ι : ℝ≥0)⌋₊ : Set (ι → F))
427+
(δ j) (u 0) (u 1) = 0)
428+
(whi : ∀ j : Fin 4,
429+
GrandChallenges.MCAUpperWitness
430+
(ReedSolomon.code domain
431+
⌊prizeRates j * (Fintype.card ι : ℝ≥0)⌋₊ : Set (ι → F))
432+
epsStar)
433+
(hδhi : ∀ j : Fin 4, (whi j).δ ≤ 1)
434+
(hadj : ∀ j : Fin 4,
435+
(latticeIndexOf (ι := ι) (whi j).δ (hδhi j)).val =
436+
(latticeIndexOf (ι := ι) (δ j) (hδ_le_one j)).val + 1) :
437+
let τ : Fin 4 → Fin (Fintype.card ι + 1) :=
438+
fun j => latticeIndexOf (ι := ι) (δ j) (hδ_le_one j)
439+
mcaPrizeLatticeResolved domain τ ∧
440+
∀ j : Fin 4,
441+
let C : Set (ι → F) :=
442+
ReedSolomon.code domain ⌊prizeRates j * (Fintype.card ι : ℝ≥0)⌋₊
443+
∃ _ : mcaThresholdExists C epsStar,
444+
mcaSatisfies C epsStar (τ j) ∧
445+
∀ i : Fin (Fintype.card ι + 1), mcaSatisfies C epsStar i → i ≤ τ j := by
446+
let τ : Fin 4 → Fin (Fintype.card ι + 1) :=
447+
fun j => latticeIndexOf (ι := ι) (δ j) (hδ_le_one j)
448+
have hτ : mcaPrizeLatticeResolved domain τ :=
449+
mcaPrizeLatticeResolved_of_mcaBadCount_zeroAdjacentFrontier
450+
domain δ hδ_le_one hzero whi hδhi hadj
451+
exact ⟨hτ, (mcaPrizeLatticeResolved_iff domain τ).mp hτ⟩
452+
453+
/-- Direct no-bad-event adjacent frontiers resolve the four-rate MCA prize through the generic
454+
adjacent-frontier API and expose the satisfy/maximality specification for those concrete
455+
thresholds. -/
456+
theorem mcaPrizeLatticeResolved_with_spec_of_forall_not_mcaEventAdjacentFrontier
457+
(domain : ι ↪ F) (δ : Fin 4 → ℝ≥0)
458+
(hδ_le_one : ∀ j : Fin 4, δ j ≤ 1)
459+
(hno : ∀ j : Fin 4, ∀ (u : Code.WordStack F (Fin 2) ι) (γ : F),
460+
¬ mcaEvent (F := F)
461+
(ReedSolomon.code domain
462+
⌊prizeRates j * (Fintype.card ι : ℝ≥0)⌋₊ : Set (ι → F))
463+
(δ j) (u 0) (u 1) γ)
464+
(whi : ∀ j : Fin 4,
465+
GrandChallenges.MCAUpperWitness
466+
(ReedSolomon.code domain
467+
⌊prizeRates j * (Fintype.card ι : ℝ≥0)⌋₊ : Set (ι → F))
468+
epsStar)
469+
(hδhi : ∀ j : Fin 4, (whi j).δ ≤ 1)
470+
(hadj : ∀ j : Fin 4,
471+
(latticeIndexOf (ι := ι) (whi j).δ (hδhi j)).val =
472+
(latticeIndexOf (ι := ι) (δ j) (hδ_le_one j)).val + 1) :
473+
let τ : Fin 4 → Fin (Fintype.card ι + 1) :=
474+
fun j => latticeIndexOf (ι := ι) (δ j) (hδ_le_one j)
475+
mcaPrizeLatticeResolved domain τ ∧
476+
∀ j : Fin 4,
477+
let C : Set (ι → F) :=
478+
ReedSolomon.code domain ⌊prizeRates j * (Fintype.card ι : ℝ≥0)⌋₊
479+
∃ _ : mcaThresholdExists C epsStar,
480+
mcaSatisfies C epsStar (τ j) ∧
481+
∀ i : Fin (Fintype.card ι + 1), mcaSatisfies C epsStar i → i ≤ τ j := by
482+
let τ : Fin 4 → Fin (Fintype.card ι + 1) :=
483+
fun j => latticeIndexOf (ι := ι) (δ j) (hδ_le_one j)
484+
have hτ : mcaPrizeLatticeResolved domain τ :=
485+
mcaPrizeLatticeResolved_of_forall_not_mcaEventAdjacentFrontier
486+
domain δ hδ_le_one hno whi hδhi hadj
487+
exact ⟨hτ, (mcaPrizeLatticeResolved_iff domain τ).mp hτ⟩
488+
348489
/-- Adjacent repaired double-cover frontiers resolve the four-rate MCA prize at the repaired
349490
lower-frontier lattice indices and expose the satisfy/maximality specification for those concrete
350491
thresholds. -/
@@ -627,6 +768,14 @@ set_option linter.style.longLine false in
627768
set_option linter.style.longLine false in
628769
#print axioms ProximityGap.GrandChallengesLattice.mcaPrizeLatticeResolved_of_forall_not_mcaEventAdjacentFrontier
629770
set_option linter.style.longLine false in
771+
#print axioms ProximityGap.GrandChallengesLattice.mcaPrizeLatticeResolved_with_spec_ofDoubleCoverAdjacentFrontier
772+
set_option linter.style.longLine false in
773+
#print axioms ProximityGap.GrandChallengesLattice.mcaPrizeLatticeResolved_with_spec_ofBadScalarDoubleCoverAdjacentFrontier
774+
set_option linter.style.longLine false in
775+
#print axioms ProximityGap.GrandChallengesLattice.mcaPrizeLatticeResolved_with_spec_of_mcaBadCount_zeroAdjacentFrontier
776+
set_option linter.style.longLine false in
777+
#print axioms ProximityGap.GrandChallengesLattice.mcaPrizeLatticeResolved_with_spec_of_forall_not_mcaEventAdjacentFrontier
778+
set_option linter.style.longLine false in
630779
#print axioms ProximityGap.GrandChallengesLattice.mcaPrizeLatticeResolved_with_spec_ofDoubleCover_and_adjacent_upperWitnesses
631780
set_option linter.style.longLine false in
632781
#print axioms ProximityGap.GrandChallengesLattice.mcaPrizeLatticeResolved_with_spec_ofBadScalarDoubleCover_and_adjacent_upperWitnesses

0 commit comments

Comments
 (0)