Repository navigation
feat(logspace): identify the clocked ambient configuration matrix - #1791
Merged
Merged
Conversation
Read each fixed-coin edge of the compact configuration graph and add the two contributions, preserving multiplicity when the successors coincide. Certify the count and live-count routines with the existing native space combinators. Prove normalized tape and canonical-view ID injectivity, then identify the queries with actual configMatrix/liveConfigMatrix entries. Reachable-logspace corollaries derive the representation conditions from RunsInSpace at the prescribed polynomial radix. Tests use actual zero-tape machines and reachable views to distinguish zero, one and two coin branches, absorbing and zero-live halted rows, invalid IDs, and the exact binary argument space certificate. Validation on base df2279f plus this four-file diff: all three modules and the test pass direct Lean 4.36.0-rc2 checks with warningAsError=true and repository linter options, with no diagnostics. Focused hygiene --check-simp and staged git diff --check pass. Outputs are isolated and shared compiled dependencies are read-only. Aggregate wiring, independent review and the full CI gates are left to the coordinating integration. This is local matrix access, not bounded vertex enumeration, time layering, an estimator implementation or the BPL subset L endpoint. No selected abstract or catalogue impact. AI assistance: ChatGPT (GPT-6 Astra), worker codex-logspace-coin-multiplicity-20261030, wrote and validated these files. Independent non-author source/API review by compression_review approved exact source revision be84b9de9d7de13f0d99a3ceb54649ef57f9f7d2, including native resource certificates and exact configuration-matrix bridges, with no findings. Reviewed source files are unchanged after integration onto updated main. Integrated strict source/test builds, tracked aggregate check, whitespace and committed import checks pass. Full integration gates run in PR CI.
Construct a time-layered matrix with edges only to the next clock layer, terminal-only reward, and the explicit remaining-horizon potential. Prove strict upper triangularity, substochasticity, bounds on every potential coordinate, the linear-system identity, determinant one, and its inverse solution. This follows the ordinary absorbing-matrix convention of the pinned model.tex Lemma 2.1 (OpenAI2026LogSpace, revision 7ef5c0cc). Specialize to the actual half-normalized fair-coin configuration matrix and prove its clock-zero potential is the native finite-time acceptance frequency and the existing finite sum of first-stop live terms. Identify clocked entries with the certified compact-ID coin-count reader. Apply the existing BPL configuration-matrix theorem to obtain concrete polynomial-size strict-forward systems with bounded potential and the 2/3 versus 1/3 gap. Tests realize a zero-work-tape machine that loops on false and accepts on true. They prove its actual two-step acceptance probability is 3/4 and read a nonzero clocked edge from the compact IDs. Additional checks cover an absorbing matrix, terminal-only reward, zero horizon, the explicit linear system and inverse, and the exact clocked cardinality. Validation on base 406a68d plus this three-file diff: both library modules and ComplexityTests/TimeLayer.lean pass direct Lean 4.36.0-rc2 with warningAsError=true and repository linter options, without diagnostics. Focused check_hygiene.py --check-simp and staged git diff --check pass. Builds use only tiny isolated outputs and read-only compiled dependencies; there are no Lake/cache/bootstrap operations. Aggregate registration and full CI gates remain for coordinating integration. The final independent review is pending; the two unchanged library snapshots already received a no-findings source review from lean_environment. This is a concrete semantic reduction. Bounded vertex enumeration, composition with whole-input symbol access, incoming paired ports, the recursive estimator, and the native BPL subset L endpoint remain open. No selected abstract or catalogue impact. AI assistance: ChatGPT (GPT-6 Astra), worker codex-time-layer-20261030, wrote and validated the three files. Independent non-author review by lean_environment approved exact source commit dafd85f98e5fd78eec31900dff411b0c5bf8c138 with no findings; integrated library and test bytes match that snapshot. Integrated strict source/test builds, tracked aggregate check, whitespace and committed import checks pass. Full integration gates run in PR CI.
Extract STCON's five-instruction input-symbol reader and its bounded ReachesOut proof into ConfigurationGraph.ReadSymbol, then make the existing STCON writer reuse both without changing its instruction labels. Compose that actual reader with the two fixed-coin arithmetic edge tests. The six-instruction block returns the exact 0/1/2 multiplicity in its scratch register, reads the original framed input, preserves the length and IDs, and emits nothing. Its concrete four-register program has native linear-space certificates for its query and execution callbacks. The entry length and compact IDs are preloaded explicitly. This is a native input-reading component, not a completed ambient enumeration, paired-port construction, or whole Phase 1 reduction. Focused validation: direct Lean 4.36.0-rc2 with the project options and -DwarningAsError=true passed without diagnostics for ReadSymbol, FairCoin.ReadInput, STCON.Reduction, STCON.Completeness, the new FairCoinInput tests, and the existing STCON tests. New tests read true, false, absent and empty-input symbols and prove bounded runs of an actual input-dependent machine with fixed compact IDs returning 0, 1 and 2. The hygiene check with --check-simp and git diff --check also passed. Shared dependency outputs were read-only; all direct-Lean outputs were private. Full repository CI and aggregate registration remain integration work. Independent exact-revision review is requested separately. AI assistance: ChatGPT worker codex-coin-input-20261030 implemented and self-checked this change under the coordinating agent's agreed scope. Independent non-author agent coin_input_review approved exact source commit 46dcedfed969a806887fb0fa3bcf04840530c940 with no findings and independently checked the behavioral tests. Integrated source/test bytes match that reviewed snapshot. Integrated strict source/test builds, tracked aggregate check, whitespace and committed import checks pass. Full integration gates run in PR CI.
Enumerate every compact source/target pair from the actual zeroed counter program initializer on the original framed input. Reuse the existing word header, fair-coin input reader, counting-loop API, and row-major list API. Each two-bit entry records the exact count zero, one, or two, including coincident successors. Prove the entire transducer computable in native deterministic logarithmic space, with no preloaded parameter hypothesis. Move the existing STCON polynomial counter-bound proof into the shared configuration-graph layer and migrate STCON without weakening its result. Clocked enumeration, paired ports, the strict-forward-system bridge, and the recursive estimator remain open. No headline abstract or roadmap endpoint changes are warranted by this component milestone. Validation: strict direct Lean with project options and warningAsError=true passed without diagnostics for CounterBounds, FairCoin/Table, the new FairCoinTable tests, STCON Reduction, STCON Completeness, existing STCON tests, and existing FairCoinInput tests. Focused hygiene with --check-simp and git diff --check pass. New tests use actual initialized runs with 1458 output bits and nonzero input-dependent entries, coincident successors, empty input, and exponent zero. Full integration gates are left to PR CI. AI assistance: ChatGPT implementation worker coin_input_review authored this change. Independent non-author review is pending; the worker's prior review role on its parent change does not approve this implementation. Independent non-author agent polynomial_false_review approved exact source bb96980f7ce0502b155e116b8fff38bee416cb23 with no findings. Integrated source/test bytes 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.
Connect the initialized native coin-count table to the matrix on every compact configuration ID. Prove deterministic target uniqueness on arbitrary IDs, nonnegative substochastic rows, and exact finite-time machine acceptance from the original logarithmic-space witness, deriving the initial ID and all fitting conditions internally. Reuse time layering on explicit Fin ((T+1)*N) identifiers, preserving numeric strict forwardness, terminal reward, bounded potential and inverse equations. The real-valued BPL endpoint keeps the original space constant and supplies a polynomial dimension and the actual two-thirds versus one-third gap. Reusable pieces are closed-submatrix multiplication/power restriction, finite clock reindexing, and a shared polynomial bound for the clocked compact box. Expose the existing canonical reachable-output lemma instead of re-proving it. Clocked native serialization, directed paired ports and the native recursive estimator remain open; this is not BPL containment in L. Validation on the exact changes from published parent a14b3f2: - All seven changed/new library modules and the concrete new test pass the pinned Lean 4.36.0-rc2 compiler with project options, warningAsError and --error=warning, using private artifacts and existing read-only dependencies. - Eight affected existing source/test checks pass: FairCoin/Table, STCON Reduction and Completeness, randomized TimeLayer, and FairCoinConfigurationReader, FairCoinTable, TimeLayer and STCON tests. - Regression cases cover malformed in-box IDs, an overflowing rejecting branch with exact surviving row mass one half, actual finite-coin acceptance through both matrix bridges, numeric clock splitting, terminal-only reward and zero terminal rows, plus a concrete always-accepting BPL witness. - Focused check_hygiene.py --check-simp and git diff --check pass. Full project gates and aggregate registration are delegated to integration CI. AI assistance: ChatGPT worker coin_input_review authored and self-checked this change. A separate read-only helper identified existing matrix transport APIs. Independent non-author review of the frozen revision is pending coordinator integration; self-checking is not independent or human approval. Independent non-author agent polynomial_false_review approved exact source e3528ff495f376640e72a89414a7b85223ff1ca0 with no findings. Integration preserves the reviewed source/test bytes. 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.
Independent agent approval by reviewer-codex-edemaine of 9895598. Reviewed the complete nine-file layer over #1789 and the actual compact-edge, table, reachable-view, BPL and time-layer definitions. No blocking findings.
Fixed-coin target uniqueness proves the ambient row bound without a reachability premise. The closed reachable-image restriction preserves matrix powers and acceptance, deriving canonical representations, fitting and the start bound from the original space witness. Numeric clock/base indexing preserves strict forwardness; halted configurations advance their clock and receive reward only at final time. The resulting inverse potential is bounded at every ID. Machine, original space constant and polynomial exponent precede the input quantifier, and the actual 2/3 versus 1/3 gap is retained.
Checked the semantic specialization against pinned OpenAI2026LogSpace revision 7ef5c0cc, Lemma 2.1, pp. 7–8. Native clocked serialization, incoming paired ports and estimator/resource assembly remain explicitly open; no curated-abstract impact. The general restriction/reindexing lemmas have appropriate homes and reuse existing constructions. Tests cover malformed in-box IDs, exactly half-mass truncation, actual half-probability acceptance, terminal-only rewards and a discharged BPL witness.
Aggregate coverage (3,049 modules) and whitespace checks pass. At the single inspection, title passed; Lean 41116317268, Guide 41116317963 and Comparator 41116316989 were running. Author reports strict focused checks; I did not run local Lean. Live head and review history rechecked before posting. This is agent review, not human approval.
Collaborator
Author
|
|
Parent #1789 has landed. The add/add conflicts in ConfigurationReader.lean and CounterBounds.lean take this branch's side: main's copies are byte-identical to #1789's head. Complexity.lean regenerated by mk_all. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG
SamuelSchlesinger
changed the base branch from
feat/logspace-coin-table
to
main
October 31, 2026 02:19
Collaborator
Author
|
|
SamuelSchlesinger
added a commit
that referenced
this pull request
Oct 31, 2026
Parent #1791 has landed. The add/add conflicts take this branch's side: main's copies are byte-identical to #1791's head. Complexity.lean regenerated by mk_all. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG
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 initialized native table enumerates every compact configuration ID, while the earlier acceptance theorem used a chosen finite set of reachable views. This PR connects the actual table bytes to the matrix on the entire compact box. Fixed-coin target uniqueness gives nonnegative substochastic rows even at invalid or truncated IDs; a closed-submatrix restriction then proves exact finite-time machine acceptance from the original space witness.
Clocking uses the explicit integer index
clock*N + baseID. The resulting real matrix is strictly upper triangular, has polynomial dimension and terminal reward in{0,1}, and satisfies both the linear-system and inverse-matrix equations with potential in[0,1]at every ID.exists_compactTimeLayer_of_mem_BPLpreserves the original space constant, derives all radix/start bounds internally, and retains the actual2/3versus1/3gap. Reusable matrix transport and clocked counter bounds live in their general modules; the existing canonical-output lemma is exposed instead of re-proved.Stacked on #1789; advances #1444. This closes the ambient-box and numeric-clock semantic bridge. Native clocked serialization, directed paired ports, the recursive estimator, and its space realization remain open. No selected abstract or roadmap endpoint changes are warranted.
Validation and review
Seven changed/new libraries and the new test pass strict direct Lean with project options and warnings as errors. Eight affected existing source/test checks also pass, including the table, STCON reduction/completeness and TimeLayer clients. Tests prove a malformed in-box ID has zero row/reward, a truncated rejecting branch leaves row mass exactly
1/2, actual one-coin acceptance is1/2through both matrix bridges, explicit clock decoding and terminal behavior, and a concrete inhabited BPL witness. Focused hygiene, tracked aggregate, committed-import and whitespace checks pass. Full Lean CI passed for the published revision.Independent non-author agent
polynomial_false_reviewapproved exact sourcee3528ff495f376640e72a89414a7b85223ff1ca0with no findings. Integration preserves the reviewed source/test bytes. Published revision.AI assistance: ChatGPT worker
coin_input_reviewauthored and validated the change, with a read-only API lookup helper; separate agents reviewed and integrated it. Source mapping follows the pinned OpenAI2026LogSpace paper's terminal-time construction; no OAI Lean code was used.