Prove STIR out-of-domain sampling bound

[latifkasuli]

What changed

• prove the STIR out-of-domain sampling bound without sorry
• expose Combine.block_size for the proof's public statement
• add a compact consumer proposition and kernel-checked bridge theorem for downstream verification tools

Why

The out-of-domain theorem was blocked by sorryAx, so source-pinned research agents could retrieve it but could not honestly promote it into a kernel-verified premise benchmark. The compact interface keeps ordinary consumer replay within a bounded heartbeat policy while its kernel dependency closure still reaches the full theorem.

Validation

• lake build ArkLib.ProofSystem.Stir.OutOfDomSmpl
• trusted collectAxioms audit: only propext, Classical.choice, and Quot.sound
• MathVerify clean declaration-readiness gate: both the full theorem and compact interface report ready at commit 93d3db6c714536b98c52c0ba9a60c347af5e4aa2
• source-pinned lexical and hybrid premise replay: promoted case ranks first and kernel-verifies in both modes

Boundary

This proves the selected ArkLib proposition under its current definitions and allowed Lean axioms. It does not by itself establish end-to-end STIR soundness or correspondence with every informal paper claim.

[github-actions]

🤖 PR Summary

⚠️ PR title does not follow conventional commit format type[(scope)]: subject. Got: Prove STIR out-of-domain sampling bound

sorry delta: -1 (1 removed) — net proof progress

Proof Completion (sorries removed)

• out_of_dom_smpl_1 (in ArkLib/ProofSystem/Stir/OutOfDomSmpl.lean): The sorry placeholder has been replaced with a full proof. The proof uses three new private lemmas: prob_exists_le_sum (union bound for probabilities), prob_uniform_fin_forall (probability that a random function from Fin s satisfies a pointwise condition), and card_eval_eq_le (bounds count of evaluation collisions by degree-1). A cast helper coe_choose_two_nnreal is also added. No new sorry or admit are introduced anywhere.

Mathematical Formalization

• outOfDomainSamplingBound: A new public top-level proposition formalizing the polymorphic form of Lemma 4.5.2 (STIR out-of-domain sampling bound).
• out_of_dom_smpl_2_statement: A new public lemma that proves outOfDomainSamplingBound by rewriting the pre-existing out_of_dom_smpl_2. This serves as a compact consumer-facing interface whose kernel dependency closure reaches the full theorem.
• The existing definitions listDecodingCollisionProbability and the lemma out_of_dom_smpl_2 remain unchanged.

Refactoring / API Changes

• Combine.block_size (in ArkLib/ProofSystem/Stir/Combine.lean): Changed from private to public, and a docstring added explaining its use in the type of master_lemma and by downstream consumers that need to reference it without relying on a private generated name.

Infrastructure / CI

• set_option maxHeartbeats increases in OutOfDomSmpl.lean: two increases (1,000,000 and 5,000,000) are applied to the new top-level definitions (outOfDomainSamplingBound and out_of_dom_smpl_2_statement) to accommodate the elaboration budget. No other infrastructure or CI changes.

Scope and Context

The core mathematical change is the proof completion and new formalization in OutOfDomSmpl.lean; the Combine.lean change is a minor visibility adjustment. The PR does not claim end-to-end STIR soundness or full correspondence with informal paper claims, only that the selected ArkLib proposition is now proven under its current definitions and allowed Lean axioms.

---

Statistics

Metric	Count
📝 Files Changed	2
✅ Lines Added	226
❌ Lines Removed	2

---

Lean Declarations

✏️ Added: 6 declaration(s)

ArkLib/ProofSystem/Stir/OutOfDomSmpl.lean (6)

• def outOfDomainSamplingBound : Prop
• lemma out_of_dom_smpl_2_statement : outOfDomainSamplingBound
• private lemma card_eval_eq_le
• private lemma coe_choose_two_nnreal (n : ℕ) :
• private lemma prob_exists_le_sum
• private lemma prob_uniform_fin_forall

✏️ Affected: 1 declaration(s) (line number changed)

• def block_size (dstar : ℕ) (degs : Fin m → ℕ) (i : Fin m) in ArkLib/ProofSystem/Stir/Combine.lean moved from L98 to L102

---

sorry Tracking

✅ Removed: 1 `sorry`(s)

ArkLib/ProofSystem/Stir/OutOfDomSmpl.lean (1)

• lemma out_of_dom_smpl_1 (L59)

---

📋 **Additional Analysis**

The diff introduces several style violations against the ArkLib contribution guidelines, particularly in naming conventions, documentation, line length, parenthesis usage, and terminal simp calls. The following list details each issue found in the changed code.

---

📄 **Per-File Summaries**

• ArkLib/ProofSystem/Stir/Combine.lean: The block_size definition in ArkLib/ProofSystem/Stir/Combine.lean was changed from private to public (non-private), and a docstring was added explaining its use in the type of master_lemma and downstream consumers that must reference it without relying on a private generated name. No other changes occur in this diff.
• ArkLib/ProofSystem/Stir/OutOfDomSmpl.lean: The diff replaces the sorry placeholder in out_of_dom_smpl_1 with a full proof, using three new private lemmas: prob_exists_le_sum (a union bound for probabilities), prob_uniform_fin_forall (computes probability that a random function from Fin s satisfies a pointwise condition), and card_eval_eq_le (bounds count of evaluation collisions by degree - 1). It also adds coe_choose_two_nnreal (a cast identity for binomial coefficients in NNReal). The listDecodingCollisionProbability definition and out_of_dom_smpl_2 lemma are unchanged, but the diff introduces a new top-level proposition outOfDomainSamplingBound (the polymorphic form of Lemma 4.5.2) and a lemma out_of_dom_smpl_2_statement that proves it by rewriting out_of_dom_smpl_2. The two new definitions each carry a set_option maxHeartbeats increase (1,000,000 and 5,000,000 respectively) to accommodate the elaboration budget. No new sorry or admit are introduced.

---

Last updated: 2026-07-12 18:54 UTC.