Source-pinned research
Search theorem names, mathematical ideas, modules, topics, projects, and role-labelled researchers. Open a result for its complete indexed Lean declaration and source record.
This index contains 573 research declarations. Search 10,000 more complete Mathlib declarations.
573 results
Clear filtersBinius.BinaryBasefold.qMap_total_fiber_disjoint
Plain-language statement
The images of qMap_total_fiber over distinct quotient points y₁ ≠ y₂ are disjoint
Source project: ArkLib
Person-level attribution pending.
Binius.BinaryBasefold.toOutCodewordsCount_mul_ϑ_eq_i_succ
Plain-language statement
If a new oracle is committed at round i + 1 (i.e., ϑ ∣ i + 1), then the index of this new oracle (which is the count of oracles from the previous round, i) multiplied by ϑ equals the current round number i + 1. TODO: double check why this is still correct when replacing hCR with ϑ | i + 1
Source project: ArkLib
Person-level attribution pending.
Binius.FRIBinius.CoreInteractionPhase.coreInteractionOracleReduction_perfectCompleteness
Plain-language statement
Perfect completeness for the core interaction oracle reduction
Source project: ArkLib
Person-level attribution pending.
Binius.FRIBinius.CoreInteractionPhase.coreInteractionOracleVerifier_rbrKnowledgeSoundness
Plain-language statement
Round-by-round knowledge soundness for the core interaction oracle verifier
Source project: ArkLib
Person-level attribution pending.
BlockRelDistance.listBlock_subset_listHamming
Plain-language statement
Claim 4.19 from [ACFY24], Part 2 As a consequence of relHammingDist_le_blockRelDistance, the list of codewords within a certain block relative distance δ is a subset of the list of codewords within the same relative Hamming distance δ.
Source project: ArkLib
Person-level attribution pending.
BlockRelDistance.relHammingDist_le_blockRelDistance
Plain-language statement
Claim 4.19 from [ACFY24], Part 1 For a smooth Reed-Solomon code, the standard relative Hamming distance δᵣ(f,g) is a lower bound for the k-wise block relative distance δᵣ(k, φ, f, g).
Source project: ArkLib
Person-level attribution pending.