Repository navigation
Conversation
…rations Successor to the completed one-run #807 repair. Prospective protocol: research/finite-protocol/PROTOCOL.md, 14 named axiom reports and up to three sequential fresh-head design runs. The exact physical reset/circuit/branch controls passed before publication; the Lean module is unbuilt at this commit. All-k availability is constructed through readout, op, bind, coarse and uniformly attached discard, with primitive circuit/reset/correction memberships explicit. Arbitrary pair-cone validity and limit closedness are not supplied. No main landing, F/E attestation, frozen-record edit or shared maxCone module change.
Run38207454267 at5e57fb740496e6e851e1fcc0da13ef392016a9cf completed with Build failure; release gate skipped. Keep the first source/head/run immutable. The fourteen theorem statements and explicit primitive premises are unchanged. Correct library lemma names, numeral conjugation, residual conditionals, reset/scalar sum normalization, and the scoped exact-branch heartbeat allowance. Prospective run2 remains within the three sequential fresh-head design-run budget. Exact physical controls remain10/10 with byte-identical replay; no all-depth availability witness is introduced as a hypothesis. No shared modules, frozen records, main, or native designations are changed.
Run38208235321 at6a2e9f0e2e3a5842491767a4ff2ff1b3652335bc completed with Build failure and a skipped gate. Retain that head, its standard eleven reports and its two errors; no result is promoted over a failed Build. Move the documentation inside the scoped option, and rewrite the uniform reset to the proved pure seed before matrix simplification. The original fourteen theorem statements and primitive premises remain unchanged. This is the final run allowed by the prospective three-run design budget. No changes to #807, shared dependency modules, main, native designations or frozen records.
This was referenced Oct 12, 2026
amaybaum
added a commit
that referenced
this pull request
Oct 12, 2026
…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.
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.
Completed historical finite-protocol design. Closing without merging after native successor #812 landed OI-FINITE-PROTOCOL-1 at main commit 2954989.
Measured design head: 7081534. The three-run historical design budget and records remain unchanged; final design run 38208911901 supplied fourteen standard named reports. The native adoption preserves the measured BridgeFiniteProtocol proof body while excluding unrelated historical design modules.
Native receipt Q 33abfb4 verifies HOLDS. Its F/E exact-head dispatches passed, and its final PR checks passed. Primitive circuit/reset/correction memberships and spectator ContextStable/LabelInvariant premises remain explicit. Convergence, limiting availability, physical pair identification and arbitrary-pair preservation remain separate obligations. The design branch and measured records are retained.