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 filtersArkLib.Lattices.Ajtai.InnerOuter.WeakBinding.inner_commit_eq_of_flatten_eq
Plain-language statement
Equal flattened inner decompositions make verified inner messages collide.
Source project: ArkLib
Person-level attribution pending.
ArkLib.Lattices.Ajtai.InnerOuter.WeakBinding.inner_relation_of_verified
Plain-language statement
Verified weak blocks with equal flattened inner decomps give a valid inner relation.
Source project: ArkLib
Person-level attribution pending.
ArkLib.Lattices.Ajtai.InnerOuter.WeakBinding.outer_relation_of_verified
Plain-language statement
Verified weak openings with different flattened witnesses give a valid outer relation.
Source project: ArkLib
Person-level attribution pending.
ArkLib.Lattices.Ajtai.InnerOuter.WeakBinding.outputToModuleSIS_valid
Plain-language statement
A successful pair of weak openings yields a valid inner or outer Module-SIS witness (over 𝓜(q, α)). The boolean-verification wrapper around outputToModuleSIS_valid_of_verified: it extracts the VerifiedOpening facts from verify_weak and applies the core.
Source project: ArkLib
Person-level attribution pending.
ArkLib.Lattices.Ajtai.InnerOuter.WeakBinding.outputToModuleSIS_valid_of_verified
Plain-language statement
Extractor validity (the reusable core). Two verified weak openings that differ yield a valid inner or outer Module-SIS witness (over 𝓜(q, α)). This is stated directly on the extracted VerifiedOpening facts, independent of how those facts were obtained , so it is reused both by the weak-binding bound below (where the VerifiedOpenings come fr...
Source project: ArkLib
Person-level attribution pending.
ArkLib.Lattices.Ajtai.InnerOuter.WeakBinding.sample_advantage_le_moduleSIS
Plain-language statement
Pointwise weak-binding to Module-SIS bound for fixed samples (over 𝓜(q, α)).
Source project: ArkLib
Person-level attribution pending.