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 filtersReedSolomon.relativeUniqueDecodingRadius_RS_eq
Plain-language statement
Relative unique decoding radius for RS code with arbitrary finite index type ι.
Source project: ArkLib
Person-level attribution pending.
ReedSolomon.toPolynomial_mem_lt_deg
Plain-language statement
The polynomials corresponding to Reed-Solomon codewords are of degree smaller than deg.
Source project: ArkLib
Person-level attribution pending.
ResourceProfile.instantiate_assoc
Plain-language statement
Instantiating symbolic capabilities is associative. Substituting impl₁ into a profile c, and then substituting impl₂ into the resulting profile, is the same as substituting the composite implementation fun k ↦ (impl₁ k).instantiate impl₂ into c directly.
Source project: VCVio
Person-level attribution pending.
RingSwitching.SumcheckPhase.coreInteraction_perfectCompleteness
Plain-language statement
Perfect completeness for large-field reduction (Sumcheck ++ FinalSum)
Source project: ArkLib
Person-level attribution pending.
RoundConsistency.generalised_round_consistency_completeness
Plain-language statement
Completeness of the round consistency check. Given a polynomial f, challenge γ, and n-th roots of unity ω, when f is honestly evaluated at the scaled points {ω i * s₀}, the round consistency check succeeds with the value (foldNth n f γ).eval (s₀^n). This establishes that the Lagrange interpolant through the evaluation points matches the n-wa...
Source project: ArkLib
Person-level attribution pending.
runObs_liftComp
Plain-language statement
runObs on a lifted base-spec computation: the trace is 1 (monoid identity).
Source project: VCVio
Person-level attribution pending.