Proofs for IndexedBinaryTree lemmas - #140
Merged
Merged
Conversation
…b/Data/IndexedBinaryTree/Lemmas.lean] Verified-zkEVM#132 instance {s} : LawfulFunctor (fun α => InternalData α s) [ArkLib/ToMathlib/Data/IndexedBinaryTree/Lemmas.lean] Verified-zkEVM#131 instance {s} : LawfulFunctor (fun α => LeafData α s) [ArkLib/ToMathlib/Data/IndexedBinaryTree/Lemmas.lean] Verified-zkEVM#130 theorem SkeletonNodeIndex.rightChild_bind_parent [ArkLib/ToMathlib/Data/IndexedBinaryTree/Lemmas.lean] Verified-zkEVM#129 theorem SkeletonNodeIndex.leftChild_bind_parent [ArkLib/ToMathlib/Data/IndexedBinaryTree/Lemmas.lean] Verified-zkEVM#128 def FullData.Equiv [ArkLib/ToMathlib/Data/IndexedBinaryTree/Equiv.lean] Verified-zkEVM#127 def SkeletonNodeIndex.SumEquiv [ArkLib/ToMathlib/Data/IndexedBinaryTree/Equiv.lean] Verified-zkEVM#126 def FullData.EquivIndexFun [ArkLib/ToMathlib/Data/IndexedBinaryTree/Equiv.lean] Verified-zkEVM#125 def InternalData.EquivIndexFun [ArkLib/ToMathlib/Data/IndexedBinaryTree/Equiv.lean] Verified-zkEVM#124 def LeafData.EquivIndexFun [ArkLib/ToMathlib/Data/IndexedBinaryTree/Equiv.lean] Verified-zkEVM#123 def SkeletonNodeIndex.path [ArkLib/ToMathlib/Data/IndexedBinaryTree/Basic.lean] Verified-zkEVM#122
Collaborator
|
Thank you! Hoping to review these tomorrow and merge. |
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
…y-free build
Three tracked scratch files held `sorry` stubs attempting genuinely-OPEN
conjectures (not closeable by formalization):
- ArkLib/P2Scratch.lean (restrictedFaaDiBrunoMatch_proof — BCIKS20 P2 Hensel,
Verified-zkEVM#139/Verified-zkEVM#140; the residual was refuted as not-unconditionally-true)
- ArkLib/Data/CodingTheory/ProximityGap/BCIKS20/P2PartitionMatchScratch.lean
(wrongly registered in the generated ArkLib.lean)
- ArkLib/GrandChallengesScratch.lean (uniformEpsMCAgsPrizeBoundConjecture —
the open uniform prize form, Verified-zkEVM#141)
None were imported or load-bearing (zero external references); only auto-sync
had touched them since landing. They were the last 3 live holes per
scripts/sorry_census.py. The open math stays tracked on Verified-zkEVM#139/Verified-zkEVM#140/Verified-zkEVM#141; the
production tree should not carry broken scratch attempts at open conjectures.
After removal + `scripts/update-lib.sh` regen of ArkLib.lean (835 imports):
- scripts/sorry_census.py: 0 holes (was 3)
- scripts/forbidden_tokens.py: clean (10 allowlisted external-paper axioms)
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
…er is not universal — refute the unsound residual axiom
ResidualAxioms.lean carries 'axiom mcaForallDoubleCover_residual : MCAForallDoubleCover C δ' for ALL codes. But MCAForallDoubleCover.not_mcaEvent shows MCAForallDoubleCover C δ is equivalent to 'no MCA bad event ever occurs', and lineDecodable_imp_epsMCA_le_target turns it into epsMCA = 0 for every code/radius — plainly false. So the axiom is unsound (makes the library inconsistent), not honest open-problem scaffolding.
New file proves this sorry-free, axiom-clean [propext, Classical.choice, Quot.sound]: concrete_mcaEvent exhibits a realizable MCA bad event (ZMod 2, Fin 1, C={0}, delta=0); not_mcaForallDoubleCover_concrete and exists_not_mcaForallDoubleCover conclude the universal axiom asserts a false proposition and must be removed (larp per Verified-zkEVM#169/Verified-zkEVM#171). A refutation artifact like double_coverage_counterexample, not a closure of open math.
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
…Cover refutation to reuse existing witness The tree already de-larped mcaForallDoubleCover_residual (axiom -> def : Prop) and LineDecodingRefutation.lean already proves the concrete bad event (mcaEvent_ubad_zero) + epsMCA_Czero_pos. To avoid duplicating that (and the file bloat Verified-zkEVM#171 flags), reuse its witness and add only the genuinely-unique lemmas that refute the MCAForallDoubleCover PREDICATE directly: not_mcaForallDoubleCover_Czero and exists_not_mcaForallDoubleCover. These are a regression guard ensuring the residual can never be honestly re-promoted to an axiom/theorem. Axiom-clean [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
… ArkLib.lean 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
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
The black-box T4.21 (`lineDecodable_imp_epsMCA_le_target`) is false (refuted in-tree). The first repair via `MCAForallDoubleCover` is *circular*: `epsMCA_eq_zero_iff_MCAForallDoubleCover` proves that hypothesis is equivalent to the conclusion `epsMCA = 0` (two distinct scalars pin a degree-≤1 line, so the "double cover" collapses to joint agreement) — so it assumes its conclusion. New module `LineDecodingT421Faithful.lean` gives the non-circular repair `mcaBadCount_lt_of_gs_curve_cover`: exposing the genuine GS interpolation data (a single candidate codeword-pair whose line covers the bad scalars on a curve, + failure of correlated agreement — strictly weaker than `epsMCA = 0`), the *proven* BCIKS20 bound `sufficiently_large_list_agreement_on_curve_implies_correlated_agreement` yields the real list-size cap `mcaBadCount C δ u₀ u₁ < M·n + 1` (the authentic `a/|F|` shape of T4.21). Axiom-clean [propext, Classical.choice, Quot.sound]; builds (3330 jobs); forbidden-tokens clean. Registered in ArkLib.lean. 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
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 8, 2026
…= (floor(delta*n)+1)/|F|) Completes the exact characterization. Construction (slopeStack): k+1 active coords (k=floor(delta*n)) carry distinct slopes phi over the common-zero coords; each slope phi(i0) is a bad scalar (line vanishes off the active set and at i0, witness size n-k >= (1-delta)n, nondegenerate at i0). The k+1 distinct slopes (phi injective on A) give >= k+1 bad scalars, so epsMCA >= (k+1)/|F|. Needs floor(delta*n)+1 <= min(|iota|, |F|). With the upper bound this PINS epsMCA(bot,delta) exactly. Axiom-clean (no sorry), 3 build-iterations. Genuine novel construction (Verified-zkEVM#140/Verified-zkEVM#171). 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 8, 2026
epsMCA_bot_eq_floor_succ_div: epsMCA(bot over F, delta) = (floor(delta*n)+1)/|F| for delta<=1 and floor(delta*n)+1 <= min(|iota|,|F|). le_antisymm of the tight upper bound (slope-counting) and the matching slopeStack lower construction. A fully machine-checked instance of the Grand MCA Challenge format (closed-form epsMCA from which delta* is read off exactly). Axiom-clean. (Verified-zkEVM#140/Verified-zkEVM#232) 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
2 participants
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.
Provides the following definitions / proofs, along with auxiliary definitions & theorems:
instance {s} : LawfulFunctor (fun α => FullData α s) [ArkLib/ToMathlib/Data/IndexedBinaryTree/Lemmas.lean] #132
instance {s} : LawfulFunctor (fun α => InternalData α s) [ArkLib/ToMathlib/Data/IndexedBinaryTree/Lemmas.lean] #131
instance {s} : LawfulFunctor (fun α => LeafData α s) [ArkLib/ToMathlib/Data/IndexedBinaryTree/Lemmas.lean] #130
theorem SkeletonNodeIndex.rightChild_bind_parent [ArkLib/ToMathlib/Data/IndexedBinaryTree/Lemmas.lean] #129
theorem SkeletonNodeIndex.leftChild_bind_parent [ArkLib/ToMathlib/Data/IndexedBinaryTree/Lemmas.lean] #128
def FullData.Equiv [ArkLib/ToMathlib/Data/IndexedBinaryTree/Equiv.lean] #127
def SkeletonNodeIndex.SumEquiv [ArkLib/ToMathlib/Data/IndexedBinaryTree/Equiv.lean] #126
def FullData.EquivIndexFun [ArkLib/ToMathlib/Data/IndexedBinaryTree/Equiv.lean] #125
def InternalData.EquivIndexFun [ArkLib/ToMathlib/Data/IndexedBinaryTree/Equiv.lean] #124
def LeafData.EquivIndexFun [ArkLib/ToMathlib/Data/IndexedBinaryTree/Equiv.lean] #123
def SkeletonNodeIndex.path [ArkLib/ToMathlib/Data/IndexedBinaryTree/Basic.lean] #122
Note: the statements of SkeletonNodeIndex.leftChild_bind_parent and SkeletonNodeIndex.rightChild_bind_parent had to be updated to match the implementation.