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 filtersProtocolSpec.ChallengeTree.leftPrefix_concat
Plain-language statement
leftPrefix commutes with extending the prefix by one round.
Source project: ArkLib
Person-level attribution pending.
ProtocolSpec.ChallengeTree.rightPrefix_concat
Plain-language statement
rightPrefix commutes with extending the right prefix by one round. The rightPrefix/Fin.snoc dites are split by split_ifs; contradictory combinations close by omega (with idx's bound), matching ones by cast_eq_cast_of_heq (stripping casts to a base HEq, then rfl/index omega).
Source project: ArkLib
Person-level attribution pending.
ProtocolSpec.ChallengeTree.rightPrefix_leaf_eq_append
Plain-language statement
At the right boundary (pre₂ is a full right transcript) the embedding is literally tr₁ ++ₜ.
Source project: ArkLib
Person-level attribution pending.
ProtocolSpec.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.