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 2 research declarations. Search 10,000 more complete Mathlib declarations.
2 results
Clear filtersArkLib.Lattices.Hachi.tensorG_coord_diff
Plain-language statement
Coordinate isolation (Hachi Lemma 8, case (C), the c5 subtract-and-divide crux): if c ≡ⱼ c', the challenge-difference sum collapses to the j-th block, tensorG (c − c') x = (cⱼ − c'ⱼ) •ᵥ (G_k *ᵥ xⱼ).
Source project: ArkLib
Person-level attribution pending.
ArkLib.Lattices.Hachi.tensorG1_coord_diff
Project documentation
Coordinate isolation at k = 1 (Hachi Lemma 8, case (C), the c4 subtract-and-divide crux): if c ≡ⱼ c', then tensorG1 (c − c') ŵ = (cⱼ − c'ⱼ) · wⱼ where w := G_blocks *ᵥ ŵ is the recomposed carrier.
Source project: ArkLib
Person-level attribution pending.