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 2,569 research declarations. Search 10,000 more complete Mathlib declarations.
2569 results
Binius.BinaryBasefold.generates_quotient_point_if_is_fiber_of_y
Plain-language statement
x is in the fiber of y under qMap_total_fiber iff y is the iterated quotient of x. That is, for binary field, the fiber of y is exactly the set of all x that map to y under the iterated quotient map.
Source project: ArkLib
Person-level attribution pending.
Binius.BinaryBasefold.hammingDist_le_of_outer_comp_injective
Plain-language statement
Hamming distance is non-increasing under inner composition with an injective function. NOTE : we can prove strict equality given g being an equivalence instead of injection.
Source project: ArkLib
Person-level attribution pending.
Binius.BinaryBasefold.pointToIterateQuotientIndex_qMap_total_fiber_eq_self
Plain-language statement
the pointToIterateQuotientIndex of qMap_total_fiber
Source project: ArkLib
Person-level attribution pending.
Binius.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.