Repository navigation
Conversation
Four checked JSON adapters reusing immutable public prerequisites.
This was referenced Oct 14, 2026
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
1 participant
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.
Coverage
Explicit author-checked context: upstream main 0b1cccf; kappa = 836330098538459/500000000000000000 = 0.001672660197076918. These generic theorems do not change or establish the selected multiplication exponent.
Four dimension-parametric modules connect actual Lean.Json values to checked ordered gathers, complete owner rows, original-position call selection, and named packed-column dictionaries. They execute field/shape/count/bounds checks and ordered assignment comparison. Successful dictionary checking derives the decoded column operator, both inverse directions and arbitrary-payload cancellation.
Finite coverage: arbitrary finite dimensions, ordered arrays, repeated indices and arbitrary payload universes. Malformed/missing fields and count mismatches fail explicitly.
Conditional-interface coverage: the executable checker must succeed for the supplied AST, route decoder and assignment. The dictionary adapter checks a separately supplied auxiliary certificate against the actual decoded columns. The source provider itself does not emit that certificate. No semantic operator equality is merely assumed.
Full-theorem coverage: original artifact bytes and selected success, duplicate-key/lexical policy, digest binding, complex phases, physical executor direction/allocation, precision, priced accesses and the full multiplication/runtime theorem remain open. Logical gather is an out-of-place read. This PR does not assert full selected parsed-field or physical-program coverage.
Reproduction
Four unchanged new sources total 31,026 bytes, with nineteen observed standard-only axiom probes and six full printed types. All four final kernel checks and independent reviews accepted without diagnostics. ACCEPTANCE.json records their exact public source identities, probes/types and scope. Detailed original evidence remains preserved with the authors.
SOURCE_MANIFEST.json and fetch_sources.py fetch and hash nine immutable public prerequisites, without copying them into this PR: eight PR1879 modules at 981afe7 and SelectedSourceSyntax from PR1831 at 542f914. REPRODUCE.md specifies Lean 4.21.0 and Mathlib 308445d7985027f538e281e18df29ca16ede2ba3, fresh scratch and topological checking. These commands are prospective; no extra local CI preflight or relocated replay was performed for submission.
Comparison and attribution
The bounded source comparison covers exact public PR1879/1831/1807/1094 heads and retained PR487/1494 interface reviews. Existing selected route tables, owner injections, gather/scatter and idle operators remain attributed to their original work. This chunk adds actual AST-format composition and claims no global novelty. Canonical exports and restricted recovery follow-ons are excluded.
James Chang with OpenAI assistance, Apache-2.0; credit to Rohan Arun's PR1094, Jeremy Kothe's T16 emitter, inherited owner/geometry work, public parser/certificate/gather prerequisites, Lean and Mathlib. Existing notices are retained.