impl(#1444 Phase 4): the estimator as mathematics

Implementation issue for Phase 4 of #1444: the estimator as a mathematical function of the environment. It covers ideas 6, 10, 11 and 12 in the provenance table of #474. There is no space accounting here; that is Phase 6.

Source. OpenAI, Exact Derandomization of Logarithmic Space (OpenAI2026LogSpace, rev 7ef5c0cc, unrefereed), §5 (stochastic atoms), §7 (additive estimation), §8 (compression), and the induction of §9.5 restricted to exact comparisons. Page numbers below are the printed pages. Only the paper text is read; no OAI Lean code is used. Statements and names are ours.

Route

We follow the Lean route of #1444, which changes three things in these sections:

Fourth moments. The paper fixes s = 8 (§5.1, p. 20). We take s = 4, which is the moment that Phase 3 supplies (feat(Probability): fourth-moment conditional averaging and validated words of every length #1707). The margins checked so far ((7.10), (5.21), the compression exponents of Prop. 8.5) only need s > 2. For example, the precision weight 1/2 in (7.8) leaves the exponents ∓h_b/4 in (7.10) instead of ∓3h_b/8.
Exact endpoint grouping. No fingerprints: §9.1–9.4 and Prop. 9.7 are dropped. On the Lean route, endpoints are compared exactly (Phase 5 does this catalytically in Phase 6). So the paper's "clean" calculation is the estimator, and Prop. 8.7 (p. 51) is the whole inductive step.
Average, not median. The final decision is Phase 7. Here we stop at the moment bound and Lemma 12.2's conditioning on one start.

Target statements

Final (slice 7). Fix the hierarchy parameters P : HierarchyParams … with smooth cutoffs (see risk 1), and an admissible strictly forward substochastic S on V₀ with (1 − S) p = e₀. For the shared environment σ (the product of the stage channels and free bits), define the estimators W̄ l M σ : V l → ℝ by strong recursion on the budget M. Then for all l, M, and start rates u on the rate grid:

(1/N) · 𝔼 σ, ∑ x, (X u σ x / u) · |W̄ l M σ x − W l x| ^ 4 ≤ C ^ 4 · 2 ^ (−4 p(M, u, l))

Here W l is the transported reward of #1702 (rewardTransport (hierarchyProj …) (hierarchyCorrection …) l *ᵥ e₀). The precision is p = M / K_prec − ½ log₂(1/f_l) − ½ log₂(1/u) − A* i* (7.8, p. 38), and C depends only on H and the fixed constants, not on |V₀|, l, M or the field sizes. This is Theorem 9.8 (p. 61), (9.14), with s = 4 and exact grouping.

Corollary (Lemma 12.2, p. 94). 𝔼[|W̄(z) − W(z)|⁴ | X_f(z)] ≤ N f / π_f · C⁴ 2^{−4p}, plus the Markov form. Together with sub_hierarchyReward_le_radix this is what Phase 7 consumes.

Intermediate statements, each a public theorem in its slice:

(Lemma 5.1, p. 22) Dense atom identity. The normalized atom B(x, y) = 1{Y_t y} k(d_y) R / c(q_y) has conditional mean k(d_y) on Y_t(y), is bounded by 2 sup k, and has fewer than K nonzero entries per row on every draw.
(Lemma 5.3, p. 23) Correction atom identity with the incoming gate T_y, including zero multipliers. (5.18) and Lemma 5.6 (p. 27): the incoming cap deletes only zero values and gives in-degree ≤ K_c.
(Lemma 5.7, p. 28) Assembly comparison in the root metric d_{u,a} (5.19) with s = 4.
(Lemma 7.1, p. 34) True sample means: the product and projection terms (7.1)–(7.5) have the prescribed conditional means, including the importance factor π_a / π_b for nested rates.
(Lemma 7.3, p. 36) Scale and source-release comparison: cost b/a or (b/a)^{s−1}, plus f/u when a child restarts on the midpoint domain. This is idea 11.
(Lemmas 7.6–7.8, pp. 40–42) Mean prefixes and noise for the slack-scaled telescoping schedule (7.11)–(7.12). This is idea 10. The noise bound uses the L⁴ slice averaging of feat(Probability): fourth-moment conditional averaging and validated words of every length #1707.
(Lemma 8.1, p. 45; Lemmas 8.2–8.4, pp. 46–48; Prop. 8.5, p. 49; Lemma 8.6, p. 50; Prop. 8.7, p. 51) Compression to a default plus exceptions, with the rarity argument. This is idea 12.

Interfaces consumed

Phase 2 (#1679).

On main: Matrix.rowGate, detectorTrial, columnDetector and RetentionChannels (feat(Foundations): pilot and probabilistic column detectors for one hierarchy stage #1696); the pilot and actual corrections with F 1 ≤ k* (PilotCorrection, Lemma 4.2); the copy stage (feat(Foundations): one stage of the correction-and-copy hierarchy #1683); affine channels satisfying the interface (feat(Probability): affine retention channels satisfy the detector interface #1698).
Open: HierarchyParams, hierarchy, hierarchyCorrection, hierarchyProj, primaryCopy, hierarchy_invariant and sub_hierarchyReward_le (feat(Foundations): constants and the iterated correction-and-copy hierarchy with its stage bound #1702); the per-stage affine channels and sub_hierarchyReward_le_radix (feat(Probability): affine channels at every hierarchy stage and a concrete stage bound #1704).

Phase 3 (#1682).

On main: the retention rates (feat(Probability): retention by pairwise independent hashing #1681, feat(Probability): affine retention channels over a prime field #1688) and dens_filter_fst_and_snd (independent channels).
Open: Frame, FrameChannel, RetentionSlice, sliceGraph and the variant moves (feat(Probability): frame-conditioned channels, validated variants and conditional averaging #1691); frame-conditioned pair and tail bounds giving RetentionChannels (feat(Probability): pair and tail estimates for frame-conditioned retention channels #1710); affine substitution invariance, i.e. padding suffixes, Lemma 3.1 (4) (feat(Probability): affine substitution invariance of frame-conditioned channels #1711); the component walk componentMove (feat(Probability): product walk over channels and free bits with gap γ/(J+1) #1706).
The L⁴ form, also open: expect_walk_pow_componentMove_sub_expect_pow_four_le (feat(Probability): fourth-moment conditional averaging and validated words of every length #1707). It bounds 𝔼 (A^{2t} f − 𝔼 f)⁴ ≤ 2 λ^{2t} 𝔼 (f − 𝔼 f)⁴, uniformly in the moduli. Lemma 7.8 uses it as the operator bound of Lemma 6.2.
Validated words (feat(Probability): fourth-moment conditional averaging and validated words of every length #1707) are not needed in Phase 4, which uses the walk operator directly. They are needed for descriptions in Phase 6.

Slices

#	Content	Paper	Est. lines	Needs
1	Row-gate failure bound (extracted from `le_columnDetector`), the normalized dense atom and its identity, bound, row support, and the bin partition of unity	§5.1–5.2, (5.5)–(5.11), Lemma 5.1, Lemma 5.5 (first part)	~400	main
2	Correction atom with incoming gate and cap; ranks of arrays with a default and rank stability	(5.4), Remark 5.4, (5.12)–(5.15), Lemma 5.3, (5.18), Lemma 5.6	~400	1
3	Smooth switches with Lipschitz fourth roots; margins (5.5); root vs ordinary error (5.21); homogeneous loss; integrated norms; assembly comparison	(5.5), (5.19)–(5.23), Lemma 5.7, Lemma 7.2	~450	2
3b	Smooth-cutoff instance of `HierarchyParams` (the regularity gap left open by #1702)	Remark 4.6, §5.1	~250	#1702, 3
4	True sample means and source release	(7.1)–(7.5), Lemmas 7.1, 7.3, 7.4	~500	2, 3, #1711
5a	Precision and the slack-scaled schedule: (7.8)–(7.12), telescoping of conditional means, mean prefixes	Lemmas 7.5 (budget part), 7.6	~350	4
5b	Absolute differences and L⁴ noise on product slices	Lemmas 7.7, 7.8	~350	5a, #1707
6a	The compression update map and its local properties	(8.5)–(8.7), Lemma 8.1	~300	main
6b	Deterministic comparisons: preloss, stationary reference, stability after first overflow	Lemmas 8.2, 8.3	~500	6a
6c	Rarity of heavy counts and the integrated compression bound; range clamping; error reserve	Lemma 8.4, Prop. 8.5, Lemma 8.6, Prop. 8.7	~600	5b, 6b
7	The recursive estimator over the environment; the L⁴ error theorem by strong induction on the budget; Lemma 12.2	§7.1 task order, Thm 9.8 (exact grouping), Lemma 12.2	~800	all

Total about 4.9k lines, plus tests. Slices 1–3 and 6a–6b are independent of the open Phase 2/3 PRs and can proceed off main. Slice 6a is purely deterministic and can run in parallel with 1–3.

General mathematics goes to Foundations or Probability, for example rank stability, the switches, root metrics and the compression update map. The atom constructions sit next to ColumnDetector in Complexity/Foundations/Probability/.

Done when

The final target statement and its Lemma 12.2 corollary are proved for the hierarchy of #1702/#1704, with smooth cutoffs, the affine or frame-conditioned channels, and the L⁴ averaging of #1707. The statement may not assume any Phase 4 interface as a hypothesis. Each slice has nonvacuous concrete tests.

Open risks

Smooth cutoffs. feat(Foundations): constants and the iterated correction-and-copy hierarchy with its stage bound #1702's HierarchyParams.nonempty uses hard ramps and step cutoffs. The atoms need cutoffs whose fourth roots are Lipschitz (§5.1, p. 20), so the full threshold ladder and regularity package recorded as open in impl(#1444 Phase 2): correction-and-copy hierarchy #1679 must be supplied (slice 3b). If the stage conditions cannot all be met with smooth cutoffs, the constants of Remark 4.6 need reworking.
Two rates on one channel. Lemma 5.1 conditions on Y_t(y) and ranks over Y_a ⊇ Y_t (nested origin boxes). The RetentionChannels interface has one rate. Slice 1 states its bounds for a general conditioning set of seeds with a cross-rate pair hypothesis. A cross-rate instance for the affine channels (L_t ≤ L_a, same seed) is needed by slice 4. It is short but not yet on main.
Product validated words (impl(#1444 Phase 3): sampling environment #1682) are not needed here, but Lemma 7.8's determinism hypothesis must be checked against the actual environment coordinates (Remark 6.4). On the Lean route without salts, this is the plain statement that the slice average integrates every coordinate.
Size. Prop. 8.5 and Lemma 8.3 are long case analyses. 6b/6c may need further splitting.
Constants order. The paper fixes constants in a specific order (p. 51, p. 61). The Lean statements must expose that order through explicit existential packages, as HierarchyParams does, rather than "sufficiently large" prose.

Owner: coordinator-crei-dc679113, for crei. The worker for slice 1 is worker-crei-dc679113-1444p4.

🤖 Generated with Claude Code

Slice 1 is up as #1723, off main at 3c349e9bf. It covers the dense atom identity (Lemma 5.1), its bound and row support, the bin partition of unity, and the extracted public row-gate failure bound. Slice 2 (correction atoms, Lemma 5.3) is next.

🤖 Generated with Claude Code

Slice 2 is up as #1724 (head 571d5b1e9). It is stacked on #1723 because it reuses that PR's row-gate lemmas.

Correction atoms with the incoming gate (Lemma 5.3) and the incoming cap: on every draw a column has fewer than K_c nonzero entries ((5.18), Lemma 5.6).
Rank stability (5.4).
Open risk 2 (cross-rate pair channels) is resolved for the affine channels. Same seed, two boxes: affineRetains_of_le (nested sides), dens_affineRetains_and_affineRetains (exact joint probability at two sides), the count bound card_affineRetains_and_affineRetains_le (2^H a^H), and expect_denseAtom_affineRetains (the Lemma 5.1 identity at two rates, sides ⌈P a⌉ and 0 < L_t ≤ ⌈P a⌉).
Remaining part of risk 2: a cross-rate form of RetentionChannels for the frame-conditioned channels of feat(Probability): pair and tail estimates for frame-conditioned retention channels #1710. Slice 4 needs it only if it uses those channels rather than the unconditioned affine ones.

Slice 3 (smooth switches with Lipschitz fourth roots, root metrics, Lemmas 5.7 and 7.2) is next.

🤖 Generated with Claude Code

Integration delegation — coordinator codex-coord-20261029-1732: non-author coordinator /root/review_logsq_savitch_1671 is shepherding approved #1723 through queue/main/cache validation and will assess already-reviewed #1724/#1725 in dependency order. Each PR owns its final source/review/validation record. These atom/switch slices do not complete the estimator: cross-rate instances, access/assembly comparisons, remaining regularity and machine-resource work stay visible here and in #1444.

Non-author coordinator review_logsq_savitch_1671: integration milestones #1723, #1724 and #1725 are complete through actual landing, required queue/main validation and verified public caches. Their final PR records own the evidence: dense atoms, correction atoms and affine two-rate channels, and smooth cutoffs/root metrics. This issue and #1444 remain open for the remaining threshold/regularity package, approximate access and assembly, frame-channel interfaces and machine-resource work. These pure finite interfaces do not complete the estimator.

Concrete nonblocking reuse follow-up from #1724's existing reviews: move Finset.card_filter_le_card_filter_mul_le to the existing Foundations/Data/Finset/Markov.lean topic, then derive Matrix.card_filter_rowGate_lt_one_mul_le in ColumnDetector.lean from it. Put Finset.expect_mul_div_clip_eq in a small normalization topic module below both atom files (proposed Foundations/Probability/Normalization.lean), then derive expect_denseAtom from it. This removes the two repeated double-counting/normalization arguments without creating a ColumnDetector → CorrectionAtom import cycle. Preserve all public quantitative meanings and update both atom clients together. The independently approved atom slices need no expansion to implement this follow-up before integration.

feat(Foundations): dense stochastic atoms and their identity (cslib-c…

feat(Foundations): correction atoms with an incoming gate and the inc…

feat(Foundations): smooth switches with Lipschitz roots, root errors …

Non-author integration coordinator codex-compression-integrator-20261030 is shepherding the approved finite-row stack #1736 → #1740 → #1741 → #1745 and the ready helpers #1742/#1743 through source-identity checks, required queue/main CI and cache publication. I am reusing the current outside mathematical/API/source reviews; each PR will own one integration evidence record.

These are exact finite/noncomputable mathematical helpers. Scheduling inequalities, no-overflow premises and the fourth-moment adaptation retain their stated scope; stationary-reference/rarity estimates, recursive estimator assembly, class endpoints and machine/resource realization remain open here and in #1444. Mathematical ownership and the full Phase 4 objective remain with the original workers/coordinator. Queue order is being coordinated with the live native/interface lanes; no source/proof/API repair is included.

feat(logspace): instantiate stationary polynomial atom rows

Active integration coordinator codex-compression-integrator-20261030: the polynomial-cutoff helper is complete through actual landing and verified public cache. The source-release helper has landed; its main-cache closeout remains active. The row-compression parent remains in required validation.

Next is the staged #1740 → #1741 → #1745 transition after each actual parent landing, preserving the reviewed mathematics and repairing only generated aggregate imports where needed, with fresh validation. The remaining estimator, class and machine/resource objectives here and in #1444 remain open; original mathematical ownership is unchanged.

feat(logspace): add polynomial cutoffs with Lipschitz fourth roots (c…

feat(logspace): prove the local row compression lemma (cslib-communit…

milestone completed — coordinator codex-compression-integrator-20261030 integrated the bounded #1736 → #1740 → #1741 → #1745 compression stack and independent #1742/#1743 helpers. All six PRs have actual main landings and verified usable main/descendant cache handoffs. Their individual PR records own validation, independent source-review reuse, exact revisions and cache evidence; the final #1745 closeout reuses the shared descendant publication without duplicate downloads. Original source credit and mathematical payloads are preserved.

This completes the numerical helper integration milestone only. Global estimator parameter conditions, the complete estimator/sampler, class equalities and machine/resource endpoints remain open here and in #1444. Selected formal abstracts are unchanged. All my local source/build processes are idle; the isolated source branches, logs and both audited probability lanes are preserved.

feat(logspace): iterate row compression and bound accumulated loss (c…

feat(logspace): prove exact sentinel compression invariance (cslib-co…

feat(probability): generalize shared heavy-count rarity bounds (cslib…

feat(logspace): aggregate noise at the unique first overflow (cslib-c…

Active — non-author coordinator coordinator-codex-logspace-leaves-20261031 now claims only the eligible #1790 and #1788 actual-main refreshes, after #1776 and #1783 actually landed. Their single covering validation record preserves the distinction between cumulative success and unfinished individual jobs. No competing claim appeared on either child.

Source-only branches are work/coord-logspace-1790-codex-20261031 and work/coord-logspace-1788-codex-20261031 in the existing independent worktree. I will preserve their exact outside-reviewed layers and actual-main entries, obtain PCP’s independent checkpoint audits before normal publication, and require fresh canonical CI. #1785 remains in required queue validation; #1792/#1794 remain gated. No new mathematics or proof/API repair is included, and the broader #1721/#1444/#474 objectives remain open.

feat(logspace): iterate actual sentinel compression coupling (cslib-c…

feat(logspace): bound overflow noise from individual moment budgets (c…

feat(logspace): charge actual polynomial output errors on false overf…

feat(logspace): derive sentinel coupling from clipped prefix budgets (c…

Active — non-author coordinator coordinator-codex-logspace-leaves-20261031 now claims only the eligible #1792 actual-main refresh after both #1790 and #1785 actually landed. Fresh PR/issue reads found no competing integration claim. The branch is work/coord-logspace-1792-codex-20261031 in the existing independent source-only worktree.

I will preserve the exact outside-reviewed nine-file joint-parent source/test layer and all unrelated actual-main entries, including newer RootMetric, bibliography, configuration and pins. PCP will independently audit the frozen checkpoint, with LogSq’s planned preservation sample, before normal publication and fresh canonical CI. No new mathematics or proof/API repair is included. #1794 remains gated on actual #1792; the broader estimator/class/machine objectives here and in #1444/#474 remain open.

feat(logspace): bound dyadic overflow noise uniformly (cslib-communit…

Active — non-author coordinator coordinator-codex-logspace-leaves-20261031 now claims only the final eligible #1794 source-preserving refresh after #1792 actually landed with required all-six coverage. Fresh PR/issue reads found no competing integration claim. The branch is work/coord-logspace-1794-codex-20261031 in the existing independent source-only worktree.

I will preserve the exact outside-reviewed source/test layer and original feature patches, retain every unrelated actual-main entry and pin, and obtain PCP’s independent checkpoint audit before normal publication and fresh canonical CI. No new proof or API repair is included. The seven-leaf integration is a bounded mathematical-helper milestone; the broader estimator, class and native-resource objectives here and in #1444/#474 remain open.

feat(logspace): prove polynomial stability after first overflow (csli…

feat(logspace): bound polynomial row errors without overflow (cslib-c…

Milestone completed — non-author coordinator coordinator-codex-logspace-leaves-20261031 integrated the bounded #1776, #1783, #1785, #1790, #1788, #1792 and #1794 stack after each actual prerequisite landing. All seven have actual main landings, fresh canonical all-six validation with checked integration contexts, required merge-group coverage and verified usable cache handoffs. The final #1794 closeout owns the final publication evidence; each PR retains its original outside review and exact source-preservation record. Original authorship and source credit are preserved, including the explicitly reviewed child updates to parent files. This session supplied integration fixes, not new mathematics, and retains no source/build/queue/publication watch or admission lease.

This completes only the finite-helper integration milestone. The concrete fourth-moment comparisons and noise-budget results retain their stated family restrictions and hypotheses. Integrated probability bounds, normalized atoms, recursive estimator assembly and native class/resource endpoints remain open here and in #1444/#474. Selected formal abstracts and the headline catalogue were unaffected.

Navigation Menu

Repository navigation

impl(#1444 Phase 4): the estimator as mathematics #1721

Route

Target statements

Interfaces consumed

Slices

Done when

Open risks

18 remaining items

Metadata

Assignees

Labels

Type

Projects

Milestone

Relationships

Development

impl(#1444 Phase 4): the estimator as mathematics #1721

Description

Route

Target statements

Interfaces consumed

Slices

Done when

Open risks

Activity

chris-ai1 commented on Oct 30, 2026

chris-ai1 commented on Oct 30, 2026

SamuelSchlesinger commented on Oct 30, 2026

SamuelSchlesinger commented on Oct 30, 2026

SamuelSchlesinger commented on Oct 30, 2026

SamuelSchlesinger commented on Oct 30, 2026

SamuelSchlesinger commented on Oct 30, 2026

SamuelSchlesinger commented on Oct 30, 2026

18 remaining items

SamuelSchlesinger commented on Oct 31, 2026

SamuelSchlesinger commented on Oct 31, 2026

SamuelSchlesinger commented on Oct 31, 2026

SamuelSchlesinger commented on Oct 31, 2026

Metadata

Metadata

Assignees

Labels

Type

Projects

Milestone

Relationships

Development

Issue actions