Repository navigation
OI-PAIR-MAXCONE-1: adopt conditional pair-cone theorem - #811
Merged
Merged
Conversation
…invariants before freeze
…tive design validation
…nt before design CI
…untercontrols before design CI
…nd freeze two-location controls
…design run before freeze
Owner designated exact F ef486aa in ChatGPT and instructed proceeding with #811. F attestation: workflow_dispatch run 38245407074, attempt 1, all 34 jobs successful on that exact head. Add only the twelve byte-frozen S1 files and the frozen controls.py. Preserve the preregistration and D roadmap unchanged. The kernel package is conditional; physical pair sourcing and K2 remain open.
…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.
…h K2 roadmap locations Execute frozen S2 as a single child of actual S1 b6fc713. F is ef486aa, attested by workflow_dispatch run 38245407074 attempt 1. S1 evidence is run 38250344438 Mathlib job 114814706272: sixteen standard named MaxCone axiom reports and the complete release gate pass; its tested tree matches actual S1. Add only the exact frozen result template and the two specified ROADMAP replacements. K2 stays OPEN; physical pair sourcing and all other obligations retain their scope. No control-plane file changes. E is not designated by this commit.
…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.
Adopt the native non-sealing finite-protocol round from its owner-designated F and E. Both exact-head dispatch attestations are successful; all 35 E jobs are green. Receipt-only Q 33abfb4 verifies HOLDS, all 45 receipts hold, and final PR verify 38258085272 passed. Architecture, primitive memberships and spectator premises remain explicit. Convergence, limit availability, physical pair identification and arbitrary-cone preservation remain separate obligations. K3 remains CONDITIONAL and K2 remains OPEN.
…main The owner replied "Proceed as suggested" to the explicit request to designate exact 6a7696a as E for #811 and proceed, after the frozen lower-inclusion wording slip was described. This is the actual reply and its exact-object context. E attestation: workflow_dispatch run 38253938894, attempt 1, all 35 jobs successful on that exact head. The sixteen named MaxCone reports use only standard axioms; the complete release gate and owned mutation shard pass. First parent is accepted main 2954989, carrying OI-FINITE-PROTOCOL-1; second parent is designated pair E. Resolve by merits all four shared files: preserve both workflow shards and required-success wiring, both kernel-only families, both aggregate imports, finite's K3 paragraph and pair's K2 paragraph plus queue summary. Finite owned files, frozen records and receipt remain byte-identical to main; pair owned files and frozen records remain byte-identical to E. The frozen result's abbreviated lower-inclusion sentence omits block invariance. The lower inclusion requires products, addition, nonnegative scaling AND block invariance, as the frozen scope table and Q3_subset_of_products_cone_block state explicitly. The full generator theorem supplies block invariance from its stated CNOT/full-flow/cyclic premises. Preserve the frozen control plane and result rather than modifying them after F. K2 stays OPEN and K3 CONDITIONAL; no physical sourcing or unconditional reconstruction is promoted.
…otocol main Add only the non-sealing receipt as a single child of actual reconciliation 82a1d18. The receipt names exact owner-designated F and E, successful exact-head workflow_dispatch attempts, and all four merits-resolved shared paths. The owner E attestation links to the published reconciliation carrying the literal reply and exact-object context. Both rounds' records and the reconciled executable tree remain unchanged. Exact-object landing authorization is a separate final step required by the frozen preregistration; this receipt commit does not grant it.
amaybaum
marked this pull request as ready for review
October 12, 2026 17:19
amaybaum
added a commit
that referenced
this pull request
Oct 12, 2026
The owner authorized merging this editorial follow-up after updating from main, retaining #811's census family, confirming the diff is exactly two wording lines, and obtaining fresh green CI. The updated head fe994df satisfies those conditions. Fresh PR run 38283803926 passed 21 jobs with one expected workflow_dispatch-only skip, testing the updated head's exact tree. The complete release gate passes; all 46 receipts hold and all 303 legacy records remain intact. Independent review confirms only the finite census note and one Lean doc comment change; theorem statements, proofs, premises, pair family and frozen records are preserved.
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.
The earlier pair-cone forcing theorem assumed self-duality H3. This adoption proves the conditional replacement from product preparation, addition and nonnegative scaling, product-test positivity, CNOT invariance and full rotation/cyclic invariance. It adopts seven conditional Lean modules, an exact rational checker/support, a kernel-only census family and a required-success CI shard. K2 remains OPEN.
Owner-designated F:
ef486aa48c445db2264d7a7f8b22520af743e4a9; exact-head dispatch 38245407074, attempt 1, all 34 jobs green before designation. S1b6fc7139659227b3f8170e0e8926945791976276adds the thirteen frozen output/control files. S2 is owner-designated E6a7696a050f6d3fd9e16a9fb17665cbe01b4b3be; exact-head dispatch 38253938894, attempt 1, all 35 jobs green. Sixteen named MaxCone reports use only standard axioms; the complete release gate and owned mutation shard pass.Reconciliation Λ:
82a1d18d5ae08d9d528fb1f8e80ad71c9a35f4d1, ordered parents accepted #812 main2954989a40bb2807d3432e13cf671d698295124fand E. The four shared files preserve both rounds' owned workflow, census, import and roadmap changes. Both round record directories and the accepted finite receipt remain unchanged. Independent reconciliation review is clean. The commit quotes the owner's actual reply “Proceed as suggested” and its exact-E context.Receipt-only Q:
09c3b69e3580ae21d1bc91e8d2e7a510e0ea00cf, sole parent Λ. The actual published object verifiesVERDICT HOLDS; all 46 receipts hold and all 303 legacy records in 75 closed namespaces remain intact. The verifier corpus/self-tests, receipt-builder self-test, pair 2743 exact checks, three checker mutations, two content fixtures/26 mutations and finite S1/S2 fixtures/19 mutations passed. PR run 38280094362 completed successfully: 21 successful jobs and one expected dispatch-only skip. Mathlib's logged synthetic checkout has Q's exact tree; sixteen pair and fourteen finite-protocol reports use only standard axioms, the global gate reports 5981 named results without sorryAx, and the complete release gate passes with all 46 receipts holding. Final independent actual-Q review is clean. The owner authorized this exact Q after independent review. #811 landed through an ordinary merge at accepted main9fea39a46f3c03baadde93d1118fcc45385ccbfb, whose tree is exactly Q's. Post-merge checks confirm all 46 receipts hold and all 303 legacy records remain intact.The frozen result's abbreviated lower-inclusion sentence omits block invariance. The reconciliation message records the omission; the frozen scope table and
Q3_subset_of_products_cone_blockstate the complete premises. Frozen wording remains intact. Historical #809's three-run design budget and 25-mutation evidence are preserved; #811's additional stale-summary check gives 26 mutations.Physical state/test identification, actual pair validity and operation preservation, limit-route closure, arbitrary finite-carrier reconstruction and full-model independence remain open. #812 is accepted; editorial follow-up #815 has also landed its two live terminology corrections while preserving both rounds' frozen records. #809 is now closed without merging; its measured design head and historical evidence remain preserved.