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 5 research declarations. Search 10,000 more complete Mathlib declarations.
5 results
Clear filtersBinius.BinaryBasefold.fiberwise_dist_lt_imp_dist_lt_unique_decoding_radius
Plain-language statement
if d⁽ⁱ⁾(f⁽ⁱ⁾, C⁽ⁱ⁾) < d_{ᵢ₊steps} / 2 (fiberwise distance), then d(f⁽ⁱ⁾, C⁽ⁱ⁾) < dᵢ/2 (regular code distance)
Source project: ArkLib
Person-level attribution pending.
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.