lalalune · lalalune · Jul 22, 2026 · Jul 22, 2026
diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
@@ -26,21 +26,23 @@ jobs:
           fetch-depth: 0
 
       - name: Initialize timing paths
+        env:
+          BUILD_SOURCE_BRANCH: ${{ github.head_ref || github.ref_name }}
         run: |
-          echo "BUILD_TIMING_RESULTS=$RUNNER_TEMP/build-timing.jsonl" >> "$GITHUB_ENV"
-          echo "BUILD_TIMING_LOG_DIR=$RUNNER_TEMP/build-timing-logs" >> "$GITHUB_ENV"
-          echo "BUILD_TIMING_ARTIFACT_DIR=$RUNNER_TEMP/build-timing-artifact" >> "$GITHUB_ENV"
-          echo "BUILD_TIMING_ARTIFACT_NAME=arklib-build-timing-data" >> "$GITHUB_ENV"
-          echo "BUILD_TIMING_BASELINE_DIR=$RUNNER_TEMP/build-timing-baseline" >> "$GITHUB_ENV"
-          echo "BUILD_TIMING_REPORT=$RUNNER_TEMP/build-timing.md" >> "$GITHUB_ENV"
-          echo "BUILD_TIMING_COMMENT=$RUNNER_TEMP/build-timing-comment.md" >> "$GITHUB_ENV"
-          echo "BUILD_TIMING_SOURCE_SHA=$GITHUB_SHA" >> "$GITHUB_ENV"
-          echo "BUILD_TIMING_SOURCE_BRANCH=${{ github.head_ref || github.ref_name }}" >> "$GITHUB_ENV"
-          echo "BUILD_TIMING_BASE_REF=" >> "$GITHUB_ENV"
-          echo "BUILD_TIMING_MERGE_BASE_SHA=" >> "$GITHUB_ENV"
-          echo "BUILD_TIMING_TEST_NAME=Validation wrapper" >> "$GITHUB_ENV"
-          echo "BUILD_TIMING_TEST_COMMAND=./scripts/validate.sh" >> "$GITHUB_ENV"
           {
+            echo "BUILD_TIMING_RESULTS=$RUNNER_TEMP/build-timing.jsonl"
+            echo "BUILD_TIMING_LOG_DIR=$RUNNER_TEMP/build-timing-logs"
+            echo "BUILD_TIMING_ARTIFACT_DIR=$RUNNER_TEMP/build-timing-artifact"
+            echo "BUILD_TIMING_ARTIFACT_NAME=arklib-build-timing-data"
+            echo "BUILD_TIMING_BASELINE_DIR=$RUNNER_TEMP/build-timing-baseline"
+            echo "BUILD_TIMING_REPORT=$RUNNER_TEMP/build-timing.md"
+            echo "BUILD_TIMING_COMMENT=$RUNNER_TEMP/build-timing-comment.md"
+            echo "BUILD_TIMING_SOURCE_SHA=$GITHUB_SHA"
+            echo "BUILD_TIMING_SOURCE_BRANCH=$BUILD_SOURCE_BRANCH"
+            echo "BUILD_TIMING_BASE_REF="
+            echo "BUILD_TIMING_MERGE_BASE_SHA="
+            echo "BUILD_TIMING_TEST_NAME=Validation wrapper"
+            echo "BUILD_TIMING_TEST_COMMAND=./scripts/validate.sh"
             echo "BUILD_TIMING_SOURCE_SUBJECT<<EOF"
             git log -1 --format=%s
             echo "EOF"

diff --git a/.github/workflows/summary.yml b/.github/workflows/summary.yml
@@ -17,8 +17,11 @@ jobs:
   summarize:
     runs-on: ubuntu-latest
     timeout-minutes: 20
+    env:
+      OPENROUTER_KEY: ${{ secrets.OPENROUTER_KEY }}
     steps:
       - name: Generate PR Summary
+        if: env.OPENROUTER_KEY != ''
         uses: alexanderlhicks/lean-summary-workflow@main
         with:
           github_token: ${{ secrets.GITHUB_TOKEN }}
@@ -31,3 +34,8 @@ jobs:
           validate_title: 'true'
           upstream_path: 'ArkLib/ToMathlib/'
           # Other optional knobs (reasoning_effort, max_*_diff_chars): see the action README.
+
+      - name: Report unavailable optional summary
+        if: env.OPENROUTER_KEY == ''
+        run: |
+          echo "OPENROUTER_KEY is not configured; skipping the optional AI summary."
diff --git a/ArkLib/Data/CodingTheory/HigherOrderMDSOrderThreeFail.lean b/ArkLib/Data/CodingTheory/HigherOrderMDSOrderThreeFail.lean
@@ -25,7 +25,7 @@ interpolation normal `(X−a)(X−b) = X² − (a+b)X + ab`, i.e. to the point `
 sums make the three normals lie in a common plane (their `(sum, product)` points are collinear), so
 they are linearly dependent and the three pair-spans share the unexpected common vector
 `w = (0,1,10)` — even though generic position would force their intersection to be `{0}`.
- 
+
 
 `reedSolomonFrame_not_isHigherMDS_three_of_sumZeroPairs` records the unconditional special case
 `σ = 0` (antipodal pairs `{x, −x}`): this is the `a+b=0` relation that Sidon/`SidonModNeg` does NOT

diff --git a/ArkLib/Data/CodingTheory/ProximityGap/LineDecoding.lean b/ArkLib/Data/CodingTheory/ProximityGap/LineDecoding.lean
@@ -162,11 +162,11 @@ double-counting). Importing it here would require `a` to carry the GS degree str
 present statement abstracts `a` as a *free* `ℝ≥0`, severing that link. Closing this `sorry`
 faithfully therefore requires **strengthening the statement** to expose the GS interpolation
 (an `a := ℓ⁷(ρn)²/3`-shaped hypothesis with a `ReedSolomon.code`/Johnson-bound side condition),
-i.e. a documented statement REPAIR, *not* a leaf proof of the present black-box form. 
+i.e. a documented statement REPAIR, *not* a leaf proof of the present black-box form.
 
-This repair has now landed: `LineDecodingCoverage.lean` provides the faithful 
-repaired theorem `lineDecodable_imp_epsMCA_le_target` which explicitly consumes the 
-`MCAForallDoubleCover` overlap-coverage data rather than the refuted black-box 
+This repair has now landed: `LineDecodingCoverage.lean` provides the faithful
+repaired theorem `lineDecodable_imp_epsMCA_le_target` which explicitly consumes the
+`MCAForallDoubleCover` overlap-coverage data rather than the refuted black-box
 line-decodability implication.
 
 -/

diff --git a/ArkLib/Data/CodingTheory/Quarantine/DisproofFoldedRS.lean b/ArkLib/Data/CodingTheory/Quarantine/DisproofFoldedRS.lean
@@ -48,13 +48,13 @@ theorem anti_clustering_explosion (hs_pos : 0 < s) (hdiv : s ∣ N)
   · field_simp [hN]
 
 /--
-If the FRS decoder achieves capacity `1 - R`, it can list-decode when the 
-FRS block-error rate is strictly less than `1 - R`. However, because of the worst-case 
-anti-clustering adversary, the effective FRS block-error rate is `s * δ`. 
+If the FRS decoder achieves capacity `1 - R`, it can list-decode when the
+FRS block-error rate is strictly less than `1 - R`. However, because of the worst-case
+anti-clustering adversary, the effective FRS block-error rate is `s * δ`.
 
 Therefore, the maximum standard RS error rate `δ` that this unfold reduction can
 tolerate is strictly bounded by `(1 - R) / s`. Since `s ≥ 2`, this bound is at best
-`(1 - R) / 2`, which is drastically worse than true capacity `1 - R` and 
+`(1 - R) / 2`, which is drastically worse than true capacity `1 - R` and
 algebraically obliterates the reduction.
 -/
 theorem unfolded_capacity_bound (hs_pos : 0 < s) (R : ℝ) (δ : ℝ)

diff --git a/ArkLib/Data/CodingTheory/Quarantine/Hypotheses.lean b/ArkLib/Data/CodingTheory/Quarantine/Hypotheses.lean
@@ -6,7 +6,7 @@ import Mathlib.Algebra.BigOperators.Group.Finset.Basic
 /-!
 # Interdisciplinary Candidate Hypotheses for the Proximity Gap
 
-This file formalizes 4 candidate bounds drawn from cross-disciplinary 
+This file formalizes 4 candidate bounds drawn from cross-disciplinary
 theoretical frameworks, aiming to bound the capacity limit of Reed-Solomon codes.
 -/
 
@@ -25,8 +25,8 @@ variable (U : Finset (Fin n → F))
 
 --------------------------------------------------------------------------------
 -- Hypothesis 1: Statistical Mechanics (Spin-Glass Phase Transition)
--- Inspired by the clustering phase transition in random CSPs (like XORSAT), 
--- if the bundle size exceeds the Johnson radius, the code words must "shatter" 
+-- Inspired by the clustering phase transition in random CSPs (like XORSAT),
+-- if the bundle size exceeds the Johnson radius, the code words must "shatter"
 -- into disconnected components separated by distance > 2.
 --------------------------------------------------------------------------------
 @[reducible] def ShatteredBundle (U : Finset (Fin n → F)) : Prop :=
@@ -40,7 +40,7 @@ def hyp_SpinGlass_shattering (e : ℕ) (center : Fin n → F)
 --------------------------------------------------------------------------------
 -- Hypothesis 2: Quantum Information (QLDPC Algebraic Adaptation)
 -- In QLDPC codes, low-weight stabilizers force errors to be highly degenerate.
--- Adapted here: The intersection of the supports of any large bundle of close codewords 
+-- Adapted here: The intersection of the supports of any large bundle of close codewords
 -- must be empty to prevent trivial decoding collapse.
 --------------------------------------------------------------------------------
 def hyp_QLDPC_degeneracy (e : ℕ) (center : Fin n → F)
@@ -51,7 +51,7 @@ def hyp_QLDPC_degeneracy (e : ℕ) (center : Fin n → F)
 --------------------------------------------------------------------------------
 -- Hypothesis 3: Algebraic Geometry (Hasse-Weil Polynomial Adaptation)
 -- The number of points on a curve over a finite field is bounded by the Hasse-Weil theorem.
--- Translated to RS codes: The number of codewords agreeing on exactly `t` coordinates 
+-- Translated to RS codes: The number of codewords agreeing on exactly `t` coordinates
 -- is polynomially bounded.
 --------------------------------------------------------------------------------
 def hyp_HasseWeil_agreement_bound (t : ℕ) (x : Fin n → F) : Prop :=
@@ -61,9 +61,9 @@ def hyp_HasseWeil_agreement_bound (t : ℕ) (x : Fin n → F) : Prop :=
 
 --------------------------------------------------------------------------------
 -- Hypothesis 4: Additive Combinatorics (Sum-Product Correlation Limits)
--- By the sum-product phenomenon over finite fields, highly correlated errors 
+-- By the sum-product phenomenon over finite fields, highly correlated errors
 -- cannot grow multiplicatively without escaping the code space.
--- If we take the pointwise product of two distinct words in the code, their weight 
+-- If we take the pointwise product of two distinct words in the code, their weight
 -- is bounded away from zero.
 --------------------------------------------------------------------------------
 def hyp_SumProduct_escape (u1 u2 : Fin n → F) (h1 : C H_matrix u1)

diff --git a/ArkLib/Data/CodingTheory/Quarantine/HypothesesRefutations.lean b/ArkLib/Data/CodingTheory/Quarantine/HypothesesRefutations.lean
@@ -10,8 +10,8 @@ set_option maxRecDepth 4096
 /-!
 # Refutations of Interdisciplinary Candidate Hypotheses
 
-We use the generic GF(3) counterexample (n=4, k=2) to formally refute 
-the candidate bounds from statistical mechanics, quantum information, 
+We use the generic GF(3) counterexample (n=4, k=2) to formally refute
+the candidate bounds from statistical mechanics, quantum information,
 and additive combinatorics.
 -/
 
@@ -54,7 +54,7 @@ theorem survives_SpinGlass_shattering :
 --------------------------------------------------------------------------------
 -- Refuting Hypothesis 2: Quantum Information (QLDPC Degeneracy)
 -- The intersection of the supports of any large bundle (>2) is empty.
--- But the support of w0 is empty! Wait, if w0 is in U, then the intersection 
+-- But the support of w0 is empty! Wait, if w0 is in U, then the intersection
 -- is indeed empty. Let's shift the bundle so 0 is not in it.
 --------------------------------------------------------------------------------
 def v0 : Fin 4 → F := ![1, 1, 2, 0]
@@ -72,7 +72,7 @@ theorem refute_QLDPC_degeneracy :
 -- Refuting Hypothesis 4: Additive Combinatorics (Sum-Product Escape)
 -- The weight of the pointwise product is bounded by n - 1.
 -- Let's take w1 * w1 (pointwise). Wait, w1 = [1, 1, 2, 0], w1*w1 = [1, 1, 1, 0].
--- Weight is 3. But n - 1 = 3, so it's bounded. 
+-- Weight is 3. But n - 1 = 3, so it's bounded.
 -- What if we use a different code? Actually, we just need the weight of u1 * u2.
 -- If u1 = [1, 1, 2, 0] and u2 = [2, 1, 0, 1], u1*u2 = [2, 1, 0, 0]. Weight is 2.
 -- Let's find u1, u2 where weight is n = 4.
@@ -86,7 +86,7 @@ def c4 : Fin 3 → F := ![2, 2, 2]
 -- pointwise: c3 * c4 = [2, 2, 2]. weight is 3.
 -- So over n=3, weight is 3, which is not <= 2.
 theorem refute_SumProduct_escape :
-    ¬ (∀ (u1 u2 : Fin 3 → F), C H_MDS u1 → C H_MDS u2 → u1 ≠ u2 → 
+    ¬ (∀ (u1 u2 : Fin 3 → F), C H_MDS u1 → C H_MDS u2 → u1 ≠ u2 →
       weight (fun i => u1 i * u2 i) ≤ 2) := by
   intro h
   have h_bound : weight (fun i => c3 i * c4 i) ≤ 2 := h c3 c4 (by decide) (by decide) (by decide)

diff --git a/ArkLib/Data/CodingTheory/SubspaceDesign/Basic.lean b/ArkLib/Data/CodingTheory/SubspaceDesign/Basic.lean
@@ -6,21 +6,21 @@ import Mathlib.Algebra.BigOperators.Group.Finset.Basic
 # Subspace Designs
 
 This file provides the basic definitions and geometric properties of subspace designs.
-A collection of subspaces `H` is called an `(s, τ)`-strong subspace design if every 
-subspace `W` of dimension at most `s` intersects the subspaces in `H` with total 
-dimension bounded by `τ`. These structures are fundamental in the construction of 
+A collection of subspaces `H` is called an `(s, τ)`-strong subspace design if every
+subspace `W` of dimension at most `s` intersects the subspaces in `H` with total
+dimension bounded by `τ`. These structures are fundamental in the construction of
 list-decodable codes, such as in the Guruswami-Guo 2025 bounds for Reed-Solomon codes.
 
 ## Main definitions
-* `intersectionMultiplicity`: The sum of dimensions of the intersections of a subspace `W` 
+* `intersectionMultiplicity`: The sum of dimensions of the intersections of a subspace `W`
   with a family of subspaces `H`.
-* `IsTauSubspaceDesign`: The property that a family `H` forms a `τ`-subspace design 
+* `IsTauSubspaceDesign`: The property that a family `H` forms a `τ`-subspace design
   for a given dimension bound `s`.
 
 ## Main theorems
-* `intersectionMultiplicity_mono`: The intersection multiplicity is monotonically 
+* `intersectionMultiplicity_mono`: The intersection multiplicity is monotonically
   increasing with respect to subspace inclusion.
-* `intersectionMultiplicity_bound`: A geometric lemma bounding the intersection 
+* `intersectionMultiplicity_bound`: A geometric lemma bounding the intersection
   multiplicity of a larger subspace `W` based on a smaller subspace `W'`.
 -/
 
@@ -34,9 +34,9 @@ variable {ι : Type*} [Fintype ι] (H : ι → Submodule F V)
 noncomputable def intersectionMultiplicity (W : Submodule F V) : ℕ :=
   ∑ i, Module.finrank F ↥(H i ⊓ W)
 
-/-- The definition of a strong `τ`-subspace design. 
-A family `H` of subspaces is an `(s, τ)`-strong subspace design if for every 
-subspace `W` of dimension at most `s`, its intersection multiplicity with `H` 
+/-- The definition of a strong `τ`-subspace design.
+A family `H` of subspaces is an `(s, τ)`-strong subspace design if for every
+subspace `W` of dimension at most `s`, its intersection multiplicity with `H`
 is bounded by `τ`. -/
 def IsTauSubspaceDesign (s τ : ℕ) : Prop :=
   ∀ W : Submodule F V, Module.finrank F W ≤ s → intersectionMultiplicity H W ≤ τ

diff --git a/ArkLib/Interaction/Oracle/Core.lean b/ArkLib/Interaction/Oracle/Core.lean
@@ -7,7 +7,7 @@ imports it.  Parked to keep the root build green; un-park by migrating to the Ov
 (see issue #60 for the full diagnosis). -/
 
 /-
-/- 
+/-
 Copyright (c) 2026 ArkLib Contributors. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Quang Dao

diff --git a/ArkLib/Interaction/Oracle/Spec.lean b/ArkLib/Interaction/Oracle/Spec.lean
@@ -7,7 +7,7 @@ imports it.  Parked to keep the root build green; un-park by migrating to the Ov
 (see issue #60 for the full diagnosis). -/
 
 /-
-/- 
+/-
 Copyright (c) 2026 ArkLib Contributors. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Quang Dao

diff --git a/ArkLib/Interaction/Reduction.lean b/ArkLib/Interaction/Reduction.lean
@@ -7,7 +7,7 @@ imports it.  Parked to keep the root build green; un-park by migrating to the Ov
 (see issue #60 for the full diagnosis). -/
 
 /-
-/- 
+/-
 Copyright (c) 2026 ArkLib Contributors. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Quang Dao

diff --git a/ArkLib/OracleReduction/Composition/Sequential/AppendRbrKnowledgePerRoundDischarge.lean b/ArkLib/OracleReduction/Composition/Sequential/AppendRbrKnowledgePerRoundDischarge.lean
@@ -103,4 +103,4 @@ theorem appendRbrKnowledgeSoundnessPerRoundResidual_msg_subsingleton [Subsinglet
 end Verifier
 
 -- Axiom audit: must report only `[propext, Classical.choice, Quot.sound]` (no `sorryAx`).
-#print axioms Verifier.appendRbrKnowledgeSoundnessPerRoundResidual_msg_subsingleton
+#print axioms Verifier.appendRbrKnowledgeSoundnessPerRoundResidual_msg_subsingleton
diff --git a/ArkLib/OracleReduction/FiatShamir/DuplexSponge/Security/CacheProvenance.lean b/ArkLib/OracleReduction/FiatShamir/DuplexSponge/Security/CacheProvenance.lean
@@ -273,4 +273,4 @@ end DuplexSpongeFS.EagerLazyDS
 #print axioms DuplexSpongeFS.EagerLazyDS.cacheFold_pair_mem
 #print axioms DuplexSpongeFS.EagerLazyDS.mem_slotList_of_hash
 #print axioms DuplexSpongeFS.EagerLazyDS.mem_slotList_of_pair_fst
-#print axioms DuplexSpongeFS.EagerLazyDS.mem_slotList_of_pair_snd
+#print axioms DuplexSpongeFS.EagerLazyDS.mem_slotList_of_pair_snd
diff --git a/ArkLib/OracleReduction/FiatShamir/DuplexSponge/Security/Correspondence.lean b/ArkLib/OracleReduction/FiatShamir/DuplexSponge/Security/Correspondence.lean
@@ -1561,7 +1561,7 @@ theorem anchored_of_E_pinv
         hbj.symm.trans (heq ▸ hb')
       have hq : sO = q := Sum.inr.inj (Sum.inr.inj (congrArg Sigma.fst hbeq))
       exact Or.inr (by rw [hcapseg, ← hc5, hq])
-  
+
 open DuplexSpongeFS.Paper in
 /-- **E_func arm.** A function violation among dedup entries is impossible in a non-anchored
 consistent log: the earlier entry caches the forward key, contradicting the freshness of the

diff --git a/ArkLib/OracleReduction/FiatShamir/DuplexSponge/Security/Extraction.lean b/ArkLib/OracleReduction/FiatShamir/DuplexSponge/Security/Extraction.lean
@@ -501,4 +501,4 @@ end DuplexSpongeFS.EagerLazyDS
 #print axioms DuplexSpongeFS.EagerLazyDS.pairRecord_take_of_le
 #print axioms DuplexSpongeFS.EagerLazyDS.anchored_of_permInv_anchor
 #print axioms DuplexSpongeFS.EagerLazyDS.anchored_of_hash_anchor
-#print axioms DuplexSpongeFS.EagerLazyDS.anchored_of_perm_anchor
+#print axioms DuplexSpongeFS.EagerLazyDS.anchored_of_perm_anchor
diff --git a/ArkLib/OracleReduction/FiatShamir/DuplexSponge/Security/Lemma58CacheProvenance.lean b/ArkLib/OracleReduction/FiatShamir/DuplexSponge/Security/Lemma58CacheProvenance.lean
@@ -273,4 +273,4 @@ end DuplexSpongeFS.EagerLazyDS
 #print axioms DuplexSpongeFS.EagerLazyDS.cacheFold_pair_mem
 #print axioms DuplexSpongeFS.EagerLazyDS.mem_slotList_of_hash
 #print axioms DuplexSpongeFS.EagerLazyDS.mem_slotList_of_pair_fst
-#print axioms DuplexSpongeFS.EagerLazyDS.mem_slotList_of_pair_snd
+#print axioms DuplexSpongeFS.EagerLazyDS.mem_slotList_of_pair_snd
diff --git a/ArkLib/OracleReduction/FiatShamir/DuplexSponge/Security/Lemma58Correspondence.lean b/ArkLib/OracleReduction/FiatShamir/DuplexSponge/Security/Lemma58Correspondence.lean
@@ -1561,7 +1561,7 @@ theorem anchored_of_E_pinv
         hbj.symm.trans (heq ▸ hb')
       have hq : sO = q := Sum.inr.inj (Sum.inr.inj (congrArg Sigma.fst hbeq))
       exact Or.inr (by rw [hcapseg, ← hc5, hq])
-  
+
 open DuplexSpongeFS.Paper in
 /-- **E_func arm.** A function violation among dedup entries is impossible in a non-anchored
 consistent log: the earlier entry caches the forward key, contradicting the freshness of the

diff --git a/ArkLib/OracleReduction/FiatShamir/DuplexSponge/Security/Lemma58Extraction.lean b/ArkLib/OracleReduction/FiatShamir/DuplexSponge/Security/Lemma58Extraction.lean
@@ -501,4 +501,4 @@ end DuplexSpongeFS.EagerLazyDS
 #print axioms DuplexSpongeFS.EagerLazyDS.pairRecord_take_of_le
 #print axioms DuplexSpongeFS.EagerLazyDS.anchored_of_permInv_anchor
 #print axioms DuplexSpongeFS.EagerLazyDS.anchored_of_hash_anchor
-#print axioms DuplexSpongeFS.EagerLazyDS.anchored_of_perm_anchor
+#print axioms DuplexSpongeFS.EagerLazyDS.anchored_of_perm_anchor
diff --git a/ArkLib/OracleReduction/FiatShamir/HVZKLazyVerifier.lean b/ArkLib/OracleReduction/FiatShamir/HVZKLazyVerifier.lean
@@ -434,4 +434,4 @@ theorem deriveTranscriptFS_lazy_run_of_runOutput
 #print axioms runToRoundFS_lazy_cached
 #print axioms deriveTranscriptFS_lazy_run_of_runOutput
 
-end Reduction
+end Reduction
diff --git a/ArkLib/OracleReduction/FiatShamirRunCollapseProof.lean b/ArkLib/OracleReduction/FiatShamirRunCollapseProof.lean
@@ -28,10 +28,10 @@ namespace FiatShamirCollapse
 open scoped NNReal ProbabilityTheory
 open ProtocolSpec
 
-/-- **Issue #116 Resolution:** The Fiat-Shamir Collapse Kernel. 
-This theorem reduces the unproven residual to the State-Separation probability bounds 
+/-- **Issue #116 Resolution:** The Fiat-Shamir Collapse Kernel.
+This theorem reduces the unproven residual to the State-Separation probability bounds
 over the Random Oracle queries. -/
-theorem fiat_shamir_collapse_breakthrough 
+theorem fiat_shamir_collapse_breakthrough
     {ι : Type} {oSpec : OracleSpec ι}
     {StmtIn : Type} {ιₛᵢ : Type} {OStmtIn : ιₛᵢ → Type} {WitIn : Type}
     {StmtOut : Type} {ιₛₒ : Type} {OStmtOut : ιₛₒ → Type} {WitOut : Type}

diff --git a/ArkLib/ProofSystem/RingSwitching/SumcheckPhase.lean b/ArkLib/ProofSystem/RingSwitching/SumcheckPhase.lean
@@ -804,7 +804,7 @@ def iteratedSumcheckKStateProp (i : Fin ℓ') (m : Fin (2 + 1))
       (localChecks :=
         let explicitVCheck :=
           (∑ b ∈ (boolDomain L ℓ').points i, h_i.val.eval b) = stmt.sumcheck_target
-        
+
         explicitVCheck
       )
 

diff --git a/ArkLib/ToMathlib/KoalaBearAttackInstance.lean b/ArkLib/ToMathlib/KoalaBearAttackInstance.lean
@@ -325,4 +325,4 @@ end ArkLib
 #print axioms ArkLib.KoalaBearAttack.instance_violates
 #print axioms ArkLib.KoalaBearAttack.fenziSanso_upperBound_attack_concrete_residual_holds
 #print axioms ArkLib.KoalaBearAttack.fenziSanso_upperBound_attack_residual_holds
-#print axioms ArkLib.KoalaBearAttack.attackUpperBound
+#print axioms ArkLib.KoalaBearAttack.attackUpperBound