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 423 research declarations. Search 10,000 more complete Mathlib declarations.
423 results
Clear filtersArkLib.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.
ArkLib.Lattices.Ajtai.InnerOuter.WeakBinding.verifiedOpening_of_verify_eq_true
Plain-language statement
Extract reusable weak-opening facts from a successful verification (over 𝓜(q, α), where Lyubashevsky–Seiler invertibility applies).
Source project: ArkLib
Person-level attribution pending.