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 423 research declarations. Search 10,000 more complete Mathlib declarations.
423 results
Clear filtersBinius.BinaryBasefold.CoreInteraction.commitOracleVerifier_rbrKnowledgeSoundness
Plain-language statement
RBR knowledge soundness for a single round oracle verifier
Source project: ArkLib
Person-level attribution pending.
Binius.BinaryBasefold.CoreInteraction.coreInteractionOracleReduction_perfectCompleteness
Plain-language statement
Perfect completeness for the core interaction oracle reduction
Source project: ArkLib
Person-level attribution pending.
Binius.BinaryBasefold.CoreInteraction.coreInteractionOracleVerifier_rbrKnowledgeSoundness
Plain-language statement
Round-by-round knowledge soundness for the core interaction oracle verifier
Source project: ArkLib
Person-level attribution pending.
Binius.BinaryBasefold.CoreInteraction.finalSumcheckOracleVerifier_rbrKnowledgeSoundness
Plain-language statement
Round-by-round knowledge soundness for the final sumcheck step
Source project: ArkLib
Person-level attribution pending.
Binius.BinaryBasefold.CoreInteraction.foldCommitOracleVerifier_rbrKnowledgeSoundness
Plain-language statement
RBR KS for Fold+Commitment block by append composition.
Source project: ArkLib
Person-level attribution pending.
Binius.BinaryBasefold.CoreInteraction.foldRelayOracleVerifier_rbrKnowledgeSoundness
Plain-language statement
RBR Knowledge Soundness of the non-commitment round verifier via append composition of fold-round and transfer-round RBR KS.
Source project: ArkLib
Person-level attribution pending.