Repository navigation
feat(logspace): charge actual polynomial output errors on false overflows - #1785
Merged
SamuelSchlesinger merged 19 commits intoOct 31, 2026
Merged
Conversation
The Phase 4 estimator needs to retain only a bounded list of exceptions without losing stability when that list changes. Formalize the native two-coordinate compression update of OpenAI2026LogSpace Section 8.2, equations (8.5)-(8.6), and all conclusions of Lemma 8.1. Prove small-entry replacement, signed large-entry preservation, coordinatewise interpolation, monotone defaults, strict candidate capacity and containment, and uniform 28-Lipschitz stability. Also prove the local 6u change bound used by the subsequent preloss argument. Add concrete tests of partial clipping, signed values, positive-default padding, empty rows, candidate selection and perturbations. This advances #1721 and #1444. Iterated propagation and its slack conversion (8.7), rarity estimates, recursive estimation and machine-space realization remain open. No selected formal abstract or roadmap endpoint changes. Validation on Lean v4.36.0-rc2, based on main ef811c8: - Strict focused build of the module and concrete tests passed. - scripts/check.sh passed all six gates: strict full build, mk_all check, strict full tests (including the global axiom audit), lint, lint-style, and checkInitImports. - check_changed_files.py, check_tidy_surface.py, and check_hygiene.py passed. - Focused hygiene with --check-simp and git diff --check passed. Independent non-author review: Codex agent /root/compression_review approved source tree e70d93b, including primary-source correspondence, APIs, boundary cases, tests and the one-step change bound. No requested fixes remain. This is agent review, not human approval. Worker: codex-row-compression-20261030, branch feat/logspace-compression-update. AI assistance: OpenAI Codex implementation and independent Codex review.
Add concrete increment-and-compression states and schedules. Prove width-independent 28^j propagation, exact restarts, a fifth-power slack bound under an explicit group-count condition, and accumulated row/default loss before overflow. This establishes the update-only part of OpenAI2026LogSpace (8.7) and the unweighted part of Lemma 8.2; weighted preloss and the final root functions remain separate. Validation on base c3f7a58: direct Lean 4.36.0-rc2 checks of both new modules with project options passed without diagnostics, using isolated output files and the parent checkout dependencies read-only. Concrete tests cover a two-group nonzero-loss execution, satisfied no-overflow bounds, an actual overflow after lowering capacity, and distinct initial-state perturbations. Focused proof hygiene including --check-simp and git diff --check passed. Aggregate regeneration and full project gates are delegated to integration. AI assistance: ChatGPT implemented and checked these proofs as worker codex-compression-iteration-20261030. Independent agent source/API review: codex-source-release-20261030 approved the library and tests at 7d08e44bbdb626b74adaa9c4d63e07faa28ce525. Publication adds only the generated aggregate import. Integrated targeted build, tests, aggregate check, hygiene and whitespace checks pass. Full gates run in PR CI.
Use decreasing power-of-two slacks and the explicit floors eta * (1/1024)^slack. Derive consecutive floor separation, both finite-sum bounds from source equation (8.8), and the local 8*rho <= eta margin. Bound propagation for the actual remaining group count, distinguishing updates after the current group from those including it. The source uses unscaled inverse powers of two; this mathematical witness explicitly scales by eta and does not choose an exponent for the full integrated estimator. Validation: direct Lean 4.36.0-rc2 checks of Floors.lean and RowCompressionFloors.lean with project options passed without diagnostics, using private outputs and parent dependencies read-only. Tests compute nonzero floors, check halving and empty schedules, and apply the sum theorem to a concrete no-overflow compression execution. Focused hygiene including --check-simp and git diff --check passed. Base is iteration milestone 7d08e44bbdb626b74adaa9c4d63e07faa28ce525; aggregate and full project validation remain integration tasks. AI assistance: ChatGPT implemented and checked the proofs as worker codex-compression-iteration-20261030. Independent agent source/API review: codex-source-release-20261030 approved module/tests at bd14fc247724f63e650ced31e7b0e6c4d30fcee1. Publication adds only generated import registration. Integrated strict module/test build, focused hygiene and whitespace checks pass. Full gates run in PR CI.
Supply a computable rational degree-seven transition and its rescaling, with real endpoint, monotonicity, and value/complement fourth-root Lipschitz laws. Exact rational cast lemmas connect the arithmetic definitions to the real analysis. Concrete tests cover interior values, affine rescaling, clamping, equal endpoints, and root perturbations across both transition boundaries. This advances issue #1721's fourth-moment route. The pinned primary source OpenAI2026LogSpace, atoms.tex Section 5.1 at revision 7ef5c0cc, uses the same normalized-integral construction with s = 8. This implementation specializes it to s = 4 and does not claim eighth-root regularity, complete hierarchy admissibility, or machine resource bounds. No OpenAI Lean was consulted. Validation on base 2d1638c with the two added files: both modules compile under the repository's Lean options with warnings as errors using isolated temporary outputs and read-only existing dependencies; focused check_hygiene.py --check-simp and git diff --cached --check pass. The final documentation-only wording change was inspected after those builds. Full repository integration gates and independent review remain for coordinator integration; no aggregate file has been edited. Authored by worker codex-logspace-polynomial-cutoffs-20261030 with ChatGPT. Independent agent source/API review: codex-compression-iteration-20261030 approved source a6967d13aafee47ae16b61ac2b12f533426f9971 and freshly compiled both files. Publication adds only the generated aggregate import. Integrated strict module/test builds, hygiene and whitespace checks pass. Full gates run in PR CI.
Remove three aggregate imports that came from untracked source copies during integration. The polynomial switch module and tests are unchanged. Validate import targets against the committed Git tree before publication.
Prove the weighted preloss assertion of OpenAI2026LogSpace Lemma 8.2 for the actual compression recursion, with explicit constant12(1+eta)/eta. Apply it to the concrete dyadic floors, discharging numerical small-floor conditions. Stationary-reference preservation, relative stability after overflow, and the complete estimator remain separate obligations. Independent agent source/API review: codex-logspace-polynomial-cutoffs-20261030 approved599c5e8a and the dyadic application delta4cc6581b. Published library/tests are identical to the reviewed source, with generated aggregate registration. Strict private Lean source/test checks, hygiene and whitespace checks pass. Full integration gates run in PR CI. Worker codex-compression-preloss-20261030; AI-assisted implementation and review.
Define the padded first-coordinate rank and prove concrete threshold, default, row-bound and rank preservation results for stationary references. Above the flat region, the rank stays fixed; inside it, the rank remains in the flat region. A gated row output with separated entry support therefore survives each update and any finite zero-increment schedule with floors at most eta and capacities at least the fixed positive rank K. This formalizes the stationary-output assertion of OpenAI2026LogSpace, Section 8.3, Lemma 8.2, revision 7ef5c0cc. It does not assert equality of whole rows, a root-discrepancy estimate, or post-overflow stability. The explicit support and gate hypotheses do not assume the preservation conclusion. Validation on base 7d08e44bbdb626b74adaa9c4d63e07faa28ce525: direct Lean 4.36.0-rc2 checks of both new files passed without diagnostics, using private outputs and existing parent-checkout dependencies read-only. Tests exhibit an above-flat rank fixed at 1/2 while a zero entry moves to 3/8, an arbitrary stationary iteration retaining nonzero output 21/2, and a low rank moving from zero to 1/8 while output 41/4 is preserved. Focused proof hygiene including --check-simp and staged git diff --check passed. Aggregate regeneration and the full project gates remain integration work. AI assistance: ChatGPT implemented and checked these proofs as worker codex-compression-iteration-20261030. Independent agent source/API review: codex-logspace-polynomial-cutoffs-20261030 approved 10a516829a8cf8ea4fd0da6a65abe00147525b46. Publication changes only dependency ancestry and generated aggregate registration. Integrated strict module/test builds and committed import/hygiene checks pass. Full gates run in PR CI.
Use Q(t) = a*u^4/(1+u)^3 with u = max(0,(t-theta)/a). For a>0, prove nonnegativity, the upper ramp bound, lower defect theta+3*a, monotonicity, and global Lipschitz constant one. The fourth root is globally Lipschitz with explicit constant |a^(1/4)|*|a^-1|; the proof also bounds its derivative at arbitrarily large positive inputs. Definitions use exact rational arithmetic and have real cast lemmas. This is an alternative rational witness for the correction-ramp conditions of OpenAI2026LogSpace Section 4.1 at revision 7ef5c0cc, adapted to issue #1721's fourth-moment route. The primary source uses eighth roots. Full hierarchy threshold/cutoff instantiation is a separate next component; no machine resource bound is asserted and no OpenAI Lean was consulted. Validation atop a6967d13: the module and focused tests compile with the repository Lean options and warnings as errors, using private temporary outputs and read-only existing dependencies. Tests cover exact rational values, negative and large inputs, real cast compatibility, uniform ramp bounds, ordinary perturbation, and the explicit fourth-root Lipschitz constant 8 when a=1/16. Focused hygiene --check-simp and diffcheck pass. Independent review and full integration gates remain for the coordinator. Authored by worker codex-logspace-polynomial-cutoffs-20261030 with ChatGPT. Independent agent source/API review: codex-source-release-20261030 approved d3d62d9ff7fe1e54fabbf8b3ce779f929736f6ba. Publication preserves source/tests and adds generated import registration. Integrated strict module/test builds and hygiene/committed import checks pass. Full gates run in PR CI.
Extend HierarchyParams with the strict core threshold ladder, a positive iteration count, strict copy-count inequality, monotone bounded cutoffs, row-gate closure, and root/complement regularity. Prove the strengthened bundle nonempty using an actual rational ramp and polynomial cutoffs. The construction chooses theta = 1/(128q), width 1/(384q), theta2 = 1/(64q), copy thresholds 1/(8q) and 1/(4q), then the factorial-tail iteration count, copies, and detector ranks in the primary source's dependency order. This advances #1721's fourth-moment hierarchy gap. It is an explicit s=4 adaptation of OpenAI2026LogSpace Sections 4.1-4.4 and Remark 4.6 at pinned revision 7ef5c0cc; the source uses s=8. It does not prove eighth-root regularity, every later atom/access-score margin, a recursive estimator, or a machine-space bound. Existing HierarchyParams APIs are unchanged. Validation atop d3d62d9f: new module and focused tests compile with pinned Lean and repository options, warnings as errors, using private outputs and read-only dependencies. Tests extract actual witnesses at q=2, prove nonzero ramp and exact plateau values, use row-root perturbation at its closed endpoint, and feed the underlying parameters into the existing stage API for a nonzero two-vertex matrix. Focused hygiene --check-simp and diffcheck pass. No aggregate or existing source file was modified. Independent review and full integration gates remain for the coordinator. Authored by worker codex-logspace-polynomial-cutoffs-20261030 with ChatGPT. Independent agent source/API review: codex-compression-iteration-20261030 approved c7ac6dea11574e721ded46aeb0f76c2ccaf79df9 and independently compiled both files. Publication preserves the reviewed source/tests and adds only generated import registration. Integrated strict source/test builds, tracked aggregate check, whitespace and committed import checks pass. Full integration gates run in PR CI.
Construct the reference state from the actual current default and true row plus accumulated compression preloss. Derive its small-negative and second-coordinate bounds from no-overflow dyadic floors, then preserve gated outputs through the remaining capacities and floors at their original indices with zero increments. Add a separate weighted root comparison with the true zero-padded output. Sensitive targets use the existing weighted preloss bound at eta/2; uniform small loss and lower clipping remove the low targets from the rank comparison. The theorem assumes scalar support, flatness and root-Lipschitz laws and a raw-prefix error envelope only at sensitive targets, not the final output estimate. It is exponent-parametric. Instantiating all source row functions and comparison to a subsequent incremented or post-overflow calculation remain separate. Source mapping: OpenAI2026LogSpace, Section 8.3, Lemma 8.2, revision 7ef5c0cc. This connects the reviewed Preloss and Reference layers using the documented margin-scaled dyadic witness. Existing files and aggregates are unchanged. Validation: pinned Lean 4.36.0-rc2 checked the new module and tests without diagnostics, using private outputs and read-only shared dependencies. Tests exhibit a nonzero increment, nonzero actual preloss, preserved nonzero output through the shifted remaining schedule, and a strictly positive fourth-root discrepancy. The review-requested low-target regression raises the padded rank from zero to 1/1048576 while a rank-dependent fourth-root output remains exactly one under a zero sensitive-target error envelope. Focused hygiene with --check-simp and staged diff checking pass. Full project gates and aggregate regeneration remain integration work. AI assistance: ChatGPT implemented and checked this milestone as worker codex-compression-iteration-20261030. Independent reviewer codex-logspace-polynomial-cutoffs-20261030 requested the low-target regression and is reviewing the frozen revision. Independent non-author source/API review by compression_review approved exact source revision c7873d034846fbab13b83d3d9a4d596343c9d191, including a rank-dependent low-target regression. Reviewed source files are unchanged. Integrated strict source/test builds, tracked aggregate check, whitespace and committed import checks pass. Full integration gates run in PR CI.
Define actual rational polynomial preparation, row-gate, auxiliary-score and broad-witness functions. Prove their range and closed threshold laws, flat rank regions, incoming-score compatibility, joint Lipschitz fourth roots, and exact rational-cast identities. Preserve the existing exponential AtomCutoffs API and Christian Reitwiessner's source credit. This is the fourth-moment adaptation for #1721 of the threshold template in OpenAI2026LogSpace (5.5), and the witness in the support-margin proof and compression-threshold table of Section 5.5, revision 7ef5c0cc. The source uses eighth roots; these degree-seven cutoffs only establish fourth-root regularity. The actual functions are proved regular, rather than an assumed regularity bundle. Normalized main outputs, access enumeration and machine-resource bounds remain separate. Validation: the new module and full focused test file compile without diagnostics with Lean 4.36.0-rc2 and repository strict options, using private outputs and read-only dependencies. Executable rational tests evaluate all three row functions to 1/4 with both switches in their transition regions. Further tests check signed inputs, closed endpoints and the witness's strict 82 > 3*27 margin, real/rational agreement, nonzero existing atomPrep and auxScore expressions on a concrete matrix, and nonconstant fourth-root variation. Focused --check-simp hygiene and staged diff checking pass. Independent review and full integration gates remain pending; aggregate regeneration belongs to the coordinator. AI assistance: implemented by worker /root/compression_review on feat/logspace-polynomial-atom-cutoffs, based on the reviewed hierarchy lane. The Stationary specialization will be a separate cross-lane change. Independent non-author source/API review by lean_environment approved exact source revision a4eae07bdd9993e038a83aea84cc3c4b31c794d9 against pinned atoms.tex, with no findings. Reviewed source files are unchanged. Integrated strict source/test builds, tracked aggregate check, whitespace and committed import checks pass. Full integration gates run in PR CI.
Dependency join for the concrete polynomial atom-row consumer. Inputs are PR #1757 and PR #1750. This is a feature-branch merge, not a merge into main. All compression source/test blobs are identical to the reviewed second parent; the first parent is retained unchanged. The tracked aggregate checker passes. No full estimator endpoint is claimed.
Prove uniqueness of the first-overflow index, a signed light-target error lower bound, the explicit 2^(p+1)/(n*rho^p) moment charge, and its specialization to the actual dyadic iterate with previous default and preloss bounds derived. Conditional heavy-count rarity, relative post-overflow stability and integrated compression remain open under #1721 and #1444. Strict isolated Lean compilation with warningAsError=true and empty diagnostics passed for the module and a signed two-group run with nonzero preloss. Focused hygiene and whitespace checks passed. AI-assisted implementation; independent review pending before publication. Independent non-author source/API review by lean_environment approved exact source revision e0066c8a1015c2270c0a9ffaec1a3209225b2ce3 against pinned compression.tex Section 8.4, with no findings. Reviewed source files are unchanged. Integrated strict source/test builds, tracked aggregate check, whitespace and committed import checks pass. Full integration gates run in PR CI.
Prove the conditional true-heavy-count estimate, deterministic endpoint-error and retained-row maximum bounds, and the actual affine-channel instance at two rates. This is the conditional-rarity component of OpenAI2026LogSpace Lemma 8.4 (revision 7ef5c0cc), contributing to #1721 and #1444. Validation: rebuilt the complete 23-module Complexity dependency closure from exact source with pinned Lean 4.36.0-rc2 and strict warnings, then checked the final concrete tests and existing RootMetric tests. Hygiene, tracked import aggregate, focused module-doc name checks and whitespace checks pass. Full project gates run in CI. AI-assisted implementation and tests: OpenAI Codex. Independent nonauthor agent /root/review_heavy_rarity approved source tree 8549f1f after checking the pinned source and final regression delta. A cache/source mismatch found in review was resolved by exposing exactly the two norm definitions consumed here and rebuilding all local prerequisites. No human approval or full estimator endpoint is claimed.
Add the concrete preparation, auxiliary-score, and broad-witness row consumers of the stationary-reference compression results for issue #1721. The three-constructor PolynomialAtomRow selects actual rational polynomial functions; no scalar support or regularity contract is assumed. Prove strict retained support, zero default output, rank flatness, stationary preservation, and a weighted fourth-root comparison with a constant quantified before the endpoint type, row, rank, schedule, and error envelopes. Bridge the existing Matrix.atomPrep and Matrix.auxScore expressions at their zero-padded ranks. Source mapping: OpenAI2026LogSpace revision 7ef5c0cc, atoms.tex Section 5.5 support margins and compression-threshold table, and compression.tex Section 8.3 Lemma 8.2 stationary preservation/root comparison. This is the explicit fourth-moment adaptation, not the source's eighth-root endpoint. The sufficient scale margin is 0 < eta <= theta/10000. Normalized main atoms, incoming-gate assembly, access enumeration, overflow stability, and machine resource bounds remain open. No curated abstract changes. Tests construct nonzero actual preloss, move the true witness rank into its polynomial transition, prove positive output and positive root discrepancy, and apply the uniform weighted theorem. A remaining compression group changes the default and erases a nonzero second coordinate while preserving the witness. A separate K > cardinality example distinguishes positive dummy padding from zero padding, with a signed raw coordinate. Validation: library and tests independently compiled without diagnostics using Lean 4.36.0-rc2 and -DwarningAsError=true under project linter options, private outputs and read-only shared dependencies. Focused hygiene --check-simp and staged git diff --check pass. Full integration gates are coordinator-owned. No aggregate changes. Authored with AI assistance by worker codex-logspace-polynomial-cutoffs-20261030; independent review pending. Dependencies: local integration merge 35e8a8ec combines independently reviewed PolynomialAtomCutoffs a4eae07b and Stationary c7873d03 unchanged. Only the two new PolynomialAtomRows files belong to this implementation. Independent non-author source/API review by lean_environment approved exact source revision 5925d6e06da530885fbf5144a844439fcf8084a6 and its unchanged reviewed cutoff/compression dependencies, with no findings. The two implementation files are unchanged after joining the published dependency lanes. Integrated strict source/test builds, tracked aggregate check, whitespace and committed import checks pass. Full integration gates run in PR CI.
Derive the deterministic heavy-set bound from nonnegative row mass, then apply finite Markov at ceil(n/2) with one distinguished endpoint. The conditional frequency is at most (2 + 8*c*Cmass)/(n*rho), including empty conditioning slices. An independent start slice preserves the bound. The actual affine broad/narrow specialization obtains c = 2^H from the existing cross-rate pair count and uses rate alpha^H. Regression examples have perfectly correlated off-endpoint hits with exact frequency 1/8 and bound 1/2, odd capacity, empty conditioning and the strict heavy threshold. The affine example uses P=7, broad side 2, narrow side 1, and the nontrivial bound 19/21, with both exceptional and nonexceptional seeds in the same conditioning slice. Validation on base c172011fc0702d7c7a4317b0ad94e57ae13e3bb1 plus these two files: direct Lean 4.36.0-rc2 elaboration of the module and its test file, with -DwarningAsError=true, -DautoImplicit=false and repository weak linter options, both exit 0 with blank diagnostics. Existing dependencies were read-only and outputs private. Focused check_hygiene.py --check-simp and git diff --cached --check passed. Aggregate and full hosted gates are left to coordinator integration under the shared disk constraint. Source: OpenAI 2026 preprint revision 7ef5c0cc, compression.tex Section 8.4, lemma/equation buf-rarity. This closes conditional true-heavy-count rarity only; masked mean/noise estimates, post-overflow stability and integrated compression remain open. No curated abstract changes. AI assistance: ChatGPT implemented and self-checked the Lean proofs and tests. Independent exact-revision review is requested from the coordinator. Independent non-author source/API review by agent derandomization_plan approved source revision 2391fbec3d50c9927750105dff0466330717b951 with no findings. Review covered finite Markov counting, the forced endpoint, odd capacities, empty slices, the actual affine specialization, and nonvacuous tests. Integrated source and tests are byte-identical to that reviewed revision. Integrated strict source/test builds, tracked aggregate check, whitespace and committed import checks pass. Full integration gates run in PR CI.
Reuse and preserve #1765, remove the parallel API from #1772, and preserve both regression suites. Independent non-author review by compression_review approved exact repair commit 87ba529262bc3c43936db63b5267038d90773a8e over dependency merge 795c68b63027b99b74666efe17c976a85ad0c9a0 with no findings. Source/test bytes match that snapshot. The additional parent preserves the independently developed #1765 at c9f0890. Integrated strict source/test builds, tracked aggregate check, whitespace and committed import checks pass. Full integration gates run in PR CI.
Compose actual compressed polynomial atom rows with the normalized first-overflow prefix error charge. Preserve both dependency histories from #1772 and #1766. Independent non-author agent polynomial_false_review approved exact source commit cc6762148fee14289865a7c30fc1231f927eed8d with no findings. Integrated source and behavioral test blobs match the reviewed revision. Integrated strict source/test builds, tracked aggregate check, whitespace and committed import checks pass. Full integration gates run in PR CI.
edemaine
approved these changes
Oct 30, 2026
edemaine
left a comment
edemaine
left a comment
Collaborator
There was a problem hiding this comment.
Agent approval by reviewer-codex-edemaine of 9941765. Reviewed the complete three-path own layer; verified all other source blobs against the two reviewed parents #1772/#1766 and reused their coverage. No findings.
The actual outputs use each state’s own padded rank/default. Their roots lie in [0,1] and discrepancy support lies in the union of two supports of size <K, giving the width-independent fourth-power bound 2K. Multiplying the existing actual raw-prefix false-overflow charge yields exactly 64K/(n_j*ρ_j^4). The finite-union proof sums those charges without an extra group-count multiplier. Nonnegative truth, zero second coordinate at light targets, zero initial default, positive floors/capacities and normalization sign are explicit; shared environment dependence is allowed.
Checked the mapping against pinned 7ef5c0cc §8.4, Proposition 8.5, printed p.49. The correlated regression has an actual overflow/default change, erased negative second coordinate, nonzero output moment 1/2 and the stated raw-prefix moment; both normalized bounds and empty horizon are exercised. Full estimator/budget obligations remain open; no curated-abstract impact.
Aggregate coverage (3,051 modules) and whitespace passed. At inspection title passed; Lean CI 41107338862, Guide and Comparator were running. No local Lean build. This is agent review, not human approval.
This was referenced Oct 30, 2026
Collaborator
Author
|
Independent mechanical preservation audit by Read the actual parents Unchanged guarded normal FF publication is authorized after fresh source-head/ownership checks. This reuses the exact outside mathematics coverage; it is a mechanical-restack preservation verdict, not a new mathematics approval or approval count. Fresh canonical native all-six validation and actual tested-checkout evidence remain mandatory before the later integration verdict/queue. No source repair, local Lean/build or cache retrieval was performed. Agent audit, not human approval. |
SamuelSchlesinger
changed the base branch from
feat/logspace-compression-heavy-count
to
main
October 31, 2026 03:39
Collaborator
Author
|
Non-author coordinator Fresh canonical CI passed all six named gates. Its finalized log verifies actual synthetic checkout Actually landed at 04:24:25 UTC as |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
The false-first-overflow charge now bounds errors in the actual final polynomial row outputs. Each computed and true output lies in [0,1] and has fewer than K retained nonzero entries, so its fourth-root discrepancy has summed fourth power at most 2K. Composing this with the existing actual raw-prefix charge gives coefficient
64*K/(n_j*ρ_j^4); a second theorem sums the charges over the finite union of possible false first overflows.The result uses each state's own padded rank and default, the existing normalized row moment, and the actual clipped raw prefix at j+1. Retention, increments, truth, and overflow may all depend on the same environment. The light-target second-coordinate condition is explicit; no independence, assumed final-output error bound, or post-overflow stability premise is used.
Both prerequisites #1772 and #1766 have landed. This PR now targets main; its own change is the two source/test files plus one aggregate import. The ordinary actual-main merge preserves both original dependency histories and all current-main entries. Advances #1721 and #1444. Prefix moment budgets, true-heavy contributions, post-overflow relative stability, summation of costs, and the recursive estimator remain open. This completes the false-type contribution for concrete polynomial row outputs, not the full integrated compression estimate or BPL ⊆ L. No headline abstract changes are warranted.
Validation and review
-DwarningAsError=true, without diagnostics. Integration rechecks the exact reviewed source/test bytes.(1+(1/8192)^4)/2, discharges every hypothesis of both normalized theorems, and checks an empty horizon.polynomial_false_reviewapproved exact sourcecc6762148fee14289865a7c30fc1231f927eed8dwith no findings, including the pinned Section 8.4 mapping, semantics, normalization, and regression examples. Published revision.AI assistance: ChatGPT agents
lean_environmentandpolynomial_false_finishimplemented and validated the change; separate agents reviewed and integrated it.Supported-main refresh: the exact outside-reviewed feature layer and original authorship are unchanged; only the generated aggregate needed reconciliation. Selected formal abstracts are unaffected: statements, definitions, models and scope remain unchanged. Current validation and integration status are in the single integration record.