therefore
Sign up
Open navigation

Source-pinned research

Research proof index

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 2 research declarations. Search 10,000 more complete Mathlib declarations.

1 topic

2 results

Clear filters
Project-declaredLean 4.31.0

Oracle Verifier coordinate Wise Special Sound

SendClaim.oracleVerifier_coordinateWiseSpecialSound

Project documentation

Coordinate-wise special soundness of SendClaim. The verifier is a pure pass-through with no challenge rounds, so CWSS collapses (via the oracle no-challenge bridge) to a transcript-level obligation. The extractor is trivial (e := fun _ _ => (), there is no witness); since the output oracle statements at inl are the input oracles unchanged and `t...

cryptographyproof systemscoding theory

Source project: ArkLib

Person-level attribution pending.

View proof record
Project-declaredLean 4.31.0

Oracle Verifier to Verifier run

SendClaim.oracleVerifier_toVerifier_run

Plain-language statement

The pure pass-through oracle verifier's underlying non-oracle verifier returns the statement together with the output oracle statements (input oracles at inl, the message at inr 0).

cryptographyproof systemscoding theory

Source project: ArkLib

Person-level attribution pending.

View proof record