Introduce pullback argument for STIR and WHIR theorems

[ElijahVlasov]

Claim 4.23 from [ACFY24] and lemma 4.9 from [ACFY24stir] share a similar combinatorial proof technique which we call "pullback argument" since the combinatorics is done via a set that is called a pullback in category theory.

In this PR we introduce various stuff simplifying the pullback argument and rewrite parts of the proof of lemma 4.9 to use the introduced infra. The upcoming PR with claim 4.23 is going to rely on that as well.

[github-actions]

🤖 PR Summary

⚠️ PR title does not follow conventional commit format type[(scope)]: subject. Got: Introduce pullback argument for STIR and WHIR theorems

Mathematical Formalization

Pullback Argument (new API)

• ArkLib/Data/Domain/CosetFftDomain/Pullback.lean (new file) introduces the core combinatorial set and its projections:
  • Pullback.pullback s t – the set of pairs (x, y) ∈ s × t such that x and y coincide on the intersection of the two subdomains (defined via subdomain).
  • Pullback.pullback₁, Pullback.pullback₂ – projections to the first and second component.
  • Key cardinality results:
    • card_pullback_eq_card_pullback₁, card_pullback₂_eq (when s ⊆ subdomain ω r).
    • pullback₁_eq_biUnion_pullback₂ – decomposition into blocks indexed by the second projection.
    • card_pullback_eq_mul_card_pullback₂ – the counting formula #pullback = 2^(r - l) * #pullback₂ (where l, r are the subdomain levels).
  • Membership lemmas (mem_pullback₁_iff_mem_pullback₂ and variants for l = 0, 1) linking the two projections.

Refactoring of STIR / WHIR Lemmas

• ArkLib/Data/CodingTheory/ProximityGap/Folding.lean rewrites parts of the proof of Lemma 4.9 from [ACFY24stir] using the new pullback API:
  • Definitions hammingDistComplementBound, hammingDistBound now use Pullback.pullback domain 0 k s instead of an explicit Finset.filter over a product.
  • correlated_agreement_implies_contradictory_hamm_dist uses Pullback.card_pullback_eq_card_pullback₁ and a Finset.card_le_card call, replacing a previous Finset.card_le_card_of_injOn argument.
  • The proof of contradictory_hamm_dist_formula is simplified via two new lemmas Pullback.card_pullback_eq_mul_card_pullback₂ and Pullback.card_pullback₂_eq.
  • The typeclass assumption on F in dist_from_code_bound_of_correlated_agreement is weakened from Fintype F to Finite F (with a have instance to recover Fintype), and the set_option linter.unusedFintypeInType is removed.
  • A new import ArkLib.Data.Domain.CosetFftDomain.Pullback is added.

Subdomain Foundation

• ArkLib/Data/Domain/CosetFftDomain/Subdomain.lean adds lemma subdomain_0_apply (marked @[simp]): for the 0-th subdomain, subdomain ω 0 i = ω i. This formalizes the identity that the base subdomain coincides with the original ω sequence, a foundational property used in the pullback argument.

Library Integration

• ArkLib.lean now imports ArkLib.Data.Domain.CosetFftDomain.Pullback, making the pullback definitions available globally.

Overall Structure

The core of the PR is the new file Pullback.lean providing the pullback combinatorics, and the refactoring in Folding.lean that applies it to the STIR/WHIR lemma. The remaining changes (ArkLib.lean, Subdomain.lean) are supporting infrastructure. The PR does not introduce any new sorry or admit placeholders; proof completions appear to be fully realized.

---

Statistics

Metric	Count
📝 Files Changed	4
✅ Lines Added	283
❌ Lines Removed	79

---

Lean Declarations

✏️ Added: 19 declaration(s)

ArkLib/Data/Domain/CosetFftDomain/Pullback.lean (18)

• def pullback (ω : D) (l r : ℕ) (s : Finset F) : Finset (Fin (2 ^ (n - l)) × Fin (2 ^ (n - r)))
• def pullback₁ (ω : D) (l r : ℕ) (s : Finset F) : Finset (Fin (2 ^ (n - l)))
• def pullback₂ (ω : D) (l r : ℕ) (s : Finset F) : Finset (Fin (2 ^ (n - r)))
• lemma card_pullback_eq_card_pullback₁ :
• lemma card_pullback_eq_mul_card_pullback₂ (hl : l ≤ r) (hr : r ≤ n) :
• lemma card_pullback₂_eq (hl : l ≤ r) (hr : r ≤ n) (hs : s ⊆ (subdomain ω r).toFinset) :
• lemma mem_pullback {i : Fin (2 ^ (n - l)) × Fin (2 ^ (n - r))} :
• lemma mem_pullback₁ {i : Fin (2 ^ (n - l))} (hl : l ≤ r) (hr : r ≤ n) :
• lemma mem_pullback₁_iff_mem_pullback₂ {i : Fin (2 ^ n)} (hl : l ≤ r) (hr : r ≤ n) :
• lemma mem_pullback₁_iff_mem_pullback₂_l_0 {i : Fin (2 ^ n)} (hr : r ≤ n) :
• lemma mem_pullback₁_iff_mem_pullback₂_l_1 {i : Fin (2 ^ n)} (h1r : 1 ≤ r) (hr : r ≤ n) :
• lemma mem_pullback₂ {i : Fin (2 ^ (n - r))} (hl : l ≤ r) (hr : r ≤ n) :
• lemma mem_s_of_mem_pullback₁ {i : Fin (2 ^ (n - l))} (h : i ∈ pullback₁ ω l r s) :
• lemma proj₁_injOn :
• lemma proj₁_mapsTo :
• lemma proj₁_surjOn :
• lemma pullback_empty : pullback ω l r ∅ = ∅
• lemma pullback₁_eq_biUnion_pullback₂ (hl : l ≤ r) (hr : r ≤ n) :

ArkLib/Data/Domain/CosetFftDomain/Subdomain.lean (1)

• lemma subdomain_0_apply (i : Fin (2 ^ n)) :

---

sorry Tracking

• No sorrys were added, removed, or affected.

---

📄 **Per-File Summaries**

• ArkLib.lean: ArkLib.lean now imports ArkLib.Data.Domain.CosetFftDomain.Pullback, making the definitions from that module available throughout the library. This adds support for pullback operations on coset FFT domains, which are likely used to relate computations across different domain sizes or structures.
• ArkLib/Data/CodingTheory/ProximityGap/Folding.lean: In Folding.lean, the proof of contradictory_hamm_dist_formula was replaced with a simpler argument that uses two new lemmas, Pullback.card_pullback_eq_mul_card_pullback₂ and Pullback.card_pullback₂_eq, after the definitions hammingDistComplementBound and hammingDistBound were refactored to use Pullback.pullback domain 0 k s instead of an explicit Finset.filter over a product. The lemma correlated_agreement_implies_contradictory_hamm_dist was similarly refactored to use Pullback.card_pullback_eq_card_pullback₁ and a Finset.card_le_card call, replacing a previous Finset.card_le_card_of_injOn argument. The typeclass assumption on F in dist_from_code_bound_of_correlated_agreement was weakened from Fintype F to Finite F (with a corresponding have instance to recover Fintype), and the set_option linter.unusedFintypeInType was removed. A new import ArkLib.Data.Domain.CosetFftDomain.Pullback was added.
• ArkLib/Data/Domain/CosetFftDomain/Pullback.lean: This new file defines the pullback set for two subdomains and its projections pullback₁ and pullback₂, and proves cardinality relations: card_pullback_eq_card_pullback₁, card_pullback₂_eq (when s ⊆ subdomain ω r), pullback₁_eq_biUnion_pullback₂ (decomposing pullback₁ as a union of blocks indexed by pullback₂), and the key formula card_pullback_eq_mul_card_pullback₂ giving #pullback = 2^(r-l) * #pullback₂. Membership lemmas mem_pullback₁_iff_mem_pullback₂ and variants for l=0,1 connect the projected images. These results formalize the pullback argument referenced in Claim 4.23 of [ACFY24] and Lemma 4.9 of [ACFY24stir].
• ArkLib/Data/Domain/CosetFftDomain/Subdomain.lean: Adds subdomain_0_apply lemma: For the 0-th subdomain (index i : Fin (2 ^ n)), subdomain ω 0 i = ω i. The lemma is marked @[simp] and proven via aesop with custom safe, unsafe, and simp rules referencing subdomain, CosetFftDomainClass.subdomain_embed, mkSubgroupUnit, and CosetFftDomain.eval_coset_fft_domain_eq_eval_generator_mul_domain. This formalizes the identity that the base subdomain coincides with the original ω sequence, a foundational property for the subdomain tower used in FFT proofs.

---

Last updated: 2026-07-24 16:29 UTC.

[github-actions]

🤖 PR Summary

⚠️ PR title does not follow conventional commit format type[(scope)]: subject. Got: Introduce pullback argument for STIR and WHIR theorems

test summary

---

Statistics

Metric	Count
📝 Files Changed	6
✅ Lines Added	291
❌ Lines Removed	86

---

Lean Declarations

✏️ Added: 21 declaration(s)

ArkLib/Data/Domain/CosetFftDomain/Block.lean (2)

• theorem pairwise_disjoint_block {s : Set F} :
• theorem pairwise_disjoint_blockIdx {s : Set F} :

ArkLib/Data/Domain/CosetFftDomain/Pullback.lean (18)

• def pullback (ω : D) (l r : ℕ) (s : Finset F) : Finset (Fin (2 ^ (n - l)) × Fin (2 ^ (n - r)))
• def pullback₁ (ω : D) (l r : ℕ) (s : Finset F) : Finset (Fin (2 ^ (n - l)))
• def pullback₂ (ω : D) (l r : ℕ) (s : Finset F) : Finset (Fin (2 ^ (n - r)))
• lemma card_pullback_eq_card_pullback₁ :
• lemma card_pullback_eq_mul_card_pullback₂ (hl : l ≤ r) (hr : r ≤ n) :
• lemma card_pullback₂_eq (hl : l ≤ r) (hr : r ≤ n) (hs : s ⊆ (subdomain ω r).toFinset) :
• lemma mem_pullback {i : Fin (2 ^ (n - l)) × Fin (2 ^ (n - r))} :
• lemma mem_pullback₁ {i : Fin (2 ^ (n - l))} (hl : l ≤ r) (hr : r ≤ n) :
• lemma mem_pullback₁_iff_mem_pullback₂ {i : Fin (2 ^ n)} (hl : l ≤ r) (hr : r ≤ n) :
• lemma mem_pullback₁_iff_mem_pullback₂_l_0 {i : Fin (2 ^ n)} (hr : r ≤ n) :
• lemma mem_pullback₁_iff_mem_pullback₂_l_1 {i : Fin (2 ^ n)} (h1r : 1 ≤ r) (hr : r ≤ n) :
• lemma mem_pullback₂ {i : Fin (2 ^ (n - r))} (hl : l ≤ r) (hr : r ≤ n) :
• lemma mem_s_of_mem_pullback₁ {i : Fin (2 ^ (n - l))} (h : i ∈ pullback₁ ω l r s) :
• lemma proj₁_injOn :
• lemma proj₁_mapsTo :
• lemma proj₁_surjOn :
• lemma pullback_empty : pullback ω l r ∅ = ∅
• lemma pullback₁_eq_biUnion_pullback₂ (hl : l ≤ r) (hr : r ≤ n) :

ArkLib/Data/Domain/CosetFftDomain/Subdomain.lean (1)

• lemma subdomain_0_apply (i : Fin (2 ^ n)) :

---

sorry Tracking

• No sorrys were added, removed, or affected.

---

📋 **Additional Analysis**

Findings

Style Guide Violations

• File ArkLib/Data/CodingTheory/Basic/BlockRelDistance.lean, line 208: ac_nf used instead of ring: The style guide specifies using ac_nf for associativity/commutativity normalization only when the goal is a pure equality of arithmetic expressions over a commutative semiring. In this case, the goal after aesop is 2 ^ k * (complDisagreementSet k φ f g).card = 2 ^ k * (complDisagreementSet k φ f g).card, which is Nat multiplication. While ac_nf works, ring is the idiomatic choice for commutative ring arithmetic on Nat here. Replacing ac_nf with ring would be more standard.
• File ArkLib/Data/CodingTheory/ProximityGap/Folding.lean, line 680: omega used as catch-all without explicit arithmetic justification: The style guide recommends omega for linear arithmetic over Nat. However, the change at line 680 uses omega to prove a goal about Nat exponent comparisons (2 ^ (r - l) ≤ 2 ^ r). This is not purely linear and omega may fail or be fragile. A more explicit proof using Nat.pow_le_pow_right would be safer and more readable.
• File ArkLib/Data/Domain/CosetFftDomain/Pullback.lean, line 171: omega used incorrectly: The goal at that point is l + (r - l) = r, which omega can handle when l ≤ r. However, omega is not imported in this file; only linarith is available. Actually linarith is imported (line 14), but omega is not imported (only linarith is used). The proof should use linarith (or omega if we add the import). This is a minor inconsistency.
• Variable naming in Pullback.lean: In the file ArkLib/Data/Domain/CosetFftDomain/Pullback.lean, the variable F is declared as {F : Type} [Field F] [DecidableEq F]. The style guide prefers α, β, γ for generic types in non-algebraic contexts, but F is acceptable here since it's a field. However, the variable ω is used for the coset FFT domain (type D), which is unusual; typically ω would be an element of F. There is no strict violation here, just a deviation from common practice that may confuse readers.

Naming Conventions

• File ArkLib/Data/Domain/CosetFftDomain/Pullback.lean: The function pullback₁ and pullback₂ are named with subscripts using ₁ and ₂ (Unicode subscript 1 and 2). The style guide says "Functions and Terms: lowerCamelCase". While pullback₁ is technically lowerCamelCase with a subscript, this is unusual and may be considered a violation of the "use standard names" guideline. More conventional names would be pullbackFst and pullbackSnd or pullbackLeft and pullbackRight.
• File ArkLib/Data/Domain/CosetFftDomain/Pullback.lean: The lemma mem_s_of_mem_pullback₁ uses s (lowercase) in the name, which is fine, but the style guide prefers mem as a prefix for membership lemmas. This is correct.

Documentation Standards

• File ArkLib/Data/Domain/CosetFftDomain/Pullback.lean: The module-level docstring uses "/-! ... -/" correctly, includes a title, summary, notation, and references. The citation format [ACFY24stir] and [ACFY24] is correct per the citation standards. However, the References section does not include the full bibliographic entry for [ACFY24stir] (only [ACFY24] is listed in the template). Additionally, the references are added inline in the docstring, but the citation standards require a separate ## References section header, which is present. The file references [ACFY24stir] but there is no BibTeX entry for it in the references section; this is a violation.
• Declaration-level docstrings: Most definitions and lemmas have docstrings in the /-- ... -/ format. However, some lemmas lack docstrings (e.g., pullback_empty, proj₁_mapsTo, proj₁_surjOn). The style guide requires "Every definition and major theorem should have a docstring." These are not "major" theorems but they are public lemmas; adding brief docstrings would be good practice.

Progress Against Roadmap/Blueprint

• The diff introduces a new file ArkLib/Data/Domain/CosetFftDomain/Pullback.lean which implements a "pullback argument" used in Claim 4.23 of [ACFY24] and Lemma 4.9 of [ACFY24stir]. This aligns with the project's focus on active formalizations (STIR/WHIR papers).
• The refactoring in Folding.lean (replacing a long block with calls to Pullback lemmas) is a significant reduction in code size and complexity. It represents progress toward a more modular library structure.
• The changes to BlockRelDistance.lean (simplifying a simp call and using ac_nf) are minor cleanups.
• The addition of pairwise_disjoint_block and pairwise_disjoint_blockIdx to Block.lean provides utility lemmas used by the new Pullback file, meaning the code is properly structured.
• There is no mention of a blueprint for this Pullback file in the diff. The contribution guidelines require a blueprint for "substantial contributions, such as a new proof system". While the Pullback file is significant, it is not a new proof system; it's a new lemma module. The lack of a blueprint is likely acceptable, but we should note that the constraints ask to "cross-reference docs, wiki excerpts, or specs against the diff" — there is no blueprint mentioned, so no flag is raised.

Deprecation Policy

• No deprecated aliases are introduced or removed in this diff.

Licensing

• The new file Pullback.lean has the correct Apache 2.0 header with copyright and authors.

Code Quality Observations

• The file Pullback.lean has an unusually large number of imports (13 lines), some of which are heavy (GroupTheory.SpecificGroups.Cyclic, Algebra.Group.Fin.Basic). The style guide emphasizes minimizing imports. It's worth checking if all these imports are necessary.
• The use of set_option warning.simp.varHead false in Subdomain.lean (line 144) is a linter suppression; the style guide discourages suppressing linters without good reason. The comment says "false alert" but doesn't explain why; this should be documented.

---

📄 **Per-File Summaries**

• ArkLib.lean: Added an import ArkLib.Data.Domain.CosetFftDomain.Pullback line to the import block in ArkLib.lean. This makes the definitions and theorems from that new file available to any file that transitively imports ArkLib, enabling the CosetFftDomain module to now use pullback-related functionality.
• ArkLib/Data/CodingTheory/Basic/BlockRelDistance.lean: The proof of the private lemma card_agreementBlockUnion was refactored. The Finset.card_biUnion hypothesis was simplified from a multi-line aesop block to by simp, the Finset.sum_equiv block's inner aesop tactic was updated from add unsafe (by rw [mul_comm]) to add safe (by ac_nf), and an rw was combined onto the preceding line. No new theorems, definitions, or sorry/admit statements were introduced.
• ArkLib/Data/CodingTheory/ProximityGap/Folding.lean: The diff refactors hammingDistComplementBound to use the new Pullback.pullback API, replacing the inline Finset construction. The proof of contradictory_hamming_dist_formula is rewritten to use Pullback.card_pullback_eq_mul_card_pullback₂ and Pullback.card_pullback₂_eq, replacing a lengthy aesop block. In correlated_agreement_implies_contradictory_hamm_dist, the Hamming distance bound argument is simplified via Pullback.card_pullback_eq_card_pullback₁ and subdomain_0_apply. The typeclass constraint on dist_from_code_bound_of_correlated_agreement is relaxed from Fintype F to Finite F, and a Fintype.ofFinite instance is added in its body. The new import ArkLib.Data.Domain.CosetFftDomain.Pullback is added.
• ArkLib/Data/Domain/CosetFftDomain/Block.lean: Added two @[simp] theorems — pairwise_disjoint_block and pairwise_disjoint_blockIdx — each stating that, for any set s of field elements, the family of blocks (resp. block index sets) indexed by s is pairwise disjoint. Each theorem is proved with aesop using disjoint_block/disjoint_blockIdx and Function.onFun, extending the existing pairwise-disjointness API by providing the Set.PairwiseDisjoint variant.
• ArkLib/Data/Domain/CosetFftDomain/Pullback.lean: This new file adds the Pullback submodule under CosetFftDomainClass, defining three sets:

• pullback ω l r s – the pullback of two subdomain maps, consisting of pairs (i₁,i₂) such that subdomain ω l i₁ ^ 2^(r−l) = subdomain ω r i₂ and subdomain ω r i₂ ∈ s;
• pullback₁ ω l r s – the first projection (image under Prod.fst) of the pullback;
• pullback₂ ω l r s – the second projection (image under Prod.snd) of the pullback.

It proves:

• pullback_empty, mem_pullback, proj₁_injOn, mem_s_of_mem_pullback₁, mem_pullback₁ (characterizing membership when l ≤ r and r ≤ n), proj₁_mapsTo, proj₁_surjOn, and card_pullback_eq_card_pullback₁ (the first projection is a bijection onto pullback₁);
• mem_pullback₂ (characterizing membership in the second projection under the same bounds), mem_pullback₁_iff_mem_pullback₂, mem_pullback₁_iff_mem_pullback₂_l_0, mem_pullback₁_iff_mem_pullback₂_l_1 (relating the images of powers of ω inside the two projections);
• card_pullback₂_eq – when s is contained in subdomain ω r, the cardinality of pullback₂ equals |s|;
• pullback₁_eq_biUnion_pullback₂ – pullback₁ decomposes as a disjoint union of blocks indexed by pullback₂;
• card_pullback_eq_mul_card_pullback₂ – the cardinality of the pullback equals 2^(r−l) * #pullback₂.

No sorry or admit appear; all proofs are complete. The file is referenced as formalising ‘Claim 4.23 from [ACFY24] and lemma 4.9 from [ACFY24stir]’.

• ArkLib/Data/Domain/CosetFftDomain/Subdomain.lean: Added lemma subdomain_0_apply (@[simp]) which states no_index (subdomain ω 0 i) = ω i for any i : Fin (2 ^ n). This provides a simplification rule identifying the zeroth subdomain with the original coset FFT domain, facilitating proofs that involve the base subdomain. The proof uses aesop with added safe, unsafe, and simp rules.

---

Last updated: 2026-07-27 10:25 UTC.