Repository navigation
OI-FINITE-PROTOCOL-1: adopt conditional finite-depth protocol - #812
Merged
Merged
Conversation
…tive design validation
…nt before design CI
…untercontrols before design CI
This was referenced Oct 12, 2026
…design run before freeze
…frastructure Owner designated exact freeze F 1f17f1a in an explicit async response and instructed proceeding on #812. F check-run attestation: workflow_dispatch run 38245409846, attempt 2, same exact head, all 34 jobs successful; completed 2026-10-12T12:19:29Z. Add only the five frozen S1 outputs and independent controls, with the preregistration and D roadmap unchanged. The Lean proof body is preserved from the measured #810 design; primitive and spectator premises remain explicit. No limit availability, arbitrary pair-cone transfer or unconditional OI reconstruction is asserted.
…lability Apply only the frozen K3 roadmap splice and exact earned result template. Freeze F: 1f17f1a; F workflow_dispatch run 38245409846, successful attempt 2. S1: 031a32b; S1 workflow run 38250404107, Mathlib job 114814907712 Build and full release gate PASS. The fourteen named finite-protocol reports use exactly propext, Classical.choice and Quot.sound; the global gate reports 5874 named results without sorryAx and all 44 existing native receipts hold. Synthetic checkout 5afd0b2 has the actual S1 tree 071fba5. The frozen control plane and all S1 executable files remain unchanged. Finite availability retains its primitive and spectator premises; physical pair transfer, convergence, limit availability and unconditional OI reconstruction remain open. E requires its own all-green exact-head workflow_dispatch attestation and owner designation.
amaybaum
changed the title
Owner designated exact E ce46c20 in an explicit ChatGPT response: "Designate this exact commit as E and proceed with #812". E attestation: workflow_dispatch run 38253942780, attempt 1, all 35 jobs successful on that exact head. Named finite-protocol reports use only standard axioms; the complete release gate and owned mutation shard passed. Reconciliation first parent is main f241510; second parent is the designated E. Main has not advanced from D, so the resolved tree is exactly E, with no conflicts or additional changes. F..E and all frozen records are preserved.
Receipt-only child of actual reconciliation ce962a4. The receipt derives immutable repository facts from exact D, owner-designated F and E, actual S1, and the reconciliation. It records F workflow_dispatch 38245409846 attempt 2 and E workflow_dispatch 38253942780 attempt 1 alongside the public owner-designation commit records. No execution file, control plane, result, roadmap or historical record changes in this receipt commit. Native validity is determined by tools/v3_verifier.py --verify-round on the receipt commit, independently of hosting attestations.
amaybaum
marked this pull request as ready for review
October 12, 2026 13:53
This was referenced Oct 12, 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.
This change constructs every finite stopped-channel depth from Architecture and explicit circuit/reset/correction memberships, and proves the balanced channel formula. It adopts the minimal BridgeFiniteProtocol module, an exact checker and independent controls, one aggregate import, a kernel-only registry family and a required-success CI shard. The scoped result and K3 roadmap addition retain K3 CONDITIONAL and K2 OPEN.
Owner-designated F: 1f17f1a. Exact-head workflow_dispatch 38245409846, attempt 2: all 34 jobs succeeded before the owner designated this exact commit and instructed proceeding.
Linear execution:
S1 run 38250404107, Mathlib job 114814907712: Build and complete release gate passed; all fourteen named reports use only propext, Classical.choice and Quot.sound. The global gate reports 5874 named results without sorryAx and all 44 existing receipts hold. Logged synthetic checkout 5afd0b2 has exactly S1's tree. The entire S1 workflow concluded successfully with twenty successful jobs and one expected dispatch-only skip.
Local frozen controls pass: ten exact groups, 36 stopped matrix-unit cases, two content fixtures and 19 mutations, exact result/roadmap reconstruction, unchanged control plane and S1 files, exact file population and linear ancestry. The preserved measured proof body and existing dependencies remain unchanged. Design #813's successful tested head and consumed one-run budget remain preserved.
E attestation: exact-head workflow_dispatch 38253942780, verify #1917, attempt 1. The run completed successfully on the exact candidate E with all 35 jobs green. The fourteen named axiom reports, complete release gate and owned mutation shard passed. The owner then designated this exact E and instructed proceeding with reconciliation and receipt. Owner-designated E: ce46c20. Reconciliation Λ: ce962a4, first parent current main/D and second parent E; tree exactly E because main had not advanced. Receipt-only Q: 33abfb4. The actual Q prints VERDICT HOLDS; all 45 receipts hold and 303 legacy records remain intact. Q changes only verification/receipts/OI-FINITE-PROTOCOL-1.json. Final PR verify 38258085272 passed with twenty successful jobs and the expected dispatch-only skip. Independent scope and receipt review found no blockers. Landed via merge commit 2954989; its tree equals Q. Post-merge verification confirms all 45 receipts hold and 303 legacy records remain intact.
Primitive memberships, spectator context/label premises, convergence, limit availability, physical pair identification, arbitrary-cone validity/transfer and full-model independence remain separate obligations. The separately scoped pair-cone adoption is #811. Original design PRs remain open until their native successors land.