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 12 research declarations. Search 10,000 more complete Mathlib declarations.
12 results
Clear filtersProtocolSpec.ChallengeTree.RightProj.tree_isStructured
Plain-language statement
If the appended source tree of a RightProj is structured then so is its right-protocol tree.
Source project: ArkLib
Person-level attribution pending.
ProtocolSpec.ChallengeTree.SplitData.fst_isStructured
Plain-language statement
If the appended source tree of a SplitData is structured then so is its first-stage tree.
Source project: ArkLib
Person-level attribution pending.
ProtocolSpec.ChallengeTree.SplitData.sndAt_isStructured
Plain-language statement
The suffix tree selected by any first-stage path of a structured SplitData is structured.
Source project: ArkLib
Person-level attribution pending.
Verifier.append_coordinateWiseSpecialSound
Plain-language statement
Coordinate-wise special soundness is preserved by binary verifier append. The deterministic first-verifier output identifies the input statement of each suffix tree consumed by the second verifier's extractor.
Source project: ArkLib
Person-level attribution pending.
Verifier.append_treeSpecialSound
Plain-language statement
Generic preservation of tree-special soundness under binary verifier append.
Source project: ArkLib
Person-level attribution pending.
Verifier.pure_accepting_of_mem
Plain-language statement
A deterministic verifier output that lies in a language is accepted with probability one.
Source project: ArkLib
Person-level attribution pending.