feat(Bridge/Clean): FormalCircuit as ConstraintSystem + BehavioralContract

[XC0R]

Summary

• toConstraintSystem: wraps FormalCircuit as a ConstraintSystem with input consistency and ConstraintsHold satisfaction
• toBehavioralContract: transfers original_soundness and original_completeness into BehavioralContract (0 sorrys)
• Targets upstream Verified-zkEVM/clean at 4a013fed (clean#357)

Supersedes #451. New file: ArkLib/Bridge/Clean.lean.

[github-actions]

🤖 PR Summary

Mathematical Formalization

• Integrates the Clean circuit framework into ArkLib/Bridge/Clean.lean using ConstraintSystem and BehavioralContract abstractions.
• Implements toConstraintSystem to wrap FormalCircuit with input consistency and ConstraintsHold satisfaction.
• Implements toBehavioralContract to transfer Clean's original_soundness and original_completeness theorems into the BehavioralContract interface.

Infrastructure

• Adds Verified-zkEVM/clean (revision 4a013fed) as an external dependency in lakefile.toml.
• Updates ArkLib.lean to export the new Bridge.Clean module.

Proof Completion

• All proofs are complete; no sorry or admit placeholders are used in the bridge implementation.

---

Statistics

Metric	Count
📝 Files Changed	4
✅ Lines Added	130
❌ Lines Removed	12

---

Lean Declarations

✏️ **Added:** 3 declaration(s)

• abbrev canonicalInputVar (Input : TypeMap) (F : Type) [Field F] [ProvableType Input] : in ArkLib/Bridge/Clean.lean
• noncomputable def toBehavioralContract (circuit : FormalCircuit F Input Output) in ArkLib/Bridge/Clean.lean
• def toConstraintSystem (circuit : FormalCircuit F Input Output) : in ArkLib/Bridge/Clean.lean

---

sorry Tracking

• No sorrys were added, removed, or affected.

---

🎨 **Style Guide Adherence**

The code review identified several stylistic violations in ArkLib/Bridge/Clean.lean regarding variable naming and syntax preferences. With over 20 total violations, they are grouped by rule below:

• Variable Conventions (Elements): 29 instances. The guide requires x, y, z, ... for elements of a generic type, but descriptive names were used instead.

  • Line 62: inp, out, and env are used as element names for Input F, Output F, and Environment F respectively.
  • Line 81: inp used instead of x.
  • Line 84: env used instead of y.

• Variable Conventions (Hypotheses): 18 instances. The guide requires h, h₁, ... for assumptions and hypotheses, but descriptive names were used.

  • Line 81: hWitGen used as a hypothesis name.
  • Line 86: hAssume, hEval, and hConstr used as hypothesis names.
  • Line 90: hLocalWit used as a hypothesis name.

• Syntax and Formatting (Functions): 8 instances. The guide specifies "Prefer fun x ↦ ... over λ x, ...", yet the code uses the => syntax for anonymous functions.

  • Line 57: Stmt := fun _ => Input F should use ↦.
  • Line 62: satisfies := fun _ inp out env => should use ↦.
  • Line 88: completeness := fun inp hAssume => by should use ↦.

• Variable Conventions (Generic types): 3 instances. The guide requires α, β, γ, ... for generic types.

  • Line 41: F is used for a generic field type.
  • Line 42: Input and Output are used as generic type parameters.

---

📄 **Per-File Summaries**

• ArkLib.lean: The changes in ArkLib.lean update the library's main entry point to include an import for the ArkLib.Bridge.Clean module, expanding the set of available definitions and theorems.
• ArkLib/Bridge/Clean.lean: This new file establishes a bridge between the Clean circuit framework and ArkLib by providing definitions to map a FormalCircuit to ArkLib's ConstraintSystem and BehavioralContract abstractions. The implementation includes formal proofs that transfer Clean's soundness and completeness guarantees to the ArkLib interface with no sorry placeholders.
• lakefile.toml: This change adds a new external dependency named Clean to the project's configuration, specifying its Git repository and a specific commit revision.

---

Last updated: 2026-05-09 10:13 UTC.

[mitschabaude]

Seems reasonable. I would only change the Stmt to include the output.

I wonder if the dependency shouldn't be the other way round - clean imports arklib. That would feel more natural, with clean being more like a frontend that will implement many concrete circuits, and arklib more like a backend

[mitschabaude]

I think better would be to make the statement an (Input F, Output F) pair

[mitschabaude]

Lgtm

[mitschabaude]

Ok so this assumption is kinda expected because FormalCircuits don't guarantee this. But we do have established a way to prove this quite easily for any given circuit, so the assumption could actually be removed with some massaging of the framework

[XC0R]

Output now in OStmt (0a71a4a). Stmt rather than OStmt would force the verifier to fix the output value; completeness could not existentially quantify over it.

On dependency direction: clean → arklib is neat long-term. Current direction avoids adding a dependency to Clean's lakefile without maintainer agreement. The bridge is ~100 lines either way.

hWitGen is addressable on the XC0R/clean fork toolchain-bump-v4.29 branch (~40+ commits, ~80+ files of v4.29 migration; core framework builds, handful of application circuits remaining). Upstream Clean has ~60+ new commits since the pinned rev, including the ProverHint refactor (PR #359) which restructures Environment and witness generation; relevant to this surface.

[mitschabaude]

Current direction avoids adding a dependency to Clean's lakefile without maintainer agreement. The bridge is ~100 lines either way.

I'm the maintainer of Clean, and I agree with the ArkLib dependency.

@quangvdao wdyt about the direction?

[quangvdao]

Does this mean Clean will depend on ArkLib or the other way around? I have no strong opinion either way

[XC0R]

Clean → ArkLib is the sound dependency direction. ArkLib provides the generic ConstraintSystem / BehavioralContract interface (#465); Clean instantiates it for FormalCircuit.

Concretely: ArkLib/Bridge/Clean.lean moves to Clean/ArkLib/Bridge.lean (or similar), Clean adds ArkLib as a lake dependency, and ArkLib stays constraint-system-agnostic. The bridge is ~100 lines either way; the difference is which repo carries the specificity.

This also means #465 can merge independently. It defines the target interface. The Clean-side instantiation lands separately.

[alexanderlhicks]

Re: dependency direction, I think it's fine either way and either direction does not necessarily preclude the other. I think for the purpose of ArkLib being a backend for Clean then Clean adding an ArkLib dependency makes more sense, but in ArkLib we might also benefit from having a circuit format which we can use to reason about recursion in a way that concretely ties in to what frontends do.

[lalalune]

G109 LANDED locally and kernel-checks: _G109ActualDepthTwoNonnegative.lean.

This completes G108's plumbing on the actual maximal-cancellation fibers. For negation-closed, zero-free G in an odd-characteristic finite field, if n = #G >= 4 and q = #F >= n^3, Lean proves:

0 <= actualDepthAnomaly G 2 2

Equivalently, allPairsDepthFiber G 2 2 <= q * depthFiber G 2 2.

Ingredients are all actual APIs: the 3n^2-3n additive-energy floor, rEnergy G 2 = additiveEnergy G, exact depth partition, G97's D0 <= 2n^2, G104's D1 = 0, and P2 <= n^4. Axiom audit: propext only; no sorry.

Interpretation: depth 2 is a genuine nonnegative producer throughout the prize regime, despite G107's sharp two-point negative countermodel. This does NOT close delta-star; higher-depth signed balance remains the obstruction.

[lalalune]

G114-G117 shifted-slice chain kernel-checks and closes the structural depth-five weld.

Verified chain:

• G114: each fixed tail pair is exactly one shifted k-block fiber, hence costs at most E_k(G).
• G115: summing tails gives blockEqualPairs <= E_k(G) * |G|^(2t).
• G116: the primitive equal-sum core injects into blockEqualPairs.
• G117: at (k,t)=(3,2), n=2^30, the exact primitive depth-five Wick target follows from E_3(G) <= 3728 n^3.

Thus the former refuted constant-21 cubic gate is replaced by a 177-times looser constant 3728. The structural slicing step has no analytic hypothesis. All headline declarations audit to propext only; no sorry.

Remaining honest obstruction: prove or refute the relaxed production cubic-energy estimate, then assemble the remaining signed depths.

[lalalune]

G118 kernel-checks: RepThree is sufficient to close the exact production primitive depth-five budget.

The existing canonical residual gives E3(G) <= 15|G|^3. Composing it with G117's shifted-slice chain immediately supplies the relaxed E3(G) <= 3728|G|^3 input and hence the |G|^8/288000 primitive-core target at |G|=2^30.

So the depth-five lane has no independent cubic-energy residual: it is closed with a 3728/15 slack factor once RepThree transfers to characteristic p. The honest remaining issue is exactly that order-six transfer (or a weaker bound allowing controlled non-pairing relation classes). G118 audits to propext only; no sorry.

[lalalune]

G119 kernel-checks and strictly weakens the depth-five analytic residual.

RepThree is not necessary. If the finite-field third energy is at most the characteristic-zero closed form plus C*n^2, with C <= 44, then round 53 absorbs the entire surplus into Wick headroom, yielding E3 <= 15n^3. Composed with G117, this proves the exact production primitive depth-five budget at n=2^30.

This route permits non-pairing six-term relations; it asks only for the aggregate bound:
addEnergy3(G) <= 15n^3 - 45n^2 + 40n + 44n^2.

Thus a single RepThree counterexample does not kill depth five. The new live target is a quadratic total wraparound surplus, not exact relation exclusion. Axiom audit: propext only; no sorry.

[lalalune]

G194 published: depth-three Möbius transform (d009d9cce, branch codex/g194-depth-three-mobius-transform).

The new frontier file proves the exact pointwise identity

factorialRepetitionDefect 3 = 3 * B - 2 * C,

where B is any canonical pair-collision fiber profile and C is the all-three-equal profile. The proof first establishes the per-triple equality-indicator identity, sums it over fibers, and uses coordinate symmetry to identify the three pair profiles.

Interpretation: the depth-three defect is not merely a positive union bound. The positive all-three overlap enters with coefficient -2; after centering and squaring, the exact next target is

V(D₃) = 9 V(B) + 4 V(C) - 12 centeredInner(B,C).

That polarization theorem is not claimed in G194; it is the next algebraic bridge needed before deciding whether the signed overlap is exploitable or another obstruction.

Validation passed:

• focused scripts/pg-iterate.sh check
• generated import update
• locked full build (8,458 jobs)
• accepted axioms only: propext, Classical.choice, Quot.sound

[lalalune]

G195 published: exact centered depth-three Möbius polarization (dfe94c462, branch codex/g195-depth-three-centered-mobius).

New axiom-clean results:

• reusable scalar bilinearity for centeredInner and quadratic scaling/subtraction laws for centeredSqMass;
• the structural bridge exactlyTwoEqualProfile = 3 · (pair01Profile - allThreeEqualProfile);
• the covariance-coordinate bridge
  ⟨E,C⟩_c = 3⟨B,C⟩_c - 3V(C);
• the exact target
  V(D₃) = 9V(B) + 4V(C) - 12⟨B,C⟩_c;
• hence ⟨B,C⟩_c ≥ 0 removes the entire signed correction from the unsigned diagonal envelope.

This is quantitatively nontrivial on G193's genuine subgroup {1,2,4} ⊂ (ZMod 7)ˣ. Its recorded values V(E)=54, V(C)=12, and ⟨E,C⟩_c=9, combined with the bridge, force ⟨B,C⟩_c=15 and V(B)=24. Thus the unsigned Möbius diagonal is 9·24+4·12=264, while the signed correction is 12·15=180, recovering the exact defect energy 84. The overlap cancellation is therefore real and large, not just formal.

Validation:

• scripts/pg-iterate.sh passed;
• generated imports updated;
• serialized module build passed (8,459 jobs);
• target axioms only propext, Classical.choice, Quot.sound.

Next angle: formalize the F₇ numerical Möbius certificate, then determine whether ⟨B,C⟩_c ≥ 0 survives for all genuine multiplicative subgroups or needs a sharper lower bound.

[lalalune]

G196 published: explicit F₇ Möbius cancellation certificate (fcf0b53ba, branch codex/g196-f7-mobius-cancellation).

For the genuine order-three subgroup G={1,2,4}⊂(ZMod 7)ˣ, Lean now proves in the signed G195 coordinates:

• centeredInner B C = 15;
• V(B)=24;
• unsigned diagonal 9V(B)+4V(C)=264;
• signed correction 12 centeredInner(B,C)=180;
• exact defect energy V(D₃)=264-180=84;
• cancellation ratio 180/264=15/22.

So triple overlap cancels over 68% of the naïve unsigned Möbius envelope in this actual subgroup. This gives a checked regression benchmark for any proposed general pair/triple correlation theorem.

Validation passed: focused proximity iteration, generated import update, and serialized module build (8,460 jobs). All printed targets use only propext, Classical.choice, and Quot.sound.

Next: probe the sign of centeredInner B C across small genuine multiplicative subgroups. A negative example would close the universal-sign angle; persistent positivity would motivate a structural theorem in convolution coordinates.

[lalalune]

G197 published: universal depth-three Möbius overlap sign REFUTED (47403a3de, branch codex/g197-f5-mobius-sign-refuted).

For the genuine full multiplicative subgroup G=F₅ˣ={1,2,3,4}, Lean proves:

• pair profile B=(4,3,3,3,3);
• triple profile C=(0,1,1,1,1);
• centeredInner(B,C)=-4, hence ¬ 0 ≤ centeredInner(B,C);
• V(B)=V(C)=4;
• unsigned Möbius diagonal 9V(B)+4V(C)=52;
• signed term -12 centeredInner(B,C)=+48;
• exact defect energy V(D₃)=100.

Equivalently, the subgroup incidence count is N=#{(x,z,a)∈G³:2x+z=3a}=12, so pN-|G|³=5·12-4³=-4.

Thus the overlap term can either cancel (G196/F₇: −180) or amplify (G197/F₅: +48). Any all-subgroup deletion argument based only on centeredInner(B,C)≥0 is closed. The result is recorded in DISPROOF_LOG.md.

Validation passed: focused proximity check and serialized module build (8,461 jobs); printed targets use only propext, Classical.choice, Quot.sound.

Next viable refinement: derive the exact incidence-count normal form centeredInner(B,C)=pN-n³ abstractly, then seek magnitude control rather than a false universal sign.

[lalalune]

G198 published: exact depth-three Möbius incidence normal form (963e826e9, branch codex/g198-mobius-incidence-normal-form).

Lean now parameterizes the canonical pair collision by (x,z)∈G² with target 2x+z, and the triple collision by a∈G with target 3a. It proves exact fiber bijections and mass laws:

• Σ_t B(t)=|G|²;
• Σ_t C(t)=|G|;
• N := Σ_t #{(x,z):2x+z=t}·#{a:3a=t};
• centeredInner(B,C)=|F|·N-|G|³.

Consequences formalized:

• centeredInner(B,C)≥0 ↔ |G|³≤|F|N, identifying exactly why G197 refutes the sign gate;
• |centeredInner(B,C)| = ||F|N-|G|³|;
• V(D₃)=9V(B)+4V(C)-12(|F|N-|G|³).

This replaces the false qualitative sign target with a precise incidence-discrepancy magnitude target. For prime fields with 3≠0, N is the direct count of (x,z,a)∈G³ satisfying 2x+z=3a.

Validation passed: focused proximity check and serialized build (8,462 jobs). All printed declarations use only propext, Classical.choice, and Quot.sound.

Next analytic question: bound ||F|N-|G|³| using subgroup additive-collision / Stepanov machinery, and compare its exponent against the depth-three deletion budget.

[lalalune]

G199 published: multiplicative normalization of the depth-three Möbius incidence (a185b659c, branch codex/g199-multiplicative-incidence-normalization).

For any finite nonzero multiplicatively closed/inverse-closed G, Lean proves:

• N = Σ_{a∈G} #P(3a) without assuming multiplication by 3 is injective;
• every P(3a) is bijective, via division by a, to {(u,v)∈G² : 2u+v=3};
• hence N=|G|·M;
• M=#{u∈G : 3-2u∈G} by uniqueness of v;
• therefore
  centeredInner(B,C)=|G|·(|F|·M-|G|²).

This is the sharpest coordinate reduction in the G194–G199 chain: a three-variable signed overlap has become one affine intersection of two multiplicative cosets.

Important applicability audit: the current G103F Stepanov theorem controls #{x∈H:x-c∈H} for the same subgroup H. Here M=#{u∈G:3-2u∈G}; after x=2u, the two sides are generally distinct multiplicative cosets unless coefficient/sign dilations lie in G. Therefore G103F cannot be cited directly in full generality. The honest next analytic target is the two-coset Stepanov generalization (relations x^n=α, (x-c)^n=β), or a proof that the production subgroup absorbs the required coefficients.

Validation passed: focused proximity check and serialized build (8,463 jobs); printed targets use only propext, Classical.choice, and Quot.sound.

[lalalune]

G200 published: coefficient-absorption bridge to the existing Stepanov theorem (004e13c33, branch codex/g200-coefficient-absorption-stepanov).

New exact result: if a nonzero multiplicative subgroup-like G contains 2 and -1, multiplication by 2 bijects

{u∈G : 3-2u∈G}

with the standard shifted collision set

{x∈G : x-3∈G}.

Over ZMod p, G103F therefore applies verbatim: under 2≤B, 2B≤t, 2t≤B³, tB≤p, x^t=1 on G, and nonzero 2/3, Lean proves

#affineCollisionFilter G ≤ 4B².

Applicability is explicitly fenced. The genuine order-three subgroup {1,2,4}⊂F₇ˣ contains 2 but not -1, proved by the new audit theorem, so coefficient absorption is not automatic from subgroup closure. In the general case the remaining target is genuinely a two-coset Stepanov theorem.

Validation passed: focused proximity check and serialized build (8,464 jobs); targets use only propext, Classical.choice, and Quot.sound.

[lalalune]

G201 published: common-envelope Stepanov reduction (e9b9bf4f0, branch codex/g201-common-envelope-stepanov).

For arbitrary coefficient cosets, choose H with 2G⊆H and −G⊆H. Lean proves the injection

u ↦ 2u : {u∈G : 3−2u∈G} ↪ {x∈H : x−3∈H}.

Consequently, if H satisfies G103F's root-of-unity and parameter hypotheses at exponent t, then

M ≤ 4B².

The result is also composed all the way back to the signed overlap:

centeredInner(B,C) ≤ |G|·(p·4B²−|G|²).

This is fully general at the combinatorial level; the exact analytic cost is that t is the exponent of the common envelope H, not necessarily |G|. Thus the next production audit is purely arithmetic: determine the smallest root-of-unity envelope containing both 2G and −G, equivalently the subgroup generated by G and the coefficient ratio −2, and test whether its exponent remains in the Stepanov range.

Validation passed: focused proximity check and serialized build (8,465 jobs); targets use only propext, Classical.choice, and Quot.sound.

[lalalune]

G202 published: common-envelope exponent overhead is genuine (40922ea90, branch codex/g202-envelope-exponent-overhead).

Generic necessary condition now proved: if 1∈G, 2G⊆H, and every x∈H satisfies x^n=1, then 2^n=1. Thus G201 can retain the original subgroup exponent only when the coefficient 2 already has compatible order.

Concrete certified obstruction:

• G={1,3,9,27,40,38,32,14}⊂F₄₁ˣ is a genuine order-eight subgroup;
• 2^8=10≠1;
• therefore no envelope containing even 2G can have exponent eight;
• (-2)^20=1, and every positive power below 20 is non-one, certifying exact order 20.

So the coefficient-generated common envelope cannot uniformly preserve the smooth subgroup scale. The envelope workaround can incur arithmetic enlargement before Stepanov is applied; a general prize argument cannot silently set t=|G|.

Validation passed: focused proximity check and serialized build (8,466 jobs); printed results use only accepted axioms.

Next surviving route: generalize the two-relation Stepanov construction directly to distinct cosets x^n=α, (x-c)^n=β, which should retain exponent n and avoid the G202 envelope penalty.

[lalalune]

G203 published: scalar-twisted generators for direct two-coset Stepanov (957227b68, branch codex/g203-two-coset-twisted-generators).

For distinct nonzero relation values x^t=α and (x-c)^t=β, define the G103F generator indexed by (a,b,b′) with scalar twist α^{-b}β^{-b′}.

Lean proves:

• the twisted family is linearly independent under exactly G103F's original DB≤t, tB≤p, c≠0 hypotheses;
• its degree bound is unchanged;
• the Hasse degeneracy identity survives with the twist scalar multiplying the same condition polynomial;
• at a two-coset collision point,
  α^{-b}β^{-b′}x^{tb}(x-c)^{tb′}=1.

This removes the G202 envelope obstruction at the generator level while retaining exponent t. The remaining assembly is to rebuild G103F's coefficient-kernel vanisher with twisted condition polynomials, then reuse the root-multiplicity/counting argument.

Validation passed: focused proximity check and serialized build (8,467 jobs); all printed declarations use accepted axioms only.

[lalalune]

G204 published: full two-coset Stepanov vanisher (1091c78e0, branch codex/g204-two-coset-vanisher).

For arbitrary nonzero α,β, under the original G103F parameter hypotheses DB≤t, 2D≤B², tB≤p, c≠0, Lean constructs a nonzero polynomial Ψ with

• deg Ψ ≤ (D−1)+2t(B−1);
• D ≤ rootMultiplicity Ψ x for every x satisfying x^t=α and (x−c)^t=β.

Key correction discovered and formalized during assembly: the generators carry the scalar twist, but the coefficient-kernel conditions remain the original condPoly. At collision points the twist cancels α^bβ^{b′}, leaving precisely the untwisted condition polynomial. This preserves the original condition count D(2D−1)<DB².

The envelope overhead from G202 is now eliminated at the vanisher level. Only the standard multiplicity-to-cardinality wrapper and D=⌊t/B⌋ arithmetic remain to obtain the direct two-coset 4B² theorem.

Validation passed: focused proximity check and serialized build (8,468 jobs); all targets use accepted axioms only.