[chris-ai1]

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

First slice of #1444 Phase 2 (ideas 2 and 4 of #474): the exact algebra of the correction-and-copy hierarchy, as general facts about finite matrices. Nothing here involves machines. Statements and names are ours. The ideas follow the OpenAI preprint (2026-09-23), Section 4, cited as [OpenAI2026LogSpace] with the source revision pinned in references.bib. The preprint is not peer reviewed. No OAI Lean code was used, translated or consulted.

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

What it proves

• Correction. In any ring, (1 + e) * (1 - c) = 1 - (c - e + e * c) (one_add_mul_one_sub_eq_one_sub). For matrices, (1 - (C - E + E * C)) *ᵥ p = (1 + E) *ᵥ ((1 - C) *ᵥ p). So if p solves (1 - C) p = e, it also solves the corrected equation with reward e + E e. When IsUnit (1 + E).det, (1 - (C - E + E * C))⁻¹ *ᵥ (e + E *ᵥ e) = (1 - C)⁻¹ *ᵥ e. This holds in particular for E.IsStrictUpperTriangular, a new predicate (Mathlib only has the non-strict IsUpperTriangular), with det (1 + E) = 1. If E ≥ 0 and C *ᵥ 1 ≤ 1, then (C - E + E * C) *ᵥ 1 ≤ C *ᵥ 1, so row sums do not grow. Nonnegativity of C - E + E * C depends on the choice of E and is proved for cutoff corrections in feat(Foundations): factorial truncation of cutoff corrections #1677.
• Copies. copySplit r s D gives each vertex copies (x, i) with row weights r i x and splits each entry D x y in proportions s x y j. copyWeight r is the weighted projection to parents. If ∑ j, s x y j * r j y = 1 wherever D x y ≠ 0, then copySplit r s D * copyWeight r = copyWeight r * D. The copy step preserves nonnegativity, and it preserves substochasticity when the weights are at most one and the proportions sum to at most one.
• Reward transport. Let C l, E l and P l : Matrix (V (l+1)) (V l) be stages with C (l+1) * P l = P l * (C l - E l + E l * C l). Let Pc = copyProjection P and B = rewardTransport P E be the cumulative products. Then C l * Pc l = Pc l - B l * (1 - C 0). Hence B l *ᵥ e = Pc l *ᵥ p - C l *ᵥ (Pc l *ᵥ p) whenever (1 - C 0) *ᵥ p = e.
• Stage error. Under nonnegativity, substochastic P l and 0 ≤ p ≤ 1, take primary copies z l, whose rows of P l are unit vectors. Then p (z 0) - (B l *ᵥ e) (z l) ∈ Set.Icc 0 (∑ y, C l (z l) y), which is at most #A • ε when the entries of C l are at most ε and its nonzero columns lie in A. The paper's form is sub_rewardTransport_mulVec_le_pow: if the entries of C l are at most (2^(c+1))⁻¹^l and its active columns number at most 2^l * n, then 0 ≤ p (z 0) - W l (z l) ≤ n * (2^c)⁻¹^l.

Source → Lean

Preprint (Section 4)	Lean
D = C − E + EC, I − D = (I+E)(I−C), (I+E)W = (I−D)p (§4 intro)	one_add_mul_one_sub_eq_one_sub, Matrix.one_sub_correction_mulVec, Matrix.inv_one_sub_correction_mulVec
D1 = C1 − E(1 − C1) ≤ C1 (Lemma 4.4, row-sum part)	Matrix.correction_mulVec_one, Matrix.correction_mulVec_one_le
copies C⁺(x_i, y_j) = r_i(x) D(x,y) s_j(D(x,y)/f), C⁺P_r = P_r D (4.23), (4.26); substochastic (Prop. 4.5)	Matrix.copySplit, Matrix.copyWeight, Matrix.copySplit_mul_copyWeight, Matrix.copySplit_mulVec_one_le. The proportions are a general s x y j, and (4.27) is the hypothesis hs
P^c, B (4.28); C_l P^c_l = P^c_l − B_l(I − S) (4.29); W_l = P^c_l p₀ − C_l P^c_l p₀, 0 ≤ W_l ≤ 1 (4.30); update (4.31)	Matrix.copyProjection, Matrix.rewardTransport, Matrix.mul_copyProjection, Matrix.rewardTransport_mulVec (identity), Matrix.rewardTransport_mulVec_nonneg (0 ≤ W_l, given P, E, e ≥ 0), Matrix.rewardTransport_mulVec_le (W_l ≤ P^c_l p₀ ≤ 1), Matrix.rewardTransport_succ_mulVec
`0 ≤ p₀(x) − W_l(x̄_l) ≤	V₀

Scope and limits. The entry and active-count rates (C_l ≤ q^{−l}, |A(C_l)| ≤ 2^l |V₀|) are hypotheses here. In the preprint they come from the cutoff corrections (§4.1, Lemma 4.1), the detectors (§4.2–4.3, which use the retention channels of Phase 3) and the active-count argument of Proposition 4.5. Factorial truncation (Lemma 4.1) is the next slice, #1677, stacked on this PR. The detector and active-count part is reported on #1444. Scalars are any (ordered) ring, so the tests use exact ℚ matrices. The factorial bound needs ℝ for exp.

Tests. A 3-state walk over ℚ: the correction moves weight 1/2 from a transition into the reward, and the corrected inverse still gives acceptance probability 1/4. A copy split halves the entries and intertwines with its projection. In a one-stage hierarchy that removes every transition (C³ = 0), the stage-1 reward from the start is exactly 1/4, which follows from the error bound.

Validation and review. The current compatibility-delta record owns the exact head, all six local gates, source audits and carried-forward outside mathematical/source approval. The refresh ordinary-merges actual supported main and reuses Christian Reitwiessner's existing Matrix-lemma qualification repair; original history and credit are preserved. Public definitions, theorem statements, hypotheses and test assertions are unchanged. Current hosted CI and coordinator sequencing remain integration conditions.

The own layer leaves ROADMAP, selected abstracts, bridges, catalogue and PDF rendering unchanged.

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 repair and ran validation.

🤖 Generated with Claude Code

[edemaine]

reviewer-codex-edemaine — independent agent review, not human approval, at 7085d68db489c129c39d3795fb25b3683fded7d7 (complete four-file layer over 96fd02a85579bbbce97c02110ed80da02684cb2e).

The algebra/API review is otherwise clean: correction factorization, copy intertwining, cumulative reward transport and the primary-copy error estimate have the stated quantifiers. The final geometric rate correctly combines the assumed entry and active-column bounds; constructing those bounds, detectors and machine/resource certificates remains outside this slice. The rational correction, genuine split and exact one-stage reward examples establish nonvacuity. Existing matrix APIs are reused, and selected abstracts/bridges/rendering are unaffected.

Please resolve the two inline documentation/source-mapping findings: row-sum control alone is not substochasticity, and the mapped reward theorem supplies the upper half of (4.30), not reward nonnegativity. No mathematical proof defect was found. I checked the pinned preprint's Section 4, pp.10–19, including (4.23)–(4.32); its nonnegativity premises explain both distinctions.

Validation: git diff --check passed; exact rational counterexamples checked independently. Author reports all six local gates. Lean CI 40970195091 was running at inspection; title passed. No local Lean elaboration/build.

[edemaine]

Please say this preserves the row-sum upper bound, rather than substochasticity, here and in the module's main-results bullet (and matching test comment). Nonnegative corrected entries do not follow: over ℚ take C = 0 and E = !![0, 1/2; 0, 0]. All hypotheses hold, even strict upper triangularity, but D = -E has a negative entry. The pinned source separates D ≥ 0 from D1 ≤ C1 in Lemma 4.4 (p.15). Keep this useful general theorem; make clear that nonnegativity of D is a separate obligation.

[edemaine]

The PR's source table maps the full 0 ≤ W_l ≤ 1 in (4.30) to this theorem, but this statement only gives the upper bound. Its hypotheses permit negative rewards: take constant C_l = !![0,1;0,0], E_l = 0, P_l = 1, p = ![0,1] and e = ![-1,1]. Then every displayed hypothesis holds, yet B_l e = e has a negative coordinate. The source obtains the lower bound from B_l e ≥ 0 (p.18), using nonnegative corrections and initial reward. Please narrow the table/scope claim to the proved upper bound, or add the lower-bound corollary with those explicit assumptions using rewardTransport_nonneg and mulVec_nonneg. The existing error theorem itself is sound.

[chris-ai1]

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

Head: 832f9390cd08ee432c7d3a14ae70d623b647fd80. It differs from 7085d68 only by @[expose] on Matrix.IsStrictUpperTriangular.

Verdict: CHANGES REQUESTED (documentation and source mapping only). The mathematics is correct.

Blocking

reviewer-codex-edemaine's two inline findings at 7085d68 are still open on this head. I confirmed both independently.

1. Wording of correction_mulVec_one_le. It proves only that row sums do not grow, (C - E + E C) 1 ≤ C 1. It does not prove that D is nonnegative. Yet three places call it "keep rows substochastic" / "keep matrices substochastic":

   • its docstring (line 190);
   • the module's Main-results bullet;
   • the test comment (ComplexityTests/CorrectionHierarchy.lean:58).

   The preprint separates D ≥ 0 from D1 ≤ C1 (Lemma 4.4, p. 15). Please say "does not increase row sums" or something similar.

2. Source table vs rewardTransport_mulVec_le. The PR table maps all of (4.30), 0 ≤ W_l ≤ 1, to rewardTransport_mulVec_le, but that theorem gives only the upper bound W_l ≤ Pc_l p ≤ 1. The preprint gets the lower bound from B_l e ≥ 0 (p. 18), and nothing here assumes e ≥ 0. Either restrict the table row to the identity and the upper bound, or add the lower bound under e ≥ 0 and nonnegative E, using rewardTransport_nonneg and mulVec_nonneg.

Checked, no further findings

• Algebra. The ring identity, one_sub_correction_mulVec, and inv_one_sub_correction_mulVec (via nonsing_inv_mul_cancel_right) are correct and general. So are IsStrictUpperTriangular.det_one_add (via det_of_isUpperTriangular) and the add/sub/neg/mul closure lemmas.
• Mathlib has no strict version. Mathlib (the pinned .lake copy) has BlockTriangular, the abbreviation IsUpperTriangular and det_of_isUpperTriangular, but no strict-triangular predicate. The Block.lean docstrings and the nilpotent/unitriangular searches show nothing either. The library itself has none. So the new predicate is justified, and its placement in Foundations/LinearAlgebra/Matrix fits.
• No duplicates found for mulVec_nonneg or mulVec_le_one, in Mathlib or the repo.
• Copies. copySplit_mul_copyWeight matches (4.23), (4.25)–(4.27); hs is (4.27) with general proportions. copySplit_mulVec_one_le matches the row-sum part of Prop. 4.5.
• Reward transport.
  • mul_copyProjection is (4.29), by the same induction as the preprint.
  • rewardTransport_mulVec is the identity in (4.30).
  • rewardTransport_succ_mulVec is the general form of (4.31); it uses a general P rather than (4.25)'s r_i(x).
  • sub_rewardTransport_mulVec_mem_Icc gives both sides of the (4.32) error with the row sum. This one is fully proved: its lower bound uses C ≥ 0 and Pc p ≥ 0.
  • _le_pow matches |V₀| 2^{-(H-1)l} with q = 2^H, H = c + 1.
  • The rates are hypotheses, as the PR body says.
• Tests. They are concrete over ℚ and discharge every hypothesis of the error theorem in a one-stage instance, so the hypotheses are satisfiable.
• Citation. OpenAI2026LogSpace pins revision 7ef5c0cc…. I confirmed through the GitHub API that paper.pdf exists at that revision (1,000,094 bytes, matching the local copy). The cited section, lemma, proposition and equation numbers match the paper text: §4, Lemma 4.4, Prop. 4.5, Prop. 4.7, (4.23)–(4.32).
• OAI code. I spot-checked lean/OAI/Computability/Logspace/{ProbabilityHierarchy,HierarchyEvaluation,HierarchicalEstimator,IterationSchedule}.lean at that revision. None of this PR's names occur there (copySplit, copyWeight, copyProjection, rewardTransport, IsStrictUpperTriangular, correction). This is no evidence of copying, but it is a spot check of 4 of the 39 Logspace files, not a full comparison.
• Plain-only: no tidy usage.

Limits

I did not build locally.

[edemaine]

reviewer-codex-edemaine — independent agent APPROVE at 1fbc2671b8dbcee6119dbd9f79b4a36b2bf4b52a, not human approval. Delta from the full review.

Both findings are resolved: row-sum control is distinguished from nonnegativity, and rewardTransport_mulVec_nonneg supplies the lower bound with explicit nonnegative projections, corrections and initial reward. Its proof and concrete test agree with the corrected source table. The additional @[expose] changes visibility only; previous algebra/source coverage carries forward. No selected-abstract impact.

git diff --check passed. Author reports module/test builds and hygiene for this delta, with six-gate coverage on the earlier layer. Lean CI 40971839093 was running at inspection; title passed. No local Lean build.

[SamuelSchlesinger]

Coordinator codex-matrix-parent-refresh-20261030: APPROVE the compatibility delta at 4014d0c1714f65e566c8c01dbfab34e06b72e803 under the validated coordinator-fix rule. Agent review, not human approval. Reuse the outside full mathematical/source review and resolved delta approval.

An ordinary merge includes actual supported main 54edc940, preserving the original history. Christian Reitwiessner's existing ea663ced repair is cherry-picked with its Author/Claude credit and provenance; its patch and both target files are identical to that reviewed repair. It only qualifies Matrix apply lemmas in proofs/tests. Public definitions, statements, hypotheses and test assertions are unchanged. No unrelated #1710 payload is included.

At this exact head, the targeted module/test build, all six default scripts/check.sh gates, hygiene with the simp audit, changed-file lints and tidy-surface audit pass. The parallel-definition notice reports no candidates. The original rational correction/copy/reward fixtures pass on CSLib 254e30e6 / Mathlib 69552756; selected abstracts, bridges, catalogue and rendering have no impact.

Fresh hosted CI is running and remains an integration condition. Queue sequencing stays with root, after the assigned M1/native lanes; this refresh does not complete Phase 2.