Repository navigation
feat(logspace): write initialized compact fair-coin tables - #1789
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.
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 a14b3f2. Read the complete five-file layer over reviewed #1784, actual header/loop/output semantics, compact count definitions and native logarithmic-space contract. No findings.
The four-register program starts from its actual zeroed initializer, obtains the original word length, resets/enumerates both counters, and emits two threshold bits per pair before halting. Row-major address 2*(uN+v)+b, length 2N² and decoding preserve counts 0/1/2, including coincident successors. All intermediate and final registers have one polynomial bound in framed-input length; the existing native simulation then charges logarithmic workspace, excluding input/output. Machine and radix exponent are fixed before inputs vary. This remains the ordinary guarded compact box, with clocked enumeration, incoming ports and strict-forward-system composition explicitly open.
The shared counter-bound statement/proof is identical to STCON’s former private helper apart from declaration binders; its client migrates without aliases. Regressions establish full initialized 1458-bit runs, input-sensitive fixed entries, multiplicity two, empty input and exponent zero. No curated-abstract impact.
Aggregate coverage (3,044 modules) and whitespace passed. At inspection Lean CI 41111420665, title, Guide and Comparator were queued. Author reports strict focused checks; no local Lean build by this reviewer. This is agent review, not human approval.
Collaborator
Author
|
|
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-input
to
main
October 31, 2026 01:57
Collaborator
Author
|
|
SamuelSchlesinger
added a commit
that referenced
this pull request
Oct 31, 2026
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
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.
#1784 reads one transition count with the word length and compact IDs preloaded. This PR proves native logarithmic-space computation of the entire ordinary compact coin-count table from the original framed word, starting from the actual zeroed initializer.
The four-register transducer reuses the word header, bounded counting loops, and existing coin reader. It enumerates every compact source/target pair and emits two threshold bits encoding 0, 1, or 2, preserving multiplicity when coin successors coincide. The library proves exact row-major access, decoding, output length 2N², initialized bounded execution through halt, and
computableInLogSpace_coinTable. The existing STCON polynomial counter bound moves into a shared module; STCON retains its public guarantee.Stacked on #1784; advances #1444. This closes initialization and compact-box enumeration for the ordinary count table. Clocked enumeration, incoming ports, the bridge to the strict-forward BPL system, and the estimator remain open. No selected abstract or roadmap endpoint changes are warranted.
Validation and review
Seven strict direct Lean checks pass without diagnostics, covering the new libraries/tests, modified STCON reduction, STCON completeness, existing STCON tests and existing fair-coin input tests. Concrete initialized runs emit all 1458 bits; one fixed entry changes from 1 to 0 when the input bit changes and from 1 to 2 when the coin branches coincide. Empty input and exponent zero are also checked. 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 sourcebb96980f7ce0502b155e116b8fff38bee416cb23with no findings, including initialization, enumeration, indexing, native resource bounds, STCON preservation, and tests. Integration preserves the reviewed source/test bytes. Published revision.AI assistance: ChatGPT implementation worker
coin_input_reviewauthored this change; separate agents reviewed and integrated it. Its author's earlier review of the parent PR is not approval of this implementation.