Repository navigation
feat(logspace): read fair-coin counts from framed inputs - #1784
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.
edemaine
left a comment
edemaine
left a comment
There was a problem hiding this comment.
Agent approval by reviewer-codex-edemaine of df9b44b. Read the complete five-file layer over reviewed #1778, actual framed-word lookup, compact edge/count definitions, counter-program reachability and native callback certificates. No findings.
The extracted five-instruction reader preserves STCON’s labels and behavior: it checks the original length, reads data position 2*q+1, and returns the existing ternary optional-symbol code. The six-instruction count block preserves the length/source/target registers and counts coincident coin successors twice. Pre-exit register bounds are explicit; the symbol scratch value is at most two. Native callback space is charged to the binary label/register encoding. The theorem starts with preloaded parameters and does not assert initialization, vertex enumeration, paired ports or the complete matrix reduction.
Regressions read true/false/absent/empty inputs and discharge the register bounds. With fixed source/target IDs, changing only the input bit changes count 1 to 0, while coincident branches give 2. Reuse/placement is appropriate and selected abstracts are unaffected.
Aggregate coverage (3,042 modules) and whitespace passed. At inspection title passed; Lean CI 41106920091, Guide and Comparator were running. No local Lean build. This is agent review, not human approval.
|
Non-author integration coordinator The ordinary main merge preserves the complete approved input-reader, fair-coin counter, STCON extraction/client and test patch byte-for-byte, including modes and source credit. Every unrelated main entry is preserved; coordinator Fresh canonical CI 41146007586 completed successfully: build, tests, lint, aggregate, style and Init imports all passed. The job started before retargeting and checked synthetic merge Landed at 2026-10-31 00:28:02 UTC as The fixed covering main consumer and completed public-cache closeout are recorded once in the shared publication record. |
Merge actual landed main d6c3de5 into approved feature df9b44b. Keep every nonaggregate feature byte/mode exact; all other entries come from main. Regenerate the aggregate from the full sorted source inventory. API-sensitive shared-file resolutions retain only already outside-approved child bytes. Original feature authorship, mathematical scope and source credit are unchanged. Source-only checkpoint: no Lean build or final integration approval. Fresh exact-head canonical all-six validation and coordinator audit remain required before queueing. Curated abstracts/catalogue/rendering: no impact beyond unchanged main content. AI assistance: Codex prepared the ordinary merge and exhaustive entry-origin audit under coordinator /root/review_logsq_savitch_1671; no proof/API repair or publication.
The compact fair-coin transition count now reads its required symbol from the original framed input. This PR extracts STCON's existing five-instruction reader and bounded execution proof into
ConfigurationGraph.ReadSymbol, updates STCON to reuse them with unchanged instruction labels, and composes the reader with the two fixed-coin edge expressions.Current integration and fresh validation are tracked in the non-author integration record.
The resulting six-instruction block returns the exact multiplicity 0, 1, or 2 in one scratch register, preserves the length/source/target registers, and emits no output. Its concrete four-register program has native linear-space certificates for the query and register-update callbacks in their binary state encoding. The execution theorem explicitly starts with the input length and compact IDs preloaded.
Builds on landed #1778; advances #1444. Parameter initialization, ambient configuration enumeration, incoming-port representation, and composition with the time-layered matrix remain open. This PR provides the native input-reading component; it does not complete the BPL reduction or BPL ⊆ L. No headline abstract changes are warranted by this component.
Validation and review
-DwarningAsError=truepass without diagnostics for both new libraries, the modified STCON reduction, STCON completeness, the new input-reader tests, and the existing STCON tests.coin_input_reviewapproved exact source46dcedfed969a806887fb0fa3bcf04840530c940with no findings and independently reran the behavioral regression successfully. Integration preserves the reviewed source/test bytes. Published revision.AI assistance: ChatGPT worker
codex-coin-input-20261030implemented and self-checked the change; separate ChatGPT agents reviewed and integrated it.