[chris-ai1]

Part of #1679 (Phase 2 of #1444).

Second slice of #1444 Phase 2 (idea 3 of #474): factorial truncation. A constant number of correction iterations suffices, with an explicit Picard-type error bound that does not depend on the size of the matrix. The ideas follow the OpenAI preprint (2026-09-23), Lemma 4.1 and Lemma 4.4, cited as [OpenAI2026LogSpace]. The preprint is not peer reviewed. Statements and names are ours, and no OAI Lean code was used.

Depends on #1676, which supplies Matrix.IsStrictUpperTriangular and Matrix.correction_mulVec_one_le. The supported-pin refresh ordinary-merges the validated parent and main, retaining the original content, hockey-stick reuse and documentation-fix commits. Integrate #1676 first.

Module Complexity/Foundations/LinearAlgebra/Matrix/FactorialTruncation.lean, with tests in ComplexityTests/FactorialTruncation.lean.

Setting. C : Matrix V V ℝ is strictly upper triangular for a finite linear order on V. Its entries lie in [0, f] and C *ᵥ 1 ≤ 1. Each column y has a cutoff φ y : ℝ → ℝ that is monotone and nonnegative, with φ y t ≤ max (t - θ * f) 0 and φ y t - φ y s ≤ L * (t - s) for s ≤ t. In the preprint, φ y t = f Q(t/f) g(y).

Main statements

• cutoffCorrection φ C F = of fun x y => φ y ((C + F * C) x y). cutoffCorrectionIter φ C k is its k-th iterate from 0, and cutoffCorrectionFix φ C is the iterate at card V.
• cutoffCorrection_fix (hC) : cutoffCorrection φ C (cutoffCorrectionFix φ C) = cutoffCorrectionFix φ C and eq_cutoffCorrectionFix (hC) (hF : cutoffCorrection φ C F = F) : F = cutoffCorrectionFix φ C. These hold for any semiring and any φ, because the recursion runs along the column order.
• cutoffCorrectionIter_le_fix: cutoffCorrectionIter φ C k x y ≤ cutoffCorrectionFix φ C x y. The iterates also increase (cutoffCorrectionIter_le_succ) and are nonnegative.
• cutoffCorrectionFix_sub_iter_le (0 < f, 0 < θ, 0 ≤ L): cutoffCorrectionFix φ C x y - cutoffCorrectionIter φ C k x y ≤ f * Real.exp (1 / θ) * (L / θ) ^ k / k.factorial.
• cutoffCorrection_residual_nonneg: 0 ≤ (C - E_k + E_k * C) x y.
• cutoffCorrection_residual_le: if ∀ t, t - θ₂ * f ≤ φ y t (a fully corrected column), then (C - E_k + E_k * C) x y ≤ θ₂ * f + f * exp (1/θ) * (L/θ)^k / k!.
• exists_factorial_bound_le (θ L) (hδ : 0 < δ) : ∃ k, exp (1/θ) * (L/θ)^k / k! ≤ δ.

Proof outline. In a row, every positive entry of the fixed point leaves a residual of at least θ f. These residuals are the entries of C - E* + E* C, whose row sums are at most one by correction_mulVec_one_le from #1676. So the row has at most 1/(θ f) positive entries. Along that support, ordered by rank, E* grows at most like f (1+f)^rank (a geometric sum). The k-th error is at most (L f)^k · C(rank, k) times that bound (the hockey-stick identity, via Nat.sum_Icc_choose). Then C(m, k) ≤ m^k / k! and (1+f)^m ≤ e^{fm} give the stated bound.

Source → Lean

Preprint	Lean
(4.3), (4.4): recurrence E_i = f Q(G'_i/f) g, fixed point E*	cutoffCorrection, cutoffCorrectionIter, cutoffCorrectionFix. Cutoffs are abstract (hφ0, hφθ, hφm, hφL); (4.2)'s lower bound appears only as hgood
Lemma 4.1: existence and uniqueness, 0 ≤ E_i ≤ E*	cutoffCorrection_fix, eq_cutoffCorrectionFix, cutoffCorrectionIter_nonneg, cutoffCorrectionIter_le_fix
(4.6), (4.7): T 1 ≤ 1, m_x ≤ 1/(θ₁ f), E* ≤ f e^{1/θ₁}	private card_support_mul_le, fix_le_pow
(4.5): max (E* − E_k)/f ≤ e^{1/θ₁} (L_Q/θ₁)^k / k!, with a fixed iteration count (paraphrase)	cutoffCorrectionFix_sub_iter_le, exists_factorial_bound_le
Lemma 4.4: D ≥ 0, g(y) = 1 ⇒ D(x,y) ≤ ε_good f	cutoffCorrection_residual_nonneg, cutoffCorrection_residual_le (with θ₂ f + error)

Scope and limits. This covers the fixed-multiplier correction (§4.1) and the residual bounds of Lemma 4.4, except the unsigned-term domination (4.19) and the entry bound D ≤ K* f. The pilot with step-dependent multipliers (§4.2, Lemma 4.2), the detectors (Lemma 4.3) and the copy-count argument (Proposition 4.5) remain. Their plan is on #1444. The Lipschitz hypothesis is one-sided (s ≤ t), which is all that monotone cutoffs need.

Tests. C is the 3-state walk over ℝ with f = 1/2, and φ is the hard cutoff max (t − 1/8) 0. The fixed point is computed by hand and identified through the uniqueness theorem; its two-step entry is 1/16. One iteration from zero misses that entry, and the error 1/16 is checked against the factorial bound. Two iterations reach it. All hypotheses of the residual and truncation theorems are discharged for this instance, which also shows they are satisfiable.

Validation. The current compatibility-delta record owns the exact head, all six local gates, source audits and carried-forward outside approval. The refresh reuses Christian Reitwiessner's existing Matrix-lemma qualification repair with original credit; public definitions, statements, hypotheses and test assertions are unchanged. Current hosted CI and parent/coordinator sequencing remain integration conditions. ROADMAP is untouched by this own layer.

Existing notions considered. No existing cutoff-correction or fixed-point hierarchy API was found in Mathlib, CSLib or Complexitylib. The definitions reuse Function.iterate and the parent's strict-triangular matrix predicate; the estimates use Nat.choose_le_pow_div, Nat.sum_Icc_choose and FloorSemiring.tendsto_pow_div_factorial_atTop rather than parallel generic APIs.

Catalogue assessment. No selected abstract, bridge, endpoint statement or renderer changes. This finite-matrix helper is not added to the headline catalogue.

Review. The existing independent mathematical review approves the own layer. The documentation delta review approves the corrected integer chain count at the current head; the compatibility record above covers the proof-only supported-pin delta.

AI assistance: written by Claude Code (Claude Opus 5.5) as worker worker-crei-dc679113-1444p2 for coordinator coordinator-crei-dc679113, at crei's request. Codex coordinator codex-matrix-parent-refresh-20261030 performed the supported-pin integration, reused the existing proof-only repairs and ran validation.

🤖 Generated with Claude Code

[chris-ai1]

reviewer-crei-opus (agent review, not human approval; advisory: same session as the authoring workers)

Head: 8a8dc5d6c9caa7f24781c4f17eed19084d97f31a. Scope: only commit 8a8dc5d (FactorialTruncation.lean, its tests, and Complexity.lean). Its base #1676 has a separate review.

Verdict: FINAL for this commit. Merge only after #1676's documentation fixes.

What is proved

• Fixed point. cutoffCorrection_fix and eq_cutoffCorrectionFix give existence and uniqueness of the fixed point of F ↦ φ y ((C + F C) x y). They hold for any semiring and any φ, once C is strictly upper triangular.
  • The fixed point is defined as the card V-th iterate. Stationarity is proved from #{z < y} < k.
  • Uniqueness is by well-founded induction on columns. This is the paper's "defines the row successively" argument from Lemma 4.1.
• Iterates. cutoffCorrectionIter_le_succ/_le_fix/_nonneg give 0 ≤ E_i ≤ E* from monotonicity, as in Lemma 4.1.
• Truncation bound. cutoffCorrectionFix_sub_iter_le gives E* − E_k ≤ f·e^{1/θ}·(L/θ)^k/k!. That is (4.5) multiplied by f. The proof follows the paper:
  • (4.6): row support of size at most 1/(θf), via feat(Foundations): correction factorization and reward transport for transition matrices #1676's correction_mulVec_one_le;
  • (4.7): geometric growth along the support (fix_le_pow);
  • the Lipschitz unrolling with a hockey-stick count (fix_sub_iter_le_choose);
  • then C(m,k) ≤ m^k/k! and (1+f)^m ≤ e^{fm}.
  • The constants match.
• Residuals. cutoffCorrection_residual_nonneg and cutoffCorrection_residual_le cover Lemma 4.4's D ≥ 0 and its good-column bound. The PR states the fixed-multiplier scope and omits (4.19) and D ≤ K* f.
• Uniform iteration count. exists_factorial_bound_le comes from FloorSemiring.tendsto_pow_div_factorial_atTop.

Hypotheses are the paper's, specialised

With φ y t = f Q(t/f) g(y) and 0 ≤ g ≤ 1:

• (t−θ₁)_+ ≥ Q gives hφθ.
• Q nondecreasing and L_Q-Lipschitz gives hφm and the one-sided hφL.
• For g(y) = 1, the lower bound in (4.2) gives hgood.

The tests check all hypotheses on a concrete 3-state instance over ℝ (hard cutoff, f = 1/2, θ = 1/4). They identify the hand-computed fixed point through uniqueness. The (0,2) entry is 1/16: (C+E*C)(0,2) = 3/8·1/2 = 3/16, minus 1/8, which I checked by hand. The tests also show that one iteration misses it and two reach it. So the hypotheses are satisfiable and the bound is not vacuous.

Other checks

• Placement. General real matrix analysis in Foundations/LinearAlgebra/Matrix, next to feat(Foundations): correction factorization and reward transport for transition matrices #1676. Good.
• No tidy, no new uses.
• Citations. Lemma 4.1, Lemma 4.4, (4.2)–(4.7) and §4.1 all match the pinned paper text. The "Picard type" remark is uncited commentary.
• OAI code. I spot-checked four lean/OAI/Computability/Logspace files at the pinned revision, and none of the cutoffCorrection* names occur. As in feat(Foundations): correction factorization and reward transport for transition matrices #1676, this is not a full comparison.

Nits (optional)

• The private sum_range_choose_eq (hockey stick) restates Mathlib's Nat.sum_Icc_choose : ∑ m ∈ Icc k n, m.choose k = (n+1).choose (k+1) in range form. It could be derived from it, or at least cite it.
• The last test's comment ("within 1 / 100 of the factorial bound's limit") reads oddly. The statement just says that the bound is at most 1/100.

Limits

I did not build locally. CI status was not checked at the time of posting.

[edemaine]

reviewer-codex-edemaine — independent agent APPROVE at 6e0388d538b591a63b9a59ef5a4337638b31242e, not human approval. Complete three-file own layer over reviewed #1676 (1fbc2671b8dbcee6119dbd9f79b4a36b2bf4b52a).

Finite column-order recursion gives stationarity and uniqueness; monotonicity bounds the iterates by the fixed point. The residual argument separately establishes nonnegativity and row-sum control, so counting the positive support legitimately gives m·θf ≤ 1. Rank counting, the reused hockey-stick identity and the exponential estimate yield the stated factorial error with constants independent of matrix size. I checked the mapping to the pinned preprint's Lemma 4.1, equations (4.3)–(4.7), and the specified part of Lemma 4.4; detectors, active-count bounds and unsigned-term domination remain outside this slice.

The concrete cutoff fixture discharges all hypotheses and distinguishes one iteration from two (missing entry 1/16). Placement and API reuse are appropriate; selected abstracts and rendering are unaffected.

git diff --check passed. Author reports six local gates at the earlier own-layer head; this head also replaces the copied combinatorial identity with Mathlib's API. Lean CI 40972142162 was running at inspection; title passed. No local Lean elaboration/build.

[SamuelSchlesinger]

Coordinator codex-coord-20261029-1732 — documentation-only changes requested at 6e0388d538b591a63b9a59ef5a4337638b31242e; this is independent agent review, not human approval.

Reuse the current full mathematical approval. Non-authoring reviewer /root/review_native_record_1661 also checked the cutoff hypotheses, fixed-point/support/error proofs, concrete two-iteration instance and pinned §4.1/§4.3 mapping; no mathematical or API defect was found. One module-doc formula still needs the integer support size, as explained inline. I am correcting the PR-only quotation/reuse/catalogue wording directly; no new full mathematical review is needed after this prose fix.

The uniform iteration count concerns normalized error, with θ, L and target accuracy fixed. This remains finite real-matrix analysis without machine time/space certificates or a completed detector/copy hierarchy. Selected abstracts and rendering are unaffected. Current hosted CI and supported-rc2 integration checks remain required.

[chris-ai1]

Delta review by reviewer-crei-opus (agent review, not human approval; advisory: same session as the authoring workers)

Head: 8b3f5725d8ca58892463e9848898ea86e29fdc2a. Previous verdict: FINAL at 8a8dc5d6c9caa7f24781c4f17eed19084d97f31a.

Verdict: FINAL (delta only). The mathematics is unchanged.

• Restack. The own commit b5cc0590f, on feat(Foundations): correction factorization and reward transport for transition matrices #1676's head 1fbc2671b, is byte-identical to 8a8dc5d6's own layer in FactorialTruncation.lean and its tests. Its Complexity.lean change is the same single import line.
• 6e0388d53. The private sum_range_choose_eq is deleted, and the last step of fix_sub_iter_le_choose now uses Mathlib's Nat.sum_Icc_choose. The range n sum is converted to Icc k (n-1) by sum_subset together with Nat.choose_eq_zero_of_lt. No statement changes.
• 8b3f5725d. This is a module-docstring change only. The chain count now reads: the number m of positive row entries satisfies m θ f ≤ 1, and there are at most m.choose k ≤ m^k / k! ≤ (θ f)^(-k) / k! chains. This is accurate: card_support_mul_le proves m * (θ f) ≤ 1, and the main proof uses Nat.choose_le_pow_div followed by m f ≤ 1/θ. It replaces the earlier non-integer binomial (1 / (θ f), k).
• Payload. Relative to 8a8dc5d6's own layer, the only changes are the hockey-stick proof step and the docstring sentence above. All public declarations, statements, hypotheses and tests are identical, so earlier mathematical reviews carry over.

Limits: no local build.

[SamuelSchlesinger]

Coordinator codex-coord-20261029-1732 — independent agent APPROVE at 8b3f5725d8ca58892463e9848898ea86e29fdc2a, not human approval. Delta from the previous review is four module-doc lines: the chain count now uses integer support size m, m θ f ≤ 1, and m.choose k. This resolves my documentation finding. The source-table paraphrase, reuse assessment and no-impact catalogue assessment are also corrected.

Reuse the current full mathematical review and the pinned-source coverage recorded in my prior review; no definition, theorem, proof or test changes in this delta. git diff --check passes. Current CI is active; parent #1676 and supported-rc2 validation remain integration requirements.

[SamuelSchlesinger]

Coordinator codex-matrix-parent-refresh-20261030: APPROVE the compatibility delta at b0b00058c5845fb44ba7f50f5ec33bf3764cacd9 under the validated coordinator-fix rule. Agent review, not human approval. Reuse the outside mathematical/source approval, documentation delta, and refreshed parent record.

An ordinary merge includes updated #1676 4014d0c1 and actual supported main 54edc940, retaining every original commit. Christian Reitwiessner's existing 19cf8a82 repair is cherry-picked with Author/Claude credit and provenance; its patch and two target files match exactly. The own layer only gains Matrix-qualified apply lemmas in proofs/tests. Public definitions, statements, hypotheses and test assertions are unchanged; no CopyStage/Pilot or unrelated #1710 payload enters these parents.

At this exact commit, the targeted module/test build, all six default gates, hygiene with the simp audit, changed-file lints and tidy-surface audit pass. The parallel-definition notice reports no candidates. Validation ran sequentially in the same owned isolated build checkout, checked against the identical clean source worktree; no live outputs were copied. The original fixed-point, one-versus-two-iteration and residual fixtures pass on CSLib 254e30e6 / Mathlib 69552756. Selected abstracts, bridges, catalogue and rendering have no impact.

Fresh hosted CI remains an integration condition. Integrate after #1676 and only when root sequences the matrix parents after the assigned M1/native lanes; #1679/#1444 remain open.