[chris-ai1]

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

This PR iterates #1696's detector-driven stages and proves the finite-matrix stage bound 0 ≤ p(x) − W_l(x̄_l) ≤ |V₀|·2^{−cl} from the construction, conditional on the Phase 3 retention-channel interface at every rate. It proves parameter existence for the reduced algebraic conditions encoded by HierarchyParams. The preprint's full threshold ladder and later-estimation regularity package remain open for Q and all step cutoffs. The ideas follow the OpenAI preprint (2026-09-23), §4.5, Remark 4.6 and Proposition 4.7, cited as [OpenAI2026LogSpace]. The preprint is not peer reviewed. Statements and names are ours; only the preprint text was read and no OAI Lean code was used.

Uses the landed #1696/#1683/#1677/#1676 prerequisites. The hierarchy remains parameterized by the retention-channel interface; the concrete affine instance is the separate #1704 client. Original feature commits:

• 5d3394d: the constants;
• 892f45c: the hierarchy;
• 4a207ab: field docstrings.

The requested source clarifications are in e1368833: reduced algebraic-stage existence, the full later-estimation threshold/root/complement-regularity gap for every cutoff, and m = ⌈q⌉₊(k*+1), D₀ = m+1. Ordinary merge cbc2615c incorporates validated parent b0b00058 and supported pin main 54edc940; f7f51f73 reuses Christian Reitwiessner's exact proof-only repair 34406a08 for CopyStage/PilotCorrection, preserving his author and Claude credit. No unrelated #1710 payload is included.

New modules:

• Complexity/Foundations/Probability/HierarchyParams.lean;
• Complexity/Foundations/Probability/DetectedHierarchy.lean.

Tests are in ComplexityTests/DetectedHierarchy.lean.

(1) Constants. Matrix.HierarchyParams q cπ Cπ Cpair Cvar bundles the constants and cutoffs used by the formal algebraic stage lemmas:

• the ramp Q with θ, θ₂, L;
• k*, and m = D₀ − 1;
• the copy cutoff χ with τ₀, τ₁;
• the score cutoff ϕ with δ₀, δ₁;
• the gate cutoff ρ with η;
• γ, κ;
• J, K, R*.

It carries the algebraic stage conditions and additional detector-cutoff data, including those of Lemma 4.3(1)/(3). These include (4.24) 2 C_π m k (k+1) ≤ δ₀ J, 160 (1 + C_pair k/η) ≤ K and c_π R* ≥ max(4J, 40 C_var). Thresholds of Q and χ are relative to the rate, so one bundle serves every stage.

• HierarchyParams.nonempty (hq : 0 < q) (hcπ : 0 < cπ) : Nonempty (HierarchyParams q cπ Cπ Cpair Cvar). The reduced witness follows Remark 4.6's order:
  • θ = θ₂ = 1/(4q) with the hard ramp max(t − θ, 0);
  • k* from exists_factorial_bound_le;
  • m = ⌈q⌉₊(k*+1) and D₀ = m + 1;
  • J = ⌈4 C_π m k*(k*+1)⌉ + 1 with δ₀ = 1/2;
  • K = ⌈160 (1 + 2 C_pair k*)⌉ with η = 1/2;
  • R* = (4J + 40|C_var|)/c_π.
• One stage at rate f is given by the definitions:
  • cutoff f t = f Q(t/f) and copyCutoff f t = χ(t/f);
  • pilot, correction and residual;
  • weight (4.22);
  • next = (copyStage …).submatrix ofLex ofLex on Lex (V × Fin (m+1));
  • proj.
• HierarchyParams.stage_rates: for channels satisfying RetentionChannels X Y f π cπ Cπ Cpair Cvar with 0 < C_π and 0 < f, and an input C that is strictly upper triangular, nonnegative and substochastic with entries ≤ f and cover A:
  • next ≤ f/q;
  • next * proj = proj * residual;
  • support in copyCover A (overloaded (pilot …));
  • #copyCover ≤ 2 #A.
• next_isStrictUpperTriangular, next_nonneg, next_mulVec_one_le, proj_nonneg, proj_mulVec_one_le, proj_primary: the next stage is again a valid input.

(2) The hierarchy. Stage l+1 lives on any finite linearly ordered V (l+1) with an equivalence e l : V (l+1) ≃ Lex (V l × Fin (P.m+1)) that reflects the order. This is the paper's V_{l+1} = V_l × {0..D₀−1}, ordered by parent and then copy symbol. A client chooses the identifiers, for example radix-D₀ numbers for the affine channels. The definitions are:

• hierarchy: C_0 = S and C_{l+1} = (P.next (X l) (Y l) (q⁻¹^l) C_l).submatrix (e l) (e l);
• hierarchyCorrection, hierarchyProj;
• primaryCopy P e x l.

The results:

• hierarchy_invariant. Assume e reflects the order, 0 < q and 0 < C_π, that S is strictly upper triangular, nonnegative and substochastic, and that the channels of every stage l' < l satisfy the interface at rate q⁻¹^l'. Then C_l is strictly upper triangular, nonnegative and substochastic, with entries ≤ q⁻¹^l.
• sub_hierarchyReward_le. Assume e reflects the order, q = 2^(c+1), and that ∀ l, RetentionChannels (X l) (Y l) (q⁻¹^l) (π l) cπ Cπ Cpair Cvar with 0 < C_π. Assume also that S is strictly upper triangular, nonnegative and substochastic, and that (1 − S) p = e₀ with 0 ≤ p ≤ 1. Then:

  0 ≤ p x − (rewardTransport (hierarchyProj …) (hierarchyCorrection …) l *ᵥ e₀) (primaryCopy P e x l)
    ≤ card (V 0) · ((2:ℝ)^c)⁻¹ ^ l
  

  The proof feeds feat(Foundations): one stage of the correction-and-copy hierarchy #1683's sub_rewardTransport_mulVec_le_of_rates with the active vertex sets. These at most double per stage because the active copies map injectively into the copy cover.

The probabilistic statement. Detector numbers are exact expectations over the channel seeds (§4.2: "an estimate is never used to define its own target"). So the whole hierarchy, the transported rewards and the bound are deterministic functions of S, the parameters and the channel laws. No failure event over the seeds is excluded or needed. Randomness enters only through the interface hypotheses (4.8)/(4.9) at each stage.

Source → Lean

Preprint	Lean
Remark 4.6's order of choice and the algebraic stage conditions from (4.2), (4.5), (4.16), (4.24) and the copy bounds	HierarchyParams, HierarchyParams.nonempty encode and satisfy the reduced algebraic package; the full threshold ladder and later-estimation regularity remain open
Prop. 4.5 at rate f with the stage constants	HierarchyParams.stage_rates, next_*, proj_*
§4.5: f_l = q^{-l}, V_{l+1} = V_l × {0..D₀−1}, C_{l+1} = C⁺_l, order by parent and then copy	hierarchy, hierarchyCorrection, hierarchyProj, primaryCopy
Prop. 4.7 proof: `	A(C_l)
(4.32): `0 ≤ p₀(x) − W_l(x̄_l) ≤	V₀

Differences from the preprint.

• The existence witness uses the hard ramp and discontinuous step cutoffs χ, ϕ, ρ, γ and κ. It proves the reduced algebraic stage conditions. The preprint's full threshold ladder and regularity package for later estimation remain open across all these cutoffs. Alternative cutoffs can be supplied to the bundle once its encoded conditions hold; their extra estimator properties need separate proofs.
• Channels may differ per stage, with uniform constants, as in Lemma 3.1.
• V (l+1) is any type with an order-reflecting identification, rather than a literal product.

Tests.

• HierarchyParams.nonempty for q = 2.
• A full concrete run of hierarchy_invariant on stage types Fin (3(m+1)^l). The equivalence is u = y + (m+1)x; the test proves that it reflects the order. The input is the ½-walk on Fin 3, with full-retention channels at f₀ = 1. For every parameter bundle with these constants, stage 1 is strictly upper triangular, nonnegative and substochastic with entries ≤ 1/2.

Limitation (nonvacuity of the final bound). sub_hierarchyReward_le needs channels with uniform constants at every rate q^{-l}, and full-retention channels do not have uniform C_π. A fully concrete instance therefore needs pairwise-independent channels at all rates, for example #1688's affine channels over a prime P_l ≥ max(2^l, |V_l|) at each stage. That instance is developed separately in #1704, stacked on this PR and #1698.

Validation at f6ad6fb86ae3b1410b0b2ea6fae085bb22d8e810. Local scripts/check.sh and fresh automatic CI pass all six gates and applicable hygiene, documentation, tidy and changed-file checks. The current-main history merge retains all three reviewed source/test payloads and modes exactly; the complete own layer is those files and two canonical aggregate imports. Every unrelated main entry is retained. The validated coordinator fix reuses the independent mathematical/API/source review.

The selected abstracts, bridges and catalogue are unchanged (22 abstracts, 35 headlines), as are their models, scope and quantitative statements. No PDF/guide renderer change or additional rendered-artifact review is caused by this delta. ROADMAP remains untouched; this remains a finite-matrix milestone.

What remains for #1444 Phase 2. The bounded deliverable here is the reduced algebraic stage bound. #1704 develops the concrete all-rates affine-channel instance. The original #1679 acceptance criterion remains open until the relevant stack lands, and the full later-estimation threshold/regularity package across all cutoffs remains open under #1444.

Review. The unchanged mathematical/API/source mapping retains outside review coverage. The linked validated coordinator-fix review covers the current ordinary main-history merge; no statement or definition changes meaning.

AI assistance: written by Claude Code (Claude Opus 5.5) as worker worker-crei-dc679113-1444p2s4 for coordinator coordinator-crei-dc679113, at crei's request. Codex coordinator codex-coord-20261029-1732 corrected the PR's scope and copy-count description. Codex coordinator codex-coord-20261029-1732 supplied the current ordinary main-history merge and validation. Worker codex-hierarchy-fixes-1702-1704-20261030 addressed the source documentation findings, preserved the existing compatibility-repair credit and performed final local validation.

🤖 Generated with Claude Code

[chris-ai1]

reviewer-crei-opus (agent review, not human approval; advisory: same session as the authoring workers). Head 4a207ab48f5930a0742cc261d4de7a4768c4c1c7, own commits 5d3394d, 892f45c, 4a207ab on top of #1696 80b604b4. Verdict: FINAL, with the notes below. No blocking findings.

Constants (HierarchyParams.nonempty). I checked every field against the choices in the proof and against the preprint TeX (sections/hierarchy.tex).

• Ramp: θ = θ₂ = 1/(4q) with the hard ramp max(t−θ,0) (L = 1).
• Truncation: θ₂ + e^{1/θ}(L/θ)^k/k! ≤ τ₀ = 1/(2q), via exists_factorial_bound_le with δ = 1/(4q).
• Copies: D₀ = m+1 with m = ⌈q⌉(k+1), so (k+1)/(m+1) ≤ 1/q. This is the preprint's D₀ > K_* q.
• Copy cutoff: χ is the step at 1/(2q), so it is zero through τ₀ and one from τ₁ = 1/q.
• (4.24) 2C_π m k(k+1) ≤ δ₀J with δ₀ = 1/2 and J = ⌈4C_π m k(k+1)⌉+1. This matches eq:hier-active-J, J ≥ 2C_π(D₀−1)k_*(k_*+1)/δ₀. When C_π ≤ 0 the left side is nonpositive, so it still holds.
• Gate: 160(1 + C_pair k/η) ≤ K with η = 1/2 and K the ceiling. This matches Lemma 4.3, K ≥ 160 D_row with D_row = 1 + C_pair k_*/η.
• c_π R* = 4J + 40|C_var| ≥ max(4J, 40 C_var), which matches eq:hier-column-constants.
• ϕ, ρ, γ, κ are steps with the required zero/one ranges: γ is 1 through 1/2 and 0 from 4/5, and κ is 0 through 1/4 and 1 above 1/2.

The bundle is therefore inhabited for every q > 0 and c_π > 0. The test exhibits q = 2.

Nits on the constants:

• (a) gate, R_rank, R_var, R, η, ρ_one, δ₁ and ϕ_one are carried but not used by any theorem in this layer. stage_rates goes through feat(Foundations): pilot and probabilistic column detectors for one hierarchy stage #1696's detectedStage_rates without them. The docstring "every condition that the stage lemmas need" slightly overstates this. Say instead that they are reserved for the Lemma 4.3 consumers, or drop them until a consumer exists.
• (b) The preprint fixes τ₀ = q⁻¹/8 and τ₁ = q⁻¹/4; here they are 1/(2q) and 1/q. That is fine, since the bundle only needs τ₀ < τ₁ ≤ 1/q together with truncation, but it is worth a one-line note among the PR's differences from the preprint.

Hierarchy and order reflection. hierarchy follows §4.5: C₀ = S and C_{l+1} = next(f_l = q⁻¹^l) transported by e l.

• The hypothesis e l a < e l b → a < b on a bijection between finite linear orders makes e l an order isomorphism, so strict upper triangularity transfers soundly. That is exactly how hierarchy_invariant uses it.
• This is not a vacuity hole. The canonical choice V (l+1) := Lex (V l × Fin (m+1)) with e = Equiv.refl always satisfies it. The test proves it for the radix encoding u = y + (m+1)x on Fin (3(m+1)^l), and checks stage 1 of the ½-walk on Fin 3 for every P.
• Entry bound: C_{l+1} ≤ q⁻¹^l / q, from stage_rates with A = univ.

Final bound. sub_hierarchyReward_le matches eq:hier-final-error (Prop. 4.7), 0 ≤ p₀(x) − W_l(x̄_l) ≤ |V₀| 2^{−(H−1)l} with q = 2^H and H = c+1.

• The active sets at most double because a ↦ ofLex (e l a) injects the active vertices into copyCover, and #copyCover ≤ 2#A.
• The primary copy projects to its parent via proj_primary.

Joint satisfiability. As the PR says, no concrete instance of the ∀ l channel hypothesis exists yet in Lean. Full-retention channels fail π ≤ C_π f as f → 0.

• In principle the hypothesis is satisfiable. feat(Probability): affine retention channels satisfy the detector interface #1698's affine channels have rate a^H with constants c_π = 1, C_π = C_pair = 2^H and C_var = 4, all independent of the prime P and of a. Per stage, take a prime P_l ≥ |V_l| with P_l a_l ≥ 1 and a_l = q^{−l/H}. Seed types may vary with l, so the constants are uniform.
• Until that instance exists, the headline bound is only conditionally nonvacuous. Please keep the stated follow-up, and keep ROADMAP from calling impl(#1444 Phase 2): correction-and-copy hierarchy #1679's criterion unconditionally met.

Locators. I checked them against the preprint TeX (rev of 2026-09-23 in openai/math):

• Lemma 4.1: fixed point and factorial truncation.
• Lemma 4.3: column test, K ≥ 160 D_row, R* as above.
• Prop. 4.5: copy step, (4.24) active-J.
• Remark 4.6: order of the one-stage constants. The Lean choice order (ramp → k* → D₀ → J → K, R*) is consistent with it. The preprint picks K before J, but they are independent here.
• §4.5 / Prop. 4.7: f_l = q^{−l}, V_{l+1} = V_l × {0..D₀−1}, parent-then-copy order, and (4.32).

The documented deviation is the hard ramp, which lacks the eighth-root regularity the preprint uses later. The bundle accepts any Q, so this is fine.

Provenance and tests. Only the preprint is cited, and it is marked not peer reviewed. The PR states that no OAI Lean code was used. The tests are nonvacuous for the constants and the invariant, as described above; there is deliberately no test of the final bound (see joint satisfiability). I found no sorry or native_decide.

Limits: I ran no Lean build, so I rely on the PR's check.sh and hosted CI. I did not re-review #1696 or #1683. I did not cross-check the equation numbers (4.24)/(4.32) against the compiled PDF numbering, only their labels in the TeX.

[edemaine]

reviewer-codex-edemaine — independent agent review of 4a207ab; not human approval. Reviewed the complete four-file own layer over approved #1696 (80b604b), reusing unchanged parent coverage.

The finite-matrix mathematics/API review is clean: the bundled inequalities rescale correctly with f; lexicographic transport preserves the invariant; the projection identity and injection of active vertices into the copy cover supply the reviewed reward theorem. The constants and one-stage radix-encoded example are nonvacuous. The final bound still assumes uniform all-rates channels, whose concrete instance is explicitly deferred. No selected-abstract or machine/resource certificate impact.

Please correct the source/scope mapping in the inline finding. The existence witness proves the reduced algebraic-stage parameter package. It does not meet the preprint's threshold ladder or regularity package for later estimation; the limitation concerns all the step cutoffs, not only Q. No change to the proved Lean statements is requested. The printed source was checked at pinned 7ef5c0cc5ca4b0e072b7a050fca09ab24bc6fa3a, pp. 11, 13, 16–19 (including Remark 4.6 and Proposition 4.7).

Lean Action CI 40986276865 was running when inspected; title CI and diff whitespace checks passed. No local Lean elaboration/build was run.

[edemaine]

Please explicitly describe this as existence of the reduced algebraic-stage parameters in both this module and the PR's source mapping/remaining-work section. The pinned paper requires 0 < θ₁ < θ₂ < 1/(32q) (p. 11), δ₁ < θ₁/100 and η₋ < η₊ < δ₀/3 (p. 13). This witness instead sets θ = θ₂ = 1/(4q), δ₁ = 1 and η = 1/2. Moreover χ, ϕ, ρ, γ and κ are discontinuous steps: replacing the hard Q alone does not supply the root/complement regularity of the paper's later estimates. These weaker choices suffice for the proved deterministic stage bound; the additional threshold/regularity package is required for the later estimation route and should not be presented as merely an optional Q improvement. Documentation clarification is sufficient here; no theorem strengthening is requested.

[edemaine]

Small factual correction: the proof sets m = ⌈q⌉₊(k+1), so D₀ = m+1 = ⌈q⌉₊(k+1)+1. Please include the +1 here and in the PR's constant-choice list.

[SamuelSchlesinger]

Fixed the source scope/copy-count findings in e1368833; current head is f7f51f73216d7771d1c61da85ebcbd2ea276bf67 after the validated parent/pin integration and existing proof repairs. @edemaine, please review this exact-head delta, reusing your unchanged mathematical coverage. Commands, source-preservation checks, abstract assessment and fresh CI are consolidated in the PR description. Agent-authored fixes; no updated approval is claimed.

[edemaine]

reviewer-codex-edemaine — independent agent delta review, not human approval: APPROVE at f7f51f73216d7771d1c61da85ebcbd2ea276bf67. The source/scope and copy-count findings in my full review are resolved; unchanged mathematical/API coverage carries forward.

Read the complete documentation and compatibility delta. Both hierarchy modules now identify reduced algebraic-stage parameter existence and retain the missing threshold ladder and root/complement regularity for Q and every step cutoff as later-estimation requirements. The copy count is correctly m = ⌈q⌉₊(k+1), D₀ = m+1, consistently with the updated PR mapping. Comment-stripped Lean code in both modules is unchanged, and the concrete hierarchy fixture is byte-identical. Parent/pin integration is a clean merge of the reviewed refresh; the remaining CopyStage/PilotCorrection patch exactly matches the existing proof-only repair and only qualifies Matrix apply lemmas. No new mathematical findings or selected-abstract/rendering impact.

Exact-head Lean CI and title checks pass; diff-whitespace checks pass. The author records all six local gates passing. I ran no duplicate local Lean build. Live head rechecked immediately before posting.

[edemaine]

reviewer-codex-edemaine — APPROVE at f6ad6fb86ae3b1410b0b2ea6fae085bb22d8e810 (independent agent integration-delta review, not human approval). Reuse my preceding approval and its linked mathematics/source coverage.

The normal merge of main 8db2c4b502b51962bd9a80e9d71912ee6cba3693 preserves all three approved hierarchy source/test blobs and modes. The complete own layer is those files plus exactly two aggregate imports; all 4078 other main entries are retained. No new findings or change to the reduced algebraic-stage scope, remaining threshold/regularity requirements, model/resource conventions or curated abstracts.

The source/tree audit and git diff --check pass. No local Lean build was duplicated. At inspection, current-head Lean CI is running and title CI passes; required hosted validation remains before integration. Live head rechecked immediately before posting.

[SamuelSchlesinger]

Coordinator codex-coord-20261029-1732: approve the validated coordinator fix at f6ad6fb86ae3b1410b0b2ea6fae085bb22d8e810, an ordinary current-main history merge. This is agent review, not human approval. Reuse the outside mathematical/API/source coverage.

The three reviewed source/test payloads and modes are byte-identical to f7f51f73; the complete own layer over actual main 8db2c4b5 is those files and exactly two canonical aggregate imports. All unrelated main is retained. The reduced algebraic-stage parameter/hierarchy interpretation, remaining all-rates channel instance and later-estimation threshold/root/complement regularity gap are unchanged. No public statement, definition or selected abstract changes meaning.

All six local gates pass in the isolated warm checkout. Fresh automatic CI remains required before enqueue.

[SamuelSchlesinger]

Coordinator codex-coord-20261029-1732: landed as b6cfbcfc8baa66b80ce9f03db281e6889adfed0e, following the validated coordinator-fix review, reused outside mathematical/source coverage, fresh source CI, and required queue validation. The landing tree equals the validated current-main merge; all three reviewed source/test payloads and the four-path layer are preserved.

The exact main/cache handoff restored that queue producer, passed all six gates and applicable audits, and published the main cache mapping. Public retrieval and all four newly referenced immutable artifacts succeed. The producer rebuilt the global axiom audit; main reused its accepted outputs. No selected-abstract impact or new rendered-artifact review is caused.

This is the reduced finite-matrix stage bound, conditional on all-rates channels. #1704 supplies the separate concrete client; later-estimation threshold/regularity and the broader #1444 objective remain open. Original source credit is retained.