The certification solution

The theorems of Challenge.lean, each proved by the theorem of record of the same name. Comparator confirms at the kernel-export level that the statements match the challenge's, that the proofs use no axiom outside [propext, Classical.choice, Quot.sound], and that the kernel accepts them; see comparator-config.json and the CI workflow.

theorem Certified.regts_sevenster_converse : RS.RegtsSevensterConverseStatement

The converse: every mixed partition function is an edge-rank-bounded parameter, with base max 1 (k + 2ℓ).

theorem Certified.edgeRankBounded_of_mixedBounded {f : RS.ClosedFragment → ℂ} {B : ℕ} (hf : RS.IsMixedPartitionFunctionBounded f B) : RS.EdgeRankBounded f (max 1 (2 * B))

The rank bound from a bounded mixed partition function.

theorem Certified.regts_sevenster : RS.RegtsSevensterStatement

The forward direction, with no hypothesis.

theorem Certified.regts_sevenster_quant : RS.RegtsSevensterStatementQuant

The quantitative forward direction, with no hypothesis: both dimensions at most ⌊2eR⌋.

theorem Certified.regts_sevenster_total : RS.RegtsSevensterStatementTotal

The total-dimension forward direction: the representing model has k + 2 * ℓ ≤ R.

theorem Certified.regts_sevenster_characterisation (f : RS.ClosedFragment → ℂ) (hempty : f RS.emptyClosedFragment = 1) (hiso : ∀ (W₁ W₂ : RS.ClosedFragment) (a : RS.Fragment.Equiv W₁ W₂), f W₁ = f W₂) : (∃ (R : ℕ), RS.EdgeRankBounded f R) ↔ RS.IsMixedPartitionFunction f

The characterisation: a fragment parameter has bounded edge rank exactly when it is a mixed partition function.

theorem Certified.regts_sevenster_quant_characterisation (f : RS.ClosedFragment → ℂ) (hempty : f RS.emptyClosedFragment = 1) (hiso : ∀ (W₁ W₂ : RS.ClosedFragment) (a : RS.Fragment.Equiv W₁ W₂), f W₁ = f W₂) : (∀ (R : ℕ), RS.EdgeRankBounded f R → RS.IsMixedPartitionFunctionBounded f ⌊2 * Real.exp 1 * ↑R⌋₊) ∧ ∀ (B : ℕ), RS.IsMixedPartitionFunctionBounded f B → RS.EdgeRankBounded f (max 1 (2 * B))

The quantitative round trip: edge rank R gives dimension ⌊2eR⌋, and dimension B gives edge rank base max 1 (2B).