From 080e8366d98be7e9dc97d5f57f64f60017a474e7 Mon Sep 17 00:00:00 2001 From: CubeJerry <80299683+CubeJerry@users.noreply.github.com> Date: Sat, 31 Oct 2026 13:12:46 +0800 Subject: [PATCH] Prove event-specific phase obstruction in the selected P104 word Prepared for @CubeJerry with substantial OpenAI Codex assistance. No new kappa; all selected framework assumptions remain. --- .../role-phase-compatibility/PORTABILITY.json | 81 ++++++ research/role-phase-compatibility/PROOF.md | 184 +++++++++++++ research/role-phase-compatibility/README.md | 95 +++++++ research/role-phase-compatibility/RESULT.json | 171 ++++++++++++ .../role-phase-compatibility/SOURCES.json | 60 ++++ research/role-phase-compatibility/TASK.json | 130 +++++++++ .../role-phase-compatibility/VALIDATION.md | 72 +++++ research/role-phase-compatibility/VERIFY.json | 63 +++++ .../role-phase-compatibility/independent.py | 150 ++++++++++ research/role-phase-compatibility/verify.py | 260 ++++++++++++++++++ 10 files changed, 1266 insertions(+) create mode 100644 research/role-phase-compatibility/PORTABILITY.json create mode 100644 research/role-phase-compatibility/PROOF.md create mode 100644 research/role-phase-compatibility/README.md create mode 100644 research/role-phase-compatibility/RESULT.json create mode 100644 research/role-phase-compatibility/SOURCES.json create mode 100644 research/role-phase-compatibility/TASK.json create mode 100644 research/role-phase-compatibility/VALIDATION.md create mode 100644 research/role-phase-compatibility/VERIFY.json create mode 100644 research/role-phase-compatibility/independent.py create mode 100644 research/role-phase-compatibility/verify.py diff --git a/research/role-phase-compatibility/PORTABILITY.json b/research/role-phase-compatibility/PORTABILITY.json new file mode 100644 index 0000000000..9c253099bc --- /dev/null +++ b/research/role-phase-compatibility/PORTABILITY.json @@ -0,0 +1,81 @@ +{ + "actual_export_corruptions_rejected": [ + { + "last_error": "ValueError: Source bytes: research/p104-helper470-twin-rung-removal/WORD.json.gz", + "mutation": "word", + "optimized": false + }, + { + "last_error": "ValueError: Source bytes: research/p104-helper470-twin-rung-removal/WORD.json.gz", + "mutation": "word", + "optimized": true + }, + { + "last_error": "ValueError: Source bytes: research/p104-native-channel/vendor/clifford_exact.py", + "mutation": "native", + "optimized": false + }, + { + "last_error": "ValueError: Source bytes: research/p104-native-channel/vendor/clifford_exact.py", + "mutation": "native", + "optimized": true + }, + { + "last_error": "ValueError: Exact declared input set", + "mutation": "manifest", + "optimized": false + }, + { + "last_error": "ValueError: Exact declared input set", + "mutation": "manifest", + "optimized": true + }, + { + "last_error": "ValueError: Exact retained result", + "mutation": "result", + "optimized": false + }, + { + "last_error": "ValueError: Exact retained result", + "mutation": "result", + "optimized": true + } + ], + "export_files_unchanged": 13, + "input_sha256": { + "research/p104-helper470-twin-rung-removal/WORD.json.gz": "7834725d9e34ee846a9ccc615221ea81e0201613938afa185d2eda0c9a6c232f", + "research/p104-native-channel/vendor/clifford_exact.py": "2982ead07721e83358dc67c6f49c2b4c16a236a6bebdfd72f58221be1f5d0962", + "research/p104-native-channel/vendor/native_verify.py": "3049471905b47b385c88378a1a3be7a18b8858aadd035b8a6da2f4a03b470f38" + }, + "runs": [ + { + "marker": "PASS_ROLE_PHASE_COMPATIBILITY events=14 contacts=8 moves=6 iff_four_divides_width", + "optimized": false, + "script": "verify.py" + }, + { + "marker": "PASS_ROLE_PHASE_COMPATIBILITY events=14 contacts=8 moves=6 iff_four_divides_width", + "optimized": true, + "script": "verify.py" + }, + { + "marker": "PASS_INDEPENDENT_ROLE_PHASE columns=9 contacts=8 relaxed_graphs=32", + "optimized": false, + "script": "independent.py" + }, + { + "marker": "PASS_INDEPENDENT_ROLE_PHASE columns=9 contacts=8 relaxed_graphs=32", + "optimized": true, + "script": "independent.py" + } + ], + "scientific_file_sha256": { + "RESULT.json": "62c74b438e5293758b5861d015323af4d11f893d4c80321047bafa0fab39377a", + "SOURCES.json": "b57b8cd601d23db80d9c5463732d8db45d0c3a46fa4943a80453d48b42a4c351", + "VERIFY.json": "e40a2768804fe4a7b3dc78275b5be4148d4bd784ece11fe6e4850fc98a474a0e", + "independent.py": "2da514b34c87d4ba4ffeaa9a3fe9151d4adfd1309704e26e338078f56838345d", + "verify.py": "82b0afe8519bad89c7414060171f1c3e872949df84b74ca4d9dd466928995b0c" + }, + "scope": "Scientific executable/input bytes are unchanged by this validation-record addition; complete final tree and publication checks remain separate.", + "tested_commit": "5a84b1d25f782185587f1251b200d9e08768711c" +} diff --git a/research/role-phase-compatibility/PROOF.md b/research/role-phase-compatibility/PROOF.md new file mode 100644 index 0000000000..4d9e200e65 --- /dev/null +++ b/research/role-phase-compatibility/PROOF.md @@ -0,0 +1,184 @@ +# Event-specific phases in the reached selected word + +## Claim and contract + +Fix a positive column multiplicity `f`. The selected #6030 scalar word is +`research/p104-helper470-twin-rung-removal/WORD.json.gz`, SHA256 +`7834725d9e34ee846a9ccc615221ea81e0201613938afa185d2eda0c9a6c232f`. +A MOVE from chart `a` to chart `b` has retained native normal form + +``` +T_ab = C_b C_a† = i^p S_ab, +``` + +where `S_ab` is the same literal recipe with its explicit `phase` gates +deleted. All other gates and their order are fixed. Its factorwise width-f +interpretation is `T_ab^(tensor f) = i^(pf) S_ab^(tensor f)`. + +Permit a separate scalar gauge `lambda_(r,t)(f)` of modulus one for each +role and each program cut. It may depend on role, event history and width, +but not on the numerical input. The proposed implementation deletes every +MOVE phase tag and leaves every scalar ADD/COPY/SCALE coefficient and every +other operation unchanged. At each cut its role values must equal the original +role values multiplied by these gauges. Public input/output gauges are entirely +free. A zero role may change its gauge freely; an owned reset does not carry a +phase constraint through an absent or identically zero value. + +**Theorem.** Such a gatewise gauge equivalence for the selected word exists +if and only if `4 | f`. Necessity already follows from fourteen reached events, +with no public endpoint or owned-lifecycle constraint. It remains true after +all constraints at dependent nonzero ADDs are dropped. + +This is an obstruction to a specific gauge remedy, not a defect in the correct +phase-preserving source. Endpoint-only resynthesis, changed native recipes, +changed scalar coefficients, data-dependent recodings and rounded approximate +identities are outside the theorem. No global minimum number of phase tags is +asserted. + +## Why an actual independent ADD constrains three gauges + +Use canonical-chart coordinates: the original value of a role in chart `a` +is `C_a^(tensor f) sum_j R_j x_j`, for arbitrary independent input arrays `x_j`. +The rational row `R` starts as a coordinate vector. A MOVE changes its chart +and leaves its row unchanged; a common-chart scalar gate performs its indicated +rational row operation. This is the source's exact chart interpretation. + +Consider `target += c * source`, `c != 0`, whose two pre-event rows are +linearly independent. The two operand arrays may be chosen independently: +a nonzero two-column minor gives an invertible rational map from two arbitrary +input arrays to those operands, with all other arrays zero. The common chart +is invertible, at any positive tensor width. Let `a,b` be the operand arrays. +Gatewise gauge equivalence requires + +``` +lambda_after (a + c b) = lambda_before a + c lambda_source b +``` + +for every `a,b`. Setting either operand to zero proves +`lambda_after = lambda_before = lambda_source`. This proof actually permits +any nonzero complex scalar gauges. Modulus one is retained as the stated phase +contract. Nonzero operands alone are not used as an independence test. + +A MOVE on a nonzero row requires +`lambda_after = i^(-pf) lambda_before`. An untouched nonzero role keeps its +gauge, because its actual stored value is unchanged. A nonzero SCALE also keeps +its gauge. These are exact necessary relations; no numerical sampling is used +to extend them to arbitrary inputs or arbitrary `f`. + +## Eight reached independence certificates + +All event numbers and input-column numbers below are zero-based. The complete +prefix through event 9997 is replayed over rational rows. In every displayed +minor the first row is the pre-ADD target row and the second is the source row. +All eight determinants are `+1` or `-1`. + +| Event | Literal ADD | Columns | Two-column minor | +|---:|---|---|---| +| 8255 | `229 -= 227` | 229, 227 | `diag(1,1)` | +| 9031 | `225 += 227` | 225, 227 | `diag(-1,1)` | +| 9034 | `231 += 225` | 231, 225 | `diag(1,-1)` | +| 9916 | `229 += 87` | 229, 87 | `diag(1,1)` | +| 9924 | `231 += 27` | 231, 27 | `diag(1,1)` | +| 9982 | `229 += 238` | 229, 238 | `diag(1,1)` | +| 9983 | `231 += 236` | 231, 7 | `diag(1,1)` | +| 9997 | `231 += 229` | 231, 81 | `diag(1,1)` | + +The second checker separately streams nine input columns through all 9,998 +prefix events using integer dyadic arithmetic, without the primary row engine +or `Fraction`. It obtains the same minors. These are certificates of the +specific reached rows; they do not assume that every pair of public roles stays +independent at every cut. + +## Two actual histories and the closing contact + +After event 8255, role 229 has the phase of role 227. Role 227 has no write +between events 8255 and 9031. Event 9031 therefore gives role 225 that same +phase. Role 225 has no write before it is read at event 9034, which gives role +231 the same phase. Call this shared, arbitrary nonzero phase `lambda`. + +The only writes to roles 229 and 231 between those acquisition events and +event 9997 are the following. The intervening ADDs are precisely the certified +rank-two contacts above and cannot refresh the receiver's phase. + +| Role | Chronological MOVE events | Chart path | Literal phase exponents | +|---:|---|---|---| +| 229 | 9904, 9938, 9994 | `3 -> 81 -> 254 -> 259` | `1, 0, 0` | +| 231 | 9901, 9955, 9987 | `3 -> 25 -> 256 -> 259` | `1, 1, 0` | + +Every one of these six native calls has rank one. The literal bases are + +``` +3: () 25: (38,) +81: (493,) 254: (51,478) +256: (21,38) 259: (21,38,459). +``` + +Consequently immediately before event 9997, + +``` +lambda_229 = i^(-f) lambda, +lambda_231 = i^(-2f) lambda. +``` + +The independent ADD at 9997 forces these two phases to coincide. Since +`lambda != 0`, this implies `i^f = 1`, or exactly `4 | f`. +No boundary-normalizer assumption appears in this contradiction. Free initial +phases, free final phases, different phase choices for every role occurrence, +and arbitrary gauge freedom at all omitted dependent ADDs cannot repair it. + +Conversely, when `4 | f`, the tensor factor of every explicit native `phase` +gate in the retained alphabet is one. The trivial gauge makes phase deletion +identical to the original factorwise interpretation of every MOVE, with every +scalar gate unchanged. This uses the retained literal integer phase alphabet; +it does not require a new census or physical all-column admission. + +## Separate native checks and the local repair boundary + +The source compiler lowers the six operators and reports the phase exponents +above. A separate exact Gaussian-dyadic interpreter compares every one of the +512 basis columns of each lowered recipe against its literal chart expression. +For the two three-MOVE paths `A` (role 229) and `B` (role 231), it also checks +all 512 columns of + +``` +T_A† T_B = I, S_A† S_B = -i I. +``` + +This is a check on the MOVE paths as operators; the actual chronological +histories also contain the ADDs and are handled by the row/gauge argument. +It is not presented as a six-MOVE contiguous source subroutine. + +Changing the final ADD coefficient from `1` to `i^(-f)` would reconcile these +two local phase labels: in the transformed coordinates its coefficient must +be `lambda_231/lambda_229`. This illustrates why unchanged scalar coefficients +are a substantive hypothesis. It does not repair or price the entire word. +Other contacts and normalizers remain to be checked, and a scalar phase +operation has its own physical and precision contract. + +## Scope, credit and remaining assumptions + +Nick Petalas's #6298 supplied the shared-frame triangle, its exact width +criterion and the explicit role/history-gauge open question. Unpaidmoon's +#6293 supplied the selected MOVE census and tensor-phase question. This result +adds a reached causal constraint cycle with certified independent operands; +it does not repeat either complete census. Nick Petalas's #6025 classifies +fixed nonlinear role recodings under a different all-independent-input +contract; occurrence-dependent phases and the selected reached graph are the +scope here. The elementary cycle-potential argument is classical. + +Credit DreamingOfClouds (#6030/#5907), Ali Romman (#5827/#5599 and the +independent Gaussian interpreter in #1862/#1931), Chafik Boukhalfa's native +channel, icekylinx's retained frame compiler, DLamdata (#5894), Matarener +(#5974/#5442), Rohan Arun (#1972), Adam Gall (#1940), Josie Elliston (#1071), +and the native/controller/compiler/precision lineage retained in those sources. +The exact inputs remain unchanged. Prepared for @CubeJerry with substantial +OpenAI Codex assistance, including separately written row/column checks and +lead review. Apache-2.0. + +No new kappa, paid-profile improvement, supplier admission or selected-frontier +change is claimed. The five assumptions `native_all_columns`, `owned_erasure`, +`compiler`, `precision_tape` and `analytic_recovery` remain. In particular this +scoped theorem uses the exact common-chart and factorwise tensor contract; +it does not independently establish every selected native map, machine tariff, +rounded multiplier, storage bound or outer analytic theorem. No independent +human or proof-kernel verification is claimed. diff --git a/research/role-phase-compatibility/README.md b/research/role-phase-compatibility/README.md new file mode 100644 index 0000000000..46d345271c --- /dev/null +++ b/research/role-phase-compatibility/README.md @@ -0,0 +1,95 @@ +# Role-specific phases cannot remove the selected MOVE tags + +Allowing a separate phase chart for every role and every event still cannot +remove all explicit MOVE phase tags while retaining the selected #6030 scalar +coefficients, unless the column multiplicity is divisible by four. This answers +the role/history-gauge question left open by #6298. **No new κ.** + +The obstruction uses fourteen actual events: eight ADDs with independently +certified rank-two operand rows and six rank-one MOVEs. Two roles acquire the +same phase, follow paths with phase sums one and two, and then meet in an +independent ADD. Even arbitrary public endpoint gauges and freedom at all +omitted dependent ADDs cannot reconcile that contact. The unchanged, correct +phase-preserving implementation is not challenged. + +[PROOF.md](PROOF.md) gives the all-input, all-width argument, the exact event +and minor tables, and the boundary of a possible changed-coefficient remedy. +[RESULT.json](RESULT.json) is a generated source-bound certificate. Base: +`a7638a4ce2a29947457ae8d6bf8cd70a234dfeac`; exact Git/SHA256 inputs and historical +question pins are in [SOURCES.json](SOURCES.json) and [TASK.json](TASK.json). + +## Reproduce + +From the repository root with CPython 3.12 and the standard library: + +```sh +python3 -B scripts/research_package.py --package research/role-phase-compatibility +``` + +Expected: `PASS_ROLE_PHASE_COMPATIBILITY`, `PASS_INDEPENDENT_ROLE_PHASE` and +`PASS_REGISTERED_RESEARCH_PACKAGE`. The registered commands run both scientific +checkers normally and with assertions disabled. Direct replay: + +```sh +python3 -I -W error -B research/role-phase-compatibility/verify.py +python3 -I -W error -B research/role-phase-compatibility/independent.py +``` + +The primary replays 9,998 events over 770 independent rational input rows, +certifies all eight minors, compiles the six MOVE recipes, checks their 3,072 +basis columns using a separate exact interpreter, and checks both 512-column +relative path operators. Twelve rejecting controls cover changed source bytes, +contacts, hidden writes, false phase/sign claims, missing rank-two hypotheses +and omitted compensating coefficients. Open-tree and width-four controls pass. + +The separate checker streams nine columns through 89,982 event applications +using integer dyadics, then solves a relaxed event-gauge graph at widths 1–32. +Every nonwitness write receives a free phase variable. Dropping the closing ADD +or altering the path phase makes all 64 control graphs consistent. The written +proof establishes arbitrary width and arbitrary unit-complex gauges; these +finite graph checks are corroboration. + +[VALIDATION.md](VALIDATION.md) records checks actually executed and their limits. +Default replays write no files. `verify.py --write-result` is the certificate +generator and refuses to overwrite an existing result. Authenticated native +source is compiled directly from its bytes, preventing a stale bytecode cache +from replacing the checked source in direct replay. + +## Novelty and limitations + +#6298's triangle allowed one phase per frame and used edges on different roles. +Here the contradiction survives a phase per role per event and is justified on +the actual reached operand rows. #6293's phase census is retained credit, not +new coverage. #6025's fixed nonlinear role recodings use a different contract. +The archive/PR survey was targeted, not exhaustive; active #6322–#6325 address +different helper and G20 questions. The publication checkpoint is recorded in +TASK.json. + +The result is a scoped gauge obstruction, not a lower bound for all native +resyntheses. It fixes all other recipe gates and all scalar coefficients, +requires gatewise exact gauge equivalence, and excludes data-dependent gauges. +No complete-word phase-deletion endpoint audit, minimum tag count, physical +scalar tariff, selected cold replay, hosted CI, Lean or Docker is claimed. +All five selected framework assumptions remain. The selected conditional +κ = 0.003125804 is unchanged. + +## Open next questions + +Can changed scalar phases and endpoint normalizers yield a cheaper complete +implementation? The first step is to propagate one legal phase assignment +through the entire word, emit every changed ADD/COPY coefficient and boundary +normalizer, and charge their native/scalar/precision costs. A repair of the +single closing ADD is only a local compatibility example, not such a program. +This package stops at the fourteen-event certificate; no global phase-cost +optimization is reserved. Structured scope and blockers are in TASK.json. + +## Attribution + +Prepared for @CubeJerry with substantial OpenAI Codex assistance in derivation, +implementation and independent column/graph checking, with lead review. +Credit Nick Petalas (#6298/#6025), unpaidmoon (#6293), DreamingOfClouds +(#6030/#5907), Ali Romman (#5827/#5599/#1862/#1931), Chafik Boukhalfa, +icekylinx, DLamdata (#5894), Matarener (#5974/#5442), and the retained source +lineage listed in PROOF.md. Classical gauge-cycle and tensor-phase facts retain +their usual attribution. Apache-2.0. No independent human or formal proof-kernel +review is claimed. diff --git a/research/role-phase-compatibility/RESULT.json b/research/role-phase-compatibility/RESULT.json new file mode 100644 index 0000000000..7b4f151067 --- /dev/null +++ b/research/role-phase-compatibility/RESULT.json @@ -0,0 +1,171 @@ +{ + "gauge_counts_widths_1_to_4": [ + 0, + 0, + 0, + 4 + ], + "independent_adds": { + "8255": { + "columns": [ + 229, + 227 + ], + "determinant": "1", + "matrix": [ + [ + "1", + "0" + ], + [ + "0", + "1" + ] + ] + }, + "9031": { + "columns": [ + 225, + 227 + ], + "determinant": "-1", + "matrix": [ + [ + "-1", + "0" + ], + [ + "0", + "1" + ] + ] + }, + "9034": { + "columns": [ + 231, + 225 + ], + "determinant": "-1", + "matrix": [ + [ + "1", + "0" + ], + [ + "0", + "-1" + ] + ] + }, + "9916": { + "columns": [ + 229, + 87 + ], + "determinant": "1", + "matrix": [ + [ + "1", + "0" + ], + [ + "0", + "1" + ] + ] + }, + "9924": { + "columns": [ + 231, + 27 + ], + "determinant": "1", + "matrix": [ + [ + "1", + "0" + ], + [ + "0", + "1" + ] + ] + }, + "9982": { + "columns": [ + 229, + 238 + ], + "determinant": "1", + "matrix": [ + [ + "1", + "0" + ], + [ + "0", + "1" + ] + ] + }, + "9983": { + "columns": [ + 231, + 7 + ], + "determinant": "1", + "matrix": [ + [ + "1", + "0" + ], + [ + "0", + "1" + ] + ] + }, + "9997": { + "columns": [ + 231, + 81 + ], + "determinant": "1", + "matrix": [ + [ + "1", + "0" + ], + [ + "0", + "1" + ] + ] + } + }, + "input_sha256": { + "research/p104-helper470-twin-rung-removal/WORD.json.gz": "7834725d9e34ee846a9ccc615221ea81e0201613938afa185d2eda0c9a6c232f", + "research/p104-native-channel/vendor/clifford_exact.py": "2982ead07721e83358dc67c6f49c2b4c16a236a6bebdfd72f58221be1f5d0962", + "research/p104-native-channel/vendor/native_verify.py": "3049471905b47b385c88378a1a3be7a18b8858aadd035b8a6da2f4a03b470f38" + }, + "loop_basis_columns": 512, + "native_basis_column_comparisons": 3072, + "native_move_phases": { + "9901": 1, + "9904": 1, + "9938": 0, + "9955": 1, + "9987": 0, + "9994": 0 + }, + "no_new_kappa": true, + "path_phase_sums_mod4": [ + 1, + 2 + ], + "prefix_events": 9998, + "rejecting_controls": 12, + "schema": "role-phase-compatibility/1", + "stripped_relative_loop": "-i I", + "witness_event_count": 14 +} diff --git a/research/role-phase-compatibility/SOURCES.json b/research/role-phase-compatibility/SOURCES.json new file mode 100644 index 0000000000..32724214fb --- /dev/null +++ b/research/role-phase-compatibility/SOURCES.json @@ -0,0 +1,60 @@ +{ + "schema_version": 1, + "base_commit": "a7638a4ce2a29947457ae8d6bf8cd70a234dfeac", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "d59b5035e7b4cbaa9d688a1d32dd0d6eb79c466a", + "sha256": "9b8d0eea95b3bf0dfcb7938a732a6439b87a2685dec2a5ab9e525b3b34debbfa" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec", + "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81" + }, + { + "path": "research/p104-helper470-twin-rung-removal/WORD.json.gz", + "usage": "input", + "git_blob": "22f9ab02d1b73ea0aa4b07ce445a14cc2602c760", + "sha256": "7834725d9e34ee846a9ccc615221ea81e0201613938afa185d2eda0c9a6c232f" + }, + { + "path": "research/p104-native-channel/vendor/clifford_exact.py", + "usage": "input", + "git_blob": "166841a037f069249f6f7f6dedb89248812f59e2", + "sha256": "2982ead07721e83358dc67c6f49c2b4c16a236a6bebdfd72f58221be1f5d0962" + }, + { + "path": "research/p104-native-channel/vendor/native_verify.py", + "usage": "input", + "git_blob": "2c209dfa9cfade3bc20ac5fc9d876b433a147f8c", + "sha256": "3049471905b47b385c88378a1a3be7a18b8858aadd035b8a6da2f4a03b470f38" + }, + { + "path": "research/move-frame-phase-obstruction/PROOF.md", + "usage": "provenance", + "git_blob": "472b07707f495e6abebbc41b42c268b5d40ab10b", + "sha256": "98b7a2eb4e15d7f3983b71b66cb65c2bcd8392e85740777ab55a3fda340d7584" + }, + { + "path": "research/move-frame-phase-obstruction/TASK.json", + "usage": "provenance", + "git_blob": "4f564fb6cdcd395cc460204f88513a29aae85000", + "sha256": "f45b514d1c715c011d53f393067cb774a6ca0fa1322a320ced237c3637b06843" + }, + { + "path": "research/move-chart-phase-power/PROOF.md", + "usage": "provenance", + "git_blob": "59358df2f1e43a2e91c5781c9ef7c24465559c0c", + "sha256": "c6015f52899d7bf9679d1aacefcd49ef0276b03375c6876def6b65ecaf060369" + }, + { + "path": "research/nonlinear-role-recoding/README.md", + "usage": "provenance", + "git_blob": "a13e9f1c5a2997922340f543fbfb9d3b75509f4c", + "sha256": "e6f15d9b4a47bde8b6cf230d7c74a3818c7051772106e1b7ef1c3ad71418d11a" + } + ] +} diff --git a/research/role-phase-compatibility/TASK.json b/research/role-phase-compatibility/TASK.json new file mode 100644 index 0000000000..418a5cf9af --- /dev/null +++ b/research/role-phase-compatibility/TASK.json @@ -0,0 +1,130 @@ +{ + "schema_version": 1, + "task_id": "uniform-transfer-audit", + "priority_revision": 8, + "base_commit": "a7638a4ce2a29947457ae8d6bf8cd70a234dfeac", + "original_card": { + "id": "uniform-transfer-audit", + "question": "Can one of the selected record's five inherited assumptions be proved at its actual caller?", + "starting_points": [ + "docs/research/current-priorities.md", + "docs/research/research-family-status.md", + "certificates/selected-result.json", + "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md" + ], + "methods": [ + "Construct and independently check one source-bound instance of the stated first experiment.", + "Seek an exact counterexample or target-specific complete-budget obstruction to that same proposed change." + ], + "acceptance_gate": "Identify the proposition and what would change downstream; do not equate a finite replay with a universal proof.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_selected_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read revision 8, the selected review and live exact-source handoffs. Then follow this card's bounded first_experiment.", + "scope": "Source-bound orientation only, not a supplier replay or theorem proof." + }, + "first_experiment": "Choose one assumption ID (native_all_columns, owned_erasure, compiler, precision_tape, analytic_recovery), one quantified implication and exact dependency closure. Check current handoffs, including #5625 row reentry and #5707 root-prefix lowering, without treating their partial scope as the whole theorem. Prove or falsify that implication with a caller-bound argument; stop at the chosen obligation. Finite tests or root digits do not discharge an all-size statement.", + "bottleneck_link": "Judge the actual current supplier contract and complete signed target/paid bill; frozen-profile ceilings require an applicability proof.", + "allowed_variations": [ + "One exact source head, helper/cut region or quantified proposition and changed hypothesis; check live handoffs first. Different seeds are not different scopes." + ], + "scope_change_triggers": [ + "Changing source head, helper/cut domain, operation alphabet or caller boundary without recording the new scope.", + "Treating an archived proposal or local numerical pass as complete supplier admission." + ], + "overlap_terms": [ + "native_all_columns", + "owned_erasure", + "compiler", + "precision_tape", + "analytic_recovery" + ], + "existing_checks": [ + { + "scope": "PR #4100: proposed unconditional construction and finite checks, without independent acceptance.", + "evidence": "research/unconditional-batched-crt/README.md", + "remaining": "Independent proof audit of one caller-bound all-size implication; all other premises remain explicit.", + "status": "author-checked", + "source_commit": "337d04939571a637aeab54a0f58f54fde811663a", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "Selected PR5599: complete helper-subspace construction and independent caller replay; five framework assumptions remain.", + "evidence": "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md", + "remaining": "The next experiment must identify uncovered source-specific work. Successor archive intake does not transfer this admission.", + "status": "reviewed", + "source_commit": "09dd0965711ca7eeb169057a420abab1c9052137", + "selected_record_sha256": "2a0220e866417774606e0f991e41b9c1d26b1f43b97857238cf478dbc7d330b5" + } + ] + }, + "scope_status": "refined", + "actual_scope": "Prove or refute role- and event-specific scalar gauges deleting the literal MOVE phases of the selected #6030 word while retaining actual scalar coefficients.", + "scope_change_reason": "Follow the explicit role/history-gauge question of #6298, allowing free endpoint gauges and dropping dependent-ADD constraints; certify reached rank-two contacts rather than assume generic local independence.", + "bottleneck_link": "Determines whether a concrete native_all_columns phase-bookkeeping obligation disappears under a more permissive chart representation; it does not discharge native admission.", + "budget_minutes": 75, + "stop_rule": "Stop at one exact reached contradiction or a fully compatible phase assignment; no global phase-cost search.", + "outcome": "completed", + "evidence": "Fourteen-event certificate: eight rank-two ADDs, six rank-one MOVEs, path phase sums 1 and 2 modulo four; independent dyadic column/graph check.", + "author": "@CubeJerry", + "ai_assistance": "Substantial OpenAI Codex assistance, including separately written rational-row and integer-dyadic column/graph checks; lead review. No independent human or proof-kernel review.", + "open_questions": [ + { + "question": "Can changed scalar phases and endpoint normalizers reduce the complete implementation cost?", + "why_it_matters": "The unchanged-coefficient phase-gauge escape is excluded, but relocating phase operations could trade native and scalar work.", + "first_step": "Emit a complete legal phase assignment with every changed ADD/COPY coefficient and endpoint normalizer, then compare the full physical invoice.", + "blocked_by": "No complete changed word, phase-cost optimum, physical scalar tariff, precision/restoration accounting or supplier admission is supplied." + } + ], + "overlap": { + "searched": "Exact question source #6298, #6293, fixed nonlinear comparison #6025, active root survey and role/phase PR search at base.", + "coverage": "Targeted archive and live-PR searches; not exhaustive. No equivalent event-specific selected-row certificate located.", + "excluded_active_prs": [ + 6322, + 6323, + 6324, + 6325 + ] + }, + "checkpoint": { + "upstream_base": "a7638a4ce2a29947457ae8d6bf8cd70a234dfeac", + "priority_revision": 8, + "selected_kappa": "0.003125804", + "source_baseline_retained": true + }, + "predecessors": [ + { + "number": 6298, + "head": "e2bec73e3f50e3b4e57a7a466eba2a3264d313ed", + "state": "closed", + "merged": true, + "title": "Prove scalar frame gauges cannot remove selected MOVE phases (no \u03ba)" + }, + { + "number": 6293, + "head": "a3df7015a9571752430314afdaf5212704b2f5dc", + "state": "closed", + "merged": true, + "title": "Record that selected MOVE absolute phases scale as i^{p f}" + }, + { + "number": 6025, + "head": "e15e504b2ce847923792cb6178f6f49903df472c", + "state": "closed", + "merged": true, + "title": "Classify fixed nonlinear role recodings under exact ADD compatibility (no new \u03ba)" + }, + { + "number": 6030, + "head": "772dd10a5859a1d15f4851feb371519789213ad8", + "state": "closed", + "merged": true, + "title": "Conditional \u03ba .003125804 (+5.22e-7 over #5907): remove helper 470's frame-593 rung, the twin of #5907's removal" + } + ], + "attribution": "@CubeJerry; Nick Petalas #6298/#6025, unpaidmoon #6293, DreamingOfClouds #6030/#5907, Ali Romman #5827/#5599/#1862/#1931 and retained native/controller/compiler lineage." +} diff --git a/research/role-phase-compatibility/VALIDATION.md b/research/role-phase-compatibility/VALIDATION.md new file mode 100644 index 0000000000..141e8c18c7 --- /dev/null +++ b/research/role-phase-compatibility/VALIDATION.md @@ -0,0 +1,72 @@ +# Executed validation + +Base: `a7638a4ce2a29947457ae8d6bf8cd70a234dfeac`. +Local environment: Linux x86-64, CPython 3.12.14, standard library only. + +Executed successfully: + +```sh +python -I -W error -B research/role-phase-compatibility/verify.py --write-result +python -I -W error -B research/role-phase-compatibility/independent.py +python -B scripts/research_package.py --package research/role-phase-compatibility --check-only +python -B scripts/research_package.py --package research/role-phase-compatibility +``` + +The first command generated the retained RESULT.json. The registered replay +runs the primary and independent checker both normally and under `-O`, with +warning-strict execution and private bytecode-cache namespaces. Every command +passed. The scientific receipt is deterministic; no receipt was handwritten. +The metadata-only pass is not mathematical acceptance. + +The primary exact Fraction-row replay certifies eight reached minors after +9,998 chronological events and checks source charts/owned-zero conditions +through that prefix. Six lowered rank-one recipes are independently interpreted +on 3,072 basis columns against their literal chart operators. Both full and +phase-deleted relative loops are checked on all 512 basis columns. Twelve +rejecting controls and the compatible tree/width-four controls pass. + +The separately written checker imports neither the primary program nor a +native compiler. It independently streams nine input columns with integer +numerator/power-of-two arithmetic (89,982 event applications), checks the +retained eight minors, and solves necessary event-gauge constraints on 32 +widths. Its graph deliberately assigns free new gauges at every nonwitness +write. All 64 missing-contact/altered-phase control graphs are consistent. +This checks a different arithmetic orientation and a graph algorithm rather +than merely rerunning the primary path-sum formula. Its native phase constants +are supplied by the primary's separately dense-checked source certificate. + +The universal claim rests on PROOF.md and exact source certificates, not on +finite width enumeration. Independent human acceptance, formal proof-kernel +acceptance, all selected native maps, the complete selected cold replay, +physical/tape/precision/erasure implementations, supplier admission and hosted +CI are not claimed. The shallow source acquisition does not provide a complete +historical-ancestry preflight; all executed live inputs and provenance pins +resolve at the single frozen canonical base. + +## Committed bytes and portable replay + +At scientific code commit `5a84b1d25f782185587f1251b200d9e08768711c`: + +```sh +python -B scripts/check_research_commit.py --package research/role-phase-compatibility --check-modes +python -B scripts/export_research_package.py export --package research/role-phase-compatibility --output /tmp/role-phase-export.tar.gz +python -B scripts/export_research_package.py check --check-inputs /tmp/role-phase-export.tar.gz +``` + +All passed, covering nine package files and three live inputs. From the +extracted Git-free export, all four direct normal/optimized commands passed +with empty PATH and read-only file/directory modes. All thirteen files +(including the export receipt) retained their bytes and modes. Private writable +copies rejected each of four actual corruptions in both modes: changed word, +changed native source, missing live-pin manifest rows, and a forged retained +minor determinant. The generated [PORTABILITY.json](PORTABILITY.json) records +the outcomes and the unchanged scientific file/input hashes. Adding this +validation record does not alter those scientific bytes. + +A separate subagent reviewed the complete proof and checker scope, including +the actual rank-two premises, absence of hidden writes, the MOVE-phase sign, +the all-width argument and the gatewise/endpoint-only distinction; it reported +no objection. It independently reran `independent.py` normally and `verify.py` +under `-O`, both successfully. The lead also reviewed the proof. This is +independent agent reasoning and separately implemented arithmetic, not human +scientific acceptance or proof-kernel verification. diff --git a/research/role-phase-compatibility/VERIFY.json b/research/role-phase-compatibility/VERIFY.json new file mode 100644 index 0000000000..d0c269979e --- /dev/null +++ b/research/role-phase-compatibility/VERIFY.json @@ -0,0 +1,63 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/p104-helper470-twin-rung-removal/WORD.json.gz", + "research/p104-native-channel/vendor/clifford_exact.py", + "research/p104-native-channel/vendor/native_verify.py" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Exact reached minors and native phase certificate with rejecting controls." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Exact reached minors and native phase certificate with rejecting controls." + }, + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-B", + "{package}/independent.py" + ], + "timeout_seconds": 120, + "checks": "Independent dyadic input-column replay and relaxed event-gauge graph with opened-cycle controls." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-W", + "error", + "-B", + "{package}/independent.py" + ], + "timeout_seconds": 120, + "checks": "Independent dyadic input-column replay and relaxed event-gauge graph with opened-cycle controls." + } + ] +} diff --git a/research/role-phase-compatibility/independent.py b/research/role-phase-compatibility/independent.py new file mode 100644 index 0000000000..738cdfd381 --- /dev/null +++ b/research/role-phase-compatibility/independent.py @@ -0,0 +1,150 @@ +#!/usr/bin/env python3 +"""Independent integer-dyadic column replay and relaxed event-gauge graph. + +No primary verifier, Fraction arithmetic, Clifford compiler, or pricing routine +is imported. Native phase values are the separately dense-checked certificate. +""" +from collections import deque +from hashlib import sha256 +import gzip +import json +from pathlib import Path + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +SOURCE = ROOT / 'research/p104-helper470-twin-rung-removal/WORD.json.gz' +WORD_HASH = '7834725d9e34ee846a9ccc615221ea81e0201613938afa185d2eda0c9a6c232f' +CONTACTS = {8255:(229,227,1,1), 9031:(225,227,-1,1), + 9034:(231,225,1,-1), 9916:(229,87,1,1), + 9924:(231,27,1,1), 9982:(229,238,1,1), + 9983:(231,7,1,1), 9997:(231,81,1,1)} +PHASES = {9901:1,9904:1,9938:0,9955:1,9987:0,9994:0} + + +def demand(ok, reason): + if not ok: + raise ValueError(reason) + + +def normalize(numerator, exponent): + if numerator == 0: + return (0, 0) + while exponent and numerator % 2 == 0: + numerator //= 2 + exponent -= 1 + return numerator, exponent + + +def coefficient(text): + parts = text.split('/') + demand(len(parts) in (1,2), 'Rational text') + numerator = int(parts[0]) + denominator = int(parts[1]) if len(parts) == 2 else 1 + demand(denominator > 0 and denominator & (denominator-1) == 0, 'Dyadic coefficient') + return normalize(numerator, denominator.bit_length()-1) + + +def addition(a, b): + exponent = max(a[1], b[1]) + return normalize((a[0] << (exponent-a[1])) + (b[0] << (exponent-b[1])), exponent) + + +def multiplication(a, b): + return normalize(a[0]*b[0], a[1]+b[1]) + + +def column_replay(program): + columns = sorted({column for row in CONTACTS.values() for column in row[:2]}) + samples = {event:{} for event in CONTACTS} + for column in columns: + values = [(0,0)] * 799 + values[column] = (1,0) + for event, instruction in enumerate(program[:9998]): + operation, target = instruction[:2] + if event in CONTACTS: + source = instruction[2] + samples[event][column] = (values[target], values[source]) + if operation in ('INIT','CLEAR'): + values[target] = (0,0) + elif operation == 'SCALE': + values[target] = multiplication(values[target], coefficient(instruction[2])) + elif operation in ('ADD','COPY'): + source, q = instruction[2:4] + values[target] = addition(values[target], multiplication(coefficient(q), values[source])) + else: + demand(operation == 'MOVE', 'Known operation') + for event, (x, y, first, second) in CONTACTS.items(): + demand(samples[event][x] == ((first,0),(0,0)), 'First independent coordinate') + demand(samples[event][y] == ((0,0),(second,0)), 'Second independent coordinate') + return len(columns), samples + + +def graph(program, width, omit=None, phases=None): + """Every other event is a free new gauge: this only relaxes compatibility.""" + phases = PHASES if phases is None else phases + nodes = list(range(799)) + adjacent = {} + for index, instruction in enumerate(program[:9998]): + operation, target = instruction[:2] + previous, fresh = nodes[target], 799+index + if index in CONTACTS and index != omit: + source = nodes[instruction[2]] + constraints = ((previous,fresh,0),(source,fresh,0)) + elif index in phases: + constraints = ((previous,fresh,-width*phases[index]),) + else: + constraints = () + for u,v,difference in constraints: + adjacent.setdefault(u,[]).append((v,difference % 4)) + adjacent.setdefault(v,[]).append((u,(-difference) % 4)) + nodes[target] = fresh + return adjacent + + +def consistent(adjacent): + labels = {} + for root in adjacent: + if root in labels: + continue + labels[root] = 0 + queue = deque([root]) + while queue: + current = queue.popleft() + for other, difference in adjacent[current]: + proposed = (labels[current]+difference) % 4 + if other in labels: + if labels[other] != proposed: + return False + else: + labels[other] = proposed + queue.append(other) + return True + + +def main(): + raw = SOURCE.read_bytes() + demand(sha256(raw).hexdigest() == WORD_HASH, 'Exact source bytes') + word = json.loads(gzip.decompress(raw)) + program = word['program'] + columns, samples = column_replay(program) + for width in range(1,33): + demand(consistent(graph(program,width)) == (width % 4 == 0), 'Relaxed graph criterion') + demand(consistent(graph(program,width,omit=9997)), 'Missing final ADD opens cycle') + repaired = dict(PHASES) + repaired[9955] = 0 + demand(consistent(graph(program,width,phases=repaired)), 'Altered native phase opens cycle') + # Verify the emitted primary table against these independently computed columns. + receipt = json.loads((HERE/'RESULT.json').read_text()) + for event, (x,y,a,b) in CONTACTS.items(): + row = receipt['independent_adds'][str(event)] + demand(row == {'columns':[x,y], 'matrix':[[str(a),'0'],['0',str(b)]], + 'determinant':str(a*b)}, 'Independent retained minor') + demand(receipt['native_move_phases'] == {str(k):v for k,v in PHASES.items()}, 'Phase certificate agreement') + print(json.dumps({'integer_dyadic_columns':columns,'column_events':columns*9998, + 'independent_minors':len(samples),'width_graphs':32, + 'opened_cycle_controls':64},sort_keys=True)) + print('PASS_INDEPENDENT_ROLE_PHASE columns=9 contacts=8 relaxed_graphs=32') + + +if __name__ == '__main__': + main() diff --git a/research/role-phase-compatibility/verify.py b/research/role-phase-compatibility/verify.py new file mode 100644 index 0000000000..8c4cf3521e --- /dev/null +++ b/research/role-phase-compatibility/verify.py @@ -0,0 +1,260 @@ +#!/usr/bin/env python3 +"""Check the reached, role-specific phase obstruction; no full supplier claim.""" +from fractions import Fraction +from hashlib import sha256 +import argparse +import gzip +import json +from pathlib import Path +import sys +import types + +PACKAGE = Path(__file__).resolve().parent +ROOT = PACKAGE.parents[1] +WORD = 'research/p104-helper470-twin-rung-removal/WORD.json.gz' +CLIFFORD = 'research/p104-native-channel/vendor/clifford_exact.py' +NATIVE = 'research/p104-native-channel/vendor/native_verify.py' +PINS = { + WORD: '7834725d9e34ee846a9ccc615221ea81e0201613938afa185d2eda0c9a6c232f', + CLIFFORD: '2982ead07721e83358dc67c6f49c2b4c16a236a6bebdfd72f58221be1f5d0962', + NATIVE: '3049471905b47b385c88378a1a3be7a18b8858aadd035b8a6da2f4a03b470f38', +} +ADDS = { + 8255: (229, 227, '-1', 3, 229, 227, 1), + 9031: (225, 227, '1', 3, 225, 227, -1), + 9034: (231, 225, '1', 3, 231, 225, -1), + 9916: (229, 87, '1', 81, 229, 87, 1), + 9924: (231, 27, '1', 25, 231, 27, 1), + 9982: (229, 238, '1', 254, 229, 238, 1), + 9983: (231, 236, '1', 256, 231, 7, 1), + 9997: (231, 229, '1', 259, 231, 81, 1), +} +MOVES = { + 9901: (231, 3, 25, 1), 9904: (229, 3, 81, 1), + 9938: (229, 81, 254, 0), 9955: (231, 25, 256, 1), + 9987: (231, 256, 259, 0), 9994: (229, 254, 259, 0), +} +PATH_A = (9904, 9938, 9994) +PATH_B = (9901, 9955, 9987) + + +def need(ok, message): + if not ok: + raise ValueError(message) + + +def rejected(operation, message): + try: + operation() + except ValueError: + return 1 + raise ValueError('Control was accepted: ' + message) + + +def read_inputs(): + pins = json.loads((PACKAGE / 'SOURCES.json').read_text()) + declared = {r['path']: r['sha256'] for r in pins['files'] if r['usage'] == 'input'} + need(declared == PINS, 'Exact declared input set') + data = {} + for path, digest in PINS.items(): + raw = (ROOT / path).read_bytes() + need(sha256(raw).hexdigest() == digest, 'Source bytes: ' + path) + data[path] = raw + word = json.loads(gzip.decompress(data[WORD])) + need(word['schema'] == 'p104-accumulated-block-composition/2', 'Word schema') + need(word['public'] == 770 and word['owned_fields'] == 29, 'Public/owned inventory') + need(len(word['program']) == 22803, 'Exact selected event count') + return word, data + + +def source_module(raw, name): + # Compile authenticated source bytes directly: no stale .pyc can replace them. + module = types.ModuleType(name) + module.__file__ = str(ROOT / name) + exec(compile(raw, module.__file__, 'exec'), module.__dict__) + return module + + +def witness_events(word): + program = word['program'] + for index, (t, s, q, chart, _x, _y, _det) in ADDS.items(): + need(program[index] == ['ADD', t, s, q, chart], 'Named ADD ' + str(index)) + for index, (role, a, b, _phase) in MOVES.items(): + need(program[index] == ['MOVE', role, a, b, False], 'Named MOVE ' + str(index)) + windows = ((227, 8255, 9031, ()), (225, 9031, 9034, ()), + (229, 8255, 9997, (9904, 9916, 9938, 9982, 9994)), + (231, 9034, 9997, (9901, 9924, 9955, 9983, 9987))) + for role, first, last, expected in windows: + writes = tuple(i for i in range(first + 1, last) if program[i][1] == role) + need(writes == expected, 'No hidden write in role window ' + str(role)) + return windows + + +def row_add(target, source, coefficient): + result = dict(target) + for key, value in source.items(): + result[key] = result.get(key, Fraction(0)) + coefficient * value + if result[key] == 0: + del result[key] + return result + + +def exact_prefix(word): + rows = [{i: Fraction(1)} for i in range(770)] + [{} for _ in range(29)] + current = list(word['initial']) + [None] * 29 + active = set() + minors = {} + for index, event in enumerate(word['program'][:9998]): + op, role = event[:2] + need(type(role) is int and 0 <= role < 799, 'Role domain') + if op == 'INIT': + need(role >= 770 and role not in active and not rows[role], 'Owned INIT') + current[role] = event[2] + active.add(role) + elif op == 'CLEAR': + need(role in active and not rows[role], 'Owned exact CLEAR') + need(current[role] == event[2], 'CLEAR chart') + current[role] = None + active.remove(role) + elif op == 'MOVE': + _op, _role, a, b, owned = event + need(current[role] == a and (role in active) is owned, 'MOVE state') + current[role] = b + elif op == 'SCALE': + need(current[role] == event[-1], 'SCALE chart') + coefficient = Fraction(event[2]) + need(coefficient != 0, 'Nonzero SCALE') + rows[role] = {k: coefficient * v for k, v in rows[role].items()} + elif op in ('ADD', 'COPY'): + _op, _role, source, q, chart = event + need(current[role] == current[source] == chart, 'Scalar common chart') + need(role != source, 'Distinct scalar roles') + if op == 'COPY': + need(not rows[role], 'COPY into exact zero') + if index in ADDS: + _t, _s, _q, _f, x, y, expected = ADDS[index] + matrix = [[rows[r].get(k, Fraction(0)) for k in (x, y)] for r in (role, source)] + det = matrix[0][0] * matrix[1][1] - matrix[0][1] * matrix[1][0] + need(det == expected and det != 0, 'Reached rank-two ADD ' + str(index)) + minors[str(index)] = {'columns': [x, y], 'matrix': [[str(z) for z in r] for r in matrix], 'determinant': str(det)} + rows[role] = row_add(rows[role], rows[source], Fraction(q)) + else: + raise ValueError('Unknown opcode') + need(len(minors) == 8, 'Every independent contact certified') + return minors + + +def native_edges(word, raw): + clifford = source_module(raw[CLIFFORD], 'phase_clifford') + native = source_module(raw[NATIVE], 'phase_native') + recipes, stripped, phases = {}, {}, {} + for index, (_role, a, b, expected_phase) in MOVES.items(): + chart_a = clifford.canonical_frame(9, word['frames'][a]) + chart_b = clifford.canonical_frame(9, word['frames'][b]) + record, _compiled = clifford.lower_child(chart_a.adjoint().then(chart_b)) + recipe = native.recipe(record) + phases[index] = sum(g[1] for g in recipe if g[0] == 'phase') % 4 + need(record['rank'] == 1 and phases[index] == expected_phase, 'Native rank/phase') + literal = native.adjoint(native.frame(tuple(word['frames'][a]), 9)) + literal += native.frame(tuple(word['frames'][b]), 9) + for address in range(512): + need(native.state(recipe, address) == native.state(literal, address), 'Every native basis column') + recipes[index] = tuple(recipe) + stripped[index] = tuple(g for g in recipe if g[0] != 'phase') + return native, recipes, stripped, phases + + +def path_loop(native, recipes, stripped): + full_a = sum((recipes[i] for i in PATH_A), ()) + full_b = sum((recipes[i] for i in PATH_B), ()) + bare_a = sum((stripped[i] for i in PATH_A), ()) + bare_b = sum((stripped[i] for i in PATH_B), ()) + full = full_b + tuple(native.adjoint(full_a)) + bare = bare_b + tuple(native.adjoint(bare_a)) + for address in range(512): + need(native.state(full, address) == ({address: (1, 0)}, 0), 'Full paths agree') + need(native.state(bare, address) == ({address: (0, -1)}, 0), 'Bare paths differ by -i') + return bare + + +def finite_phase_check(phases): + a = sum(phases[i] for i in PATH_A) % 4 + b = sum(phases[i] for i in PATH_B) % 4 + need((a, b) == (1, 2), 'Distinct chronological path phases') + # Tree equations determine every gauge from the free root. The final + # ADD demands equality. This is corroboration, not the all-f proof. + counts = [sum((root - width*a) % 4 == (root - width*b) % 4 + for root in range(4)) for width in range(1, 5)] + need(counts == [0, 0, 0, 4], 'Finite gauge solution counts') + return counts + + +def controls(word, raw, native, bare, phases): + count = 0 + for path, payload in raw.items(): + count += rejected(lambda: need(sha256(payload+b'\n').hexdigest() == PINS[path], 'Changed source'), path) + bad = json.loads(json.dumps(word)) + bad['program'][9997][2] = 230 + count += rejected(lambda: witness_events(bad), 'Changed contact') + bad = json.loads(json.dumps(word)) + bad['program'][9000] = ['SCALE', 227, '1', 3] + count += rejected(lambda: witness_events(bad), 'Hidden write') + count += rejected(lambda: need(native.state(bare) == ({0: (1, 0)}, 0), 'No loop phase'), 'Phase deletion') + count += rejected(lambda: need(native.state(bare) == ({0: (0, 1)}, 0), 'Wrong sign'), 'Loop sign') + bad_phase = dict(phases) + bad_phase[9955] = 0 + count += rejected(lambda: finite_phase_check(bad_phase), 'Wrong native phase') + # A missing independence hypothesis cannot justify equal phases. + a, b = (1, 0), (0, 0) + need(a[0]*b[1]-a[1]*b[0] == 0, 'Dependent control is actually dependent') + count += rejected(lambda: need(a[0]*b[1]-a[1]*b[0] != 0, 'Required rank two'), 'Zero source') + # Removing the closing contact leaves a tree with four gauges at each width. + need(all(len({(q, (q-f)%4, (q-2*f)%4) for q in range(4)}) == 4 for f in range(1,5)), 'Open tree control') + # An actual altered ADD coefficient would repair this cycle only. + def rotate(pair, power): + x, y = pair + return ((x,y),(-y,x),(-x,-y),(y,-x))[power % 4] + for f in range(1,5): + target, source = rotate((1,2), -2*f), rotate((3,4), -f) + correction = rotate(source, -f) + repaired = tuple(x+y for x,y in zip(target, correction)) + required = rotate((4,6), -2*f) + need(repaired == required, 'Actual changed-coefficient ADD') + unmodified = tuple(x+y for x,y in zip(target, source)) + if f % 4: + count += rejected(lambda: need(unmodified == required, 'Unmodified ADD'), 'Missing compensating coefficient') + else: + need(unmodified == required, 'Width-four unchanged ADD') + return count + + +def main(): + parser = argparse.ArgumentParser() + parser.add_argument('--write-result', action='store_true') + args = parser.parse_args() + word, raw = read_inputs() + witness_events(word) + minors = exact_prefix(word) + native, recipes, stripped, phases = native_edges(word, raw) + bare = path_loop(native, recipes, stripped) + counts = finite_phase_check(phases) + rejected_count = controls(word, raw, native, bare, phases) + result = {'schema':'role-phase-compatibility/1', 'no_new_kappa':True, + 'prefix_events':9998, 'witness_event_count':14, 'independent_adds':minors, + 'native_move_phases':{str(k):v for k,v in phases.items()}, + 'native_basis_column_comparisons':3072, 'loop_basis_columns':512, + 'path_phase_sums_mod4':[1,2], 'stripped_relative_loop':'-i I', + 'gauge_counts_widths_1_to_4':counts, 'rejecting_controls':rejected_count, + 'input_sha256':PINS} + result_path = PACKAGE / 'RESULT.json' + if args.write_result: + need(not result_path.exists(), 'Refuse to overwrite retained result') + result_path.write_text(json.dumps(result,indent=2,sort_keys=True)+'\n') + else: + need(json.loads(result_path.read_text()) == result, 'Exact retained result') + print(json.dumps(result,sort_keys=True)) + print('PASS_ROLE_PHASE_COMPATIBILITY events=14 contacts=8 moves=6 iff_four_divides_width') + + +if __name__ == '__main__': + main()