Repository navigation
Conversation
Add an independent conditional B3/interface audit and signed verification of PR390 existing adapters. No admitted physical package, compiler or exponent claim. Prepared and published with substantial OpenAI Codex assistance.
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
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 adds
research/tintagel-physical-interface-audit/, an independently reproducible audit of conditional B3 composition and the boundary between homogeneous and heterogeneous helper interfaces. It gives a concrete rank-eight/rank-nine obstruction to substituting PR390's endpoints into the unchanged common-W contract, and independently re-verifies PR390's two existing signed endpoint adapters on all 512 basis columns, including global phase. It does not claim that PR390 omitted these corrections.The B3 write-up assumes a complete physical Inv/GInv package in both chronological orientations, with arbitrary joint live state and a common helper multiplier. Its owners, windows, terminal correction and conditional price are explicit. The bank-completion theorem separately retains its complete-macro, no-cross-term, scratch and coverage hypotheses.
Validation: isolated offline Python replay checks the finite identities, 35 pinned source blobs, both adapter maps, and 20 classified mutation/witness/drift controls. Fresh Lean 4.33.0 compilation reproduces 15 axiom reports for the partial structural core, using only the stated standard axioms. This does not formalize the complete physical construction. Run
python3 -I -B research/tintagel-physical-interface-audit/replay.py; optional--lean /path/to/installed/leanrepeats the partial Lean check without installation or downloads.The contribution credits Jacob Sussman's route/window framework, the existing B_K schedule and PR377/381 lineage, PR390's adapters, and PR401/404/405 normalization and bank work.
NOVELTY.mdrecords the bounded comparison with PR406–412 bodies and proof summaries and PR413–416 bodies. Those implementations and full proof chains were not verified here; reported legacy-checker allegations are not adopted as audit findings. No priority claim is made for existing mechanisms.This is an audit and regression supplement, not an admitted physical provider, new compiler, full PR390 changed-walk/backward-program certification, cost improvement or exponent result. Mathematical statements, proofs, source bytes and expected results retain the reviewed revision's content. Private review and candidate transcripts are excluded; review provenance and the response summary remain. Prepared with substantial OpenAI Codex assistance; the earlier private static review and fresh executed checks are distinct evidence routes.