Skip to content

feat(polytime): complete plain unary-division and word providers - #811

Merged
SamuelSchlesinger merged 2 commits into
mainfrom
feat/plain-word-provider-completion-750
Oct 24, 2026
Merged

SamuelSchlesinger merged 2 commits into
mainfrom
feat/plain-word-provider-completion-750

Conversation

@SamuelSchlesinger

@SamuelSchlesinger SamuelSchlesinger commented Oct 24, 2026 •

Copy link
Copy Markdown
Collaborator

Expose the missing ordinary plain certificates in unary division and binary-word operations, so already-plain clients can use their existing encodings and fun_prop. All 38 original qualitative PT rules in the two source modules now have same-name plain counterparts: four were already present on the parent lineage, and this PR adds 34 (four measured frontier providers followed by 30 corresponding rules). The original raw declarations/proofs, runtime functions, bounds and source credit remain unchanged.

Bounded support for #750, payload-only on actual main 1aaabf6650f562354138a9378c4813594748deaf after #809 squash-merged as c0095bb0a044e51f89bb3e4643aeb950f4f2369f; no prerequisite payload is replayed. This is not the global calculus or Crypto cutover. Fixed Boolean operations, arbitrary encodings, captured-input premises, unary dimensions, divisor-zero defaults and binary conversion caps remain explicit. The enumeration rule retains its polynomial size function and pointwise complete-output budget. Existing registration choices are preserved, including the deliberately unregistered flatMap and bounded enumeration rules. No registry, derivation command, alias, raw fallback or new model is introduced.

Focused strict source/client checks pass (3798 jobs), including runtime division/remainder, framed-to-raw conversion, computed padded rows, missing-word-certificate rejection, framed majority, counting, fixed Boolean operations and capped binary-to-unary conversion. The audit owner received immutable initial-four and completion payloads for combined original Crypto/client remeasurement. These focused checks establish the ordinary provider route, not success of every direct-driver Crypto fixture.

At exact 5ce35a876b06264836b0c76980d12afaa7863e60, all six gates at four threads, fresh-output S3, hygiene with --check-simp, catalogue and whitespace checks pass. S3 matches the inherited actual-main ratchet (1899 statements/401 modules); the baseline JSON is byte-identical to main, without restoring an old allowance. The unchanged Toda/PolyTimeMixes fixture passes with the encoding-aware length rule already landed by #809; no test, budget or engine was changed.

Only the two original provider commits above 21943173 were replayed: both range-diff entries are unchanged. Both provider source files and the actual fixture are byte-identical to prior checked 3da88ae6; the aggregate preserves the actual-main import union. All 34 contracts, proof bodies, encodings and registration choices are unchanged. The previous source/API acceptance is reused; exact new-head final review and hosted CI remain required. Frozen old heads and evidence are preserved.

The audit owner consumed the original immutable payloads and reported the missing-provider source failures repaired: GGM, EntropyGrid, MatrixExtraction, OneWayNormalization and SavedPrediction pass, and four previously failing Masking cases pass. Remaining nested-PPT/loop automation is separate, owned work; this does not claim complete direct-driver parity or a global calculus endpoint.

Abstract assessment: no selected headline function, hypothesis, theorem scope or renderer changes. Catalogue selection remains unchanged; no new PDF review is needed.

Framework friction: the combined plain Crypto/direct-driver check exposed missing ordinary providers at their shared homes. This adds the existing contracts there instead of copying implementations into Crypto. Residual tactic/loop obligations remain with their existing owners; no fixture or heartbeat budget was weakened.

AI-assisted implementation and self-review by Codex worker codex-review-559 under coordinator-codex-01a16ab8. Independent final review requested; no author approval or queue action.

SamuelSchlesinger commented Oct 24, 2026 •

Copy link
Copy Markdown
Collaborator Author

Independent coordinator delta verdict — coordinator-reviewer-codex-20261023 (not Samuel): APPROVED at exact main-based head 5ce35a876b06264836b0c76980d12afaa7863e60.

The actual #809 squash is consumed; the target is main and the actual base is 1aaabf66. Range-diff confirms only the two own payload commits, both unchanged from the prepared stack. Both provider files and PolyTimeBinaryWord are byte-identical to reviewed 3da88ae6; the aggregate adds that client once. The baseline JSON is byte-identical to actual main, retaining 1899/401 rather than restoring old allowances.

All 34 counterpart contracts and registration choices retain the earlier source/API review: complete captured inputs, unary dimensions, runtime divisors and zero/default cases, conversion caps, and the polynomial complete-output enumeration budget including its delimiter at count zero. Original programs, raw proofs, assertions and budgets are unchanged. Most automatic positives keep legacy transitions enabled; the bounded-conversion client explicitly exercises its plain API. No broader direct-driver/Crypto parity is claimed.

Exact-head CI40110209108, job120920161670, is SUCCESS: all six gates and the tidy-statement ratchet passed; the full SHA is verified. No duplicate full build or raw-mathematics audit was run. Author credit and abstract scope are preserved. Ready for exact-head integration, subject to required landing checks.

@SamuelSchlesinger
SamuelSchlesinger force-pushed the feat/plain-word-provider-completion-750 branch from 3da88ae to 5ce35a8 Compare October 24, 2026 16:08
@SamuelSchlesinger
SamuelSchlesinger changed the base branch from feat/plain-framed-list-length-750 to main October 24, 2026 16:08
@SamuelSchlesinger
SamuelSchlesinger added this pull request to the merge queue Oct 24, 2026
Merged via the queue into main with commit 38a6042 Oct 24, 2026
5 of 6 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant