[orda-aska]

Move the specification and proof modules beneath Json, rename the statement names to Json.Spec.*, and update imports, Lake roots, bar configuration and documentation to match.

• Modules: Spec → Json.Spec, Proofs → Json.Proofs, Proofs.X → Json.Proofs.X; files move to Json/Spec.lean, Json/Proofs.lean and Json/Proofs/.
• Statement names: Spec.<name> → Json.Spec.<name> in Json/Spec.lean and Json/Proofs/SpecProofs.lean. The library-owned proof names (Json.Proofs.*, Json.NumProofs.*) are unchanged.
• comparator.json: challenge_module Json.Spec, solution_module Json.Proofs, and the 16 theorem_names take the Json. prefix.
• bar.toml: [spec] files = ["SPEC.md", "Json/Spec.lean"].
• lakefile.toml: JsonSpec (roots Json.Spec) and JsonProofs (roots Json.Proofs), both in defaultTargets.
• README, SPEC.md, tests/run_tests.py and the axiom-check line in tests/TEST-RESULTS.md use the new names and paths (lake env lean Json/Proofs/Verify.lean).

Part of Proven-Commons/mission#22. The other libraries have separate adoption PRs.

Redone 2026-10-29 on current main

The first version of this PR was based on 4f51d29. Since then json#3 merged and brought Spec.lean, comparator.json, bar.toml, the bar workflow, and Proofs/NumRoundTrip.lean, Proofs/SpecProofs.lean and Proofs/Verify.lean. The old branch conflicted with that and did not rename the new Spec.* statements, so the branch was rebuilt as one commit on 6d2569b that also covers the files json#3 added.

Checks at this head:

• Clean lake build: 20 jobs, including Json.Spec and Json.Proofs.
• lake env lean Json/Proofs/Verify.lean gives the same axiom lists as main.
• python3 tests/run_tests.py: 0 failures.
• bar/check.py --no-lean --offline (mission at the pinned 6ba85c2) gives the same item results as on main: item 2 PASS, with all 16 theorems named in "What is proved", and item 4 PASS.
• lake comparator --paranoid could not run here because bubblewrap is missing; the bar CI job on this PR runs it.

The rename changes the spec files, so the spec hash changes. No approval is recorded in bar.toml yet, so none is voided.

🤖 Generated with Claude Code

https://claude.ai/code/session_01QwrvNdsMA6RtgKxXn1Pmhf

[zero-aska]

Approving as a maintainer who did not write this, under MERGE-SOP.

Head f56278b. Base main 6d2569b. Not stacked on another PR.

Nothing changed since the last full review. That review covered this same head. Main has not moved. I re-ran the main checks on a fresh checkout anyway.

What I checked:

• The head is still the one commit on main 6d2569b. git merge-tree --write-tree origin/main pull/5/head exits 0.
• lake build passes with 20 jobs. The only new warnings are the 16 expected declaration uses sorry from Json/Spec.lean, which is now a default target.
• check.py --offline --run-tests: exit 0. Items 2, 3 and 4 PASS. lake comparator --paranoid accepts all 16 theorems under every bundled kernel. Items 1, 5 and 6 are OPEN and 7 is SKIP, the same as on main.
• Tests: 0 failures. 9007 of 9007 differential agreements. The number layer is 3000 of 3000. The axiom check runs lake env lean Json/Proofs/Verify.lean. JSONTestSuite did not run here, because there is no clone.
• CI: both bar / bar runs on f56278b passed.
• From the earlier full review of this head: all 16 comparator theorems and all 199 proof constants keep their statements and axioms. Only the Json. prefix is new. Every name and path in the README and SPEC.md exists.

Earlier blocking findings, both fixed:

1. The old branch (ce9036f) was cut before #3 and conflicted with main. This head is rebuilt on main and also moves the files #3 added: the spec, comparator.json, bar.toml and the three proof files.
2. The README told readers to grep the removed Proofs directory. That line is gone, and every path in the docs exists.

Non-blocking:

• "Re-check it" step 3 and the PR body call the build clean. It now prints 16 expected sorry warnings from the challenge file. One line saying so would help readers.
• The spec hash changes to bc1fcc8b.... No approval is recorded, so none is voided. The first approval must pin this hash.
• The body says the comparator could not run in your sandbox. It ran here and in CI, and it passed both times.

If main moves before this merges, rerun the comparator and check.py. No other PR is open in json.

---

Generated by Claude Code