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 169 research declarations. Search 10,000 more complete Mathlib declarations.
169 results
Clear filtersQueryImpl.Stateful.simulateQ_linkWith_run
Plain-language statement
Structural form of linked simulation through an explicit state frame.
Source project: VCVio
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.
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.
seededOracle.evalDist_liftComp_generateSeed_bind_simulateQ_run'_takeAtIndex
Plain-language statement
Truncating the seed at oracle i₀ to only the first k entries does not change the distribution when averaging over seeds from generateSeed.
Source project: VCVio
Person-level attribution pending.
SignatureAlg.le_probOutput_bind_of_forall_support
Plain-language statement
If every value x in the support of gen satisfies Pr[= a | f x] ≥ 1 - δ, then the overall probability satisfies Pr[= a | gen >>= f] ≥ 1 - δ. This reduces a "for all keys" completeness statement to per-key bounds.
Source project: VCVio
Person-level attribution pending.
SignatureAlg.unforgeableAdv.advantage_le_unforgeableExpNoFresh
Plain-language statement
Phase B (freshness-drop) bound. The CMA advantage is bounded above by the success probability of the same experiment with the freshness check dropped. Both unforgeableExp and unforgeableExpNoFresh factor as runtime.evalDist (joint >>= ...) sharing the same prefix joint. The hypothesis h_pull packages the runtime-specific factoring step that...
Source project: VCVio
Person-level attribution pending.