Exhibit a reversible-lifting defect on an actual native frame cycle

research/native-rounded-loop-defect/.gitattributes

@@ -0,0 +1 @@
+source/* -text

research/native-rounded-loop-defect/PINS.json

@@ -0,0 +1,37 @@
+[
+  {
+    "path": "source/ACTUAL-WORD.json.gz",
+    "upstream_path": "research/kappa-round3-warp-20261022/ACTUAL-WORD.json.gz",
+    "commit": "32890bc5de034ab8fc93ac88ead7279a6a416d04",
+    "sha256": "7679daa4ec6a40f56fc7f0202379a6f454310e94945aba4f48beaaaafb838d05",
+    "git_blob": "46d929df83817b85a5387bcdb9745e0627d6366e"
+  },
+  {
+    "path": "source/graph-certificate.json.gz",
+    "upstream_path": "research/coherent-frame-additivity/CERTIFICATE.json.gz",
+    "commit": "32890bc5de034ab8fc93ac88ead7279a6a416d04",
+    "sha256": "e69cd4db3a2bd6661d267be8a35a2f871cefe1ac03bdaf471c13ea627a705358",
+    "git_blob": "a90d2fd0441ecafda09d111237567a96f48d1dbd"
+  },
+  {
+    "path": "source/coherence-background.md",
+    "upstream_path": "research/coherent-frame-additivity/README.md",
+    "commit": "32890bc5de034ab8fc93ac88ead7279a6a416d04",
+    "sha256": "cf6889e806a9b4fa9a75beccefaa998627a9b35b77be529f0fe26718f60b9d67",
+    "git_blob": "5c72c03ba7887aedad30acf4c20f40346da2fee5"
+  },
+  {
+    "path": "source/lifting.py",
+    "upstream_path": "research/p104-reversible-lifting/lifting.py",
+    "commit": "32890bc5de034ab8fc93ac88ead7279a6a416d04",
+    "sha256": "9424ee08f22b717f6d58f7cc46f189c5549fa86778afcd0c0762ab2daf591160",
+    "git_blob": "524ed59c1e498f78134681bea49fac55e9541068"
+  },
+  {
+    "path": "source/clifford_exact.py",
+    "upstream_path": "research/t74-native-fast/vendor/native/new/code/borrow/vendor/clifford/clifford_exact.py",
+    "commit": "32890bc5de034ab8fc93ac88ead7279a6a416d04",
+    "sha256": "2982ead07721e83358dc67c6f49c2b4c16a236a6bebdfd72f58221be1f5d0962",
+    "git_blob": "166841a037f069249f6f7f6dedb89248812f59e2"
+  }
+]

research/native-rounded-loop-defect/PROOF.md

@@ -0,0 +1,31 @@
+# Concrete native holonomy obstruction
+
+## Literal source and hypothesis being tested
+
+The pinned round-three ACTUAL-WORD forward program supplies events8160,8148,8196,8197. Their native frame edges are 0→29,0→2,2→341,29→341, all rank one. The retained coherent-frame-additivity certificate places the first three in its forest and the last among its chords. Frames0,29,2,341 are respectively [],[38],[11],[38,11]. The closed walk traverses the first and last edges backwards. These occurrences may concern different supplier roles; this is the consistency cycle required of a single frame-potential implementation, not a claim that the supplier executes these four instructions consecutively on one role.
+
+For frame a let F_a be its exact canonical unitary. Each exact edge is F_b F_a^-1. The loop telescopes to identity, including its global phase. The independently decoded native recipes each equal this operator as both tableau and zero-state vector. Tableau equality alone would miss global phase and is explicitly fault-tested.
+
+Use the existing P104 integer-lifting `pair` unchanged. For Gaussian integer inputs a,b, set d=a-b, s=b+floor(d/2), d'=i d, b'=s-floor(d'/2), a'=b'+d'; floor is componentwise. The inverse uses -i. Each step is a bijective lift; reversing the quarter turn gives the exact inverse on all Gaussian integers. Signed affine monomial wrappers are exact permutations and quarter turns; inverse wrappers preserve exact reversibility. These are actual native adapters, not an abstract inverse oracle.
+
+## Witness and quantified conclusion
+
+Take 512 Gaussian integer slots, all zero except slot1=1. The authenticated executable verifies every intermediate sparse row twice: the original source in-place kernel and a separately written recipe/floor interpreter. After the loop the only nonzero entries are slot1=i, slot10=1, slot39=1. The defect is (i-1)e1+e10+e39, with squared Euclidean norm4. A rational interpreter replacing floor by exact division yields precisely e1. Every edge followed by its own inverse, and the reverse of the entire literal rounded word, restore the input exactly.
+
+For every integer g>=0 set h=2^-g. Realize the same integer-coordinate implementation on h Z[i]^512. Input h e1 gives output h(i e1+e10+e39); its defect2h is strictly nonzero. This proves failure of exact graph flatness at every dyadic precision, rather than a finite precision search failure. An interface quantified over all positive widths already fails at width1. This does not establish failure at every width, a large-input relative-error lower bound, or failure of a different jointly coherent implementation. Indeed16e1 is an aligned-lattice positive control with zero defect.
+
+If a family of bijective rounded frame potentials P_a existed with every directed rounded edge P_b P_a^-1 equal to these four actual implementations, their product around the loop would be identity on every input. The witness contradicts this. The argument concerns exact potential consistency; approximate end-to-end accuracy may still be adequate with an independently proved budget. No inference from invertibility alone to flatness is permitted.
+
+## Error, internal magnitude and complete diagnostic invoice
+
+For one pair, compare to its ideal Gaussian unitary. Let e=d/2-floor(d/2) and e'=d'/2-floor(d'/2). Each component is0 or1/2; both outputs acquire the same error e'-e. Thus the pair Euclidean error is at most1. There are256 disjoint pairs in a rank-one512-vector call, so its norm error is at most16, also for the inverse sign. Exact monomial wrappers preserve norm. Four calls therefore have worst-case Euclidean defect at most64 grid units, by unitary transport and the triangle inequality. This applies to every Gaussian integer input, not just the witness.
+
+If every initial real/imaginary component has magnitude<=M, ideal pair components have magnitude<=2M, and rounded outputs<=2M+1/2. Four prefixes therefore have components<=16M+15/2. Within the literal lifts differences, pre-floor values, sums and quarter turns are bounded conservatively by32M+16 across the four calls. Signed integers with w=1+ceil(log2(32M+17)) bits suffice; grid spacing h changes physical units, not integer register bounds. This is an absolute precision analysis of this four-edge diagnostic, not a complete multiplication error budget.
+
+The paid profile is exactly four H1, with eight signed monomial wrapper applications. At width1 there are1024 pair operations,4096 wrapped Gaussian values, and the receipt records actual permutation cycles/swaps. A register-reused arithmetic implementation of each pair uses eight real additions/subtractions, four real floor divisions by2 and one sign change; the Python source is a semantic reference, not an instruction-for-instruction tariff implementation. Its eager rotate tuple and Python temporaries are not priced as that schedule. The source code compiles cycles at invocation time; any prepared-plan variant must charge that setup/storage rather than claim it absent.
+
+One live512-vector is mutated; a monomial cycle uses one owned-zero Gaussian scratch restored after each cycle. The verifier holds independent snapshots/oracles solely as instrumentation. Eight wrapper plans contain4096(index,phase) entries; generating them and cycle schedules is ordinary O(512) work per wrapper with explicit retained plans, not recursively cheap oracle access. All diagnostic calls and reverse-control calls are separately counted in tests; the scientific profile four H1 refers only to the proposed closed walk. There is no claimed scalar allowance, saved recursive work, all-width runtime, complete supplier cleanup theorem or kappa improvement.
+
+## Family expansion decision
+
+The result closes independent edge-by-edge P104 rounding as an exact frame-potential service on this actual paid graph. It does not close history-preserving, jointly coherent, additive, or differently rounded services. The R15 nearest-even service is different and makes no exact inverse claim. Existing generic nonlinear counterexamples and graph-cycle enumeration did not establish this concrete native failure. Any next construction must state how it restores flatness and additivity, charge correction/history creation and erasure, bound precision/internal values, and compose the complete caller invoice; a local inverse test cannot substitute for those obligations.

research/native-rounded-loop-defect/README.md

@@ -0,0 +1,13 @@
+# An actual native paid cycle has nonzero integer-lifting holonomy
+
+The four-edge native frame cycle 29→0→2→341→29 is exactly identity over Gaussian rationals. Applying the existing P104 reversible integer lifting core through the literal signed native adapters instead sends the unit input e1 to i e1+e10+e39. Its defect has Euclidean norm2 in grid units. Every individual child and the reversed whole loop remain exactly invertible.
+
+This supplies the missing concrete native example for the coherent-frame-additivity handoff. It reuses the existing rounding method; it does not propose a new one. Scaling the witness by any dyadic grid spacing proves failure of exact graph flatness at every precision. The witness is width one, which suffices to refute an interface required at all positive widths. No claim is made that every width or every input fails.
+
+Run `python3 -I -B research/native-rounded-loop-defect/verify.py` and the same command with `-O`. Source bytes are authenticated before import. Both integer and ideal rational paths have an independent recipe/floor interpreter. The receipt includes every sparse cut, literal event identifiers, and actual operation counters. `PROOF.md` states scope, analytic bounds and complete diagnostic cost.
+
+## Open next questions
+
+Can coherent frame potentials replace independently rounded native edges without exceeding the recursive budget? Can a changed child ABI retain correction information around this actual loop? Additivity and endpoint correctness remain separate obligations even after graph flatness is achieved. No complete caller, recursive child tariff or new kappa is claimed.
+
+Package-boundary controls run with `python3 -I -B research/native-rounded-loop-defect/test_package.py`: copied-source mutation must fail before import; receipt mutation must fail in normal and optimized Python. All executable inputs are local to this package. Frozen predecessor bytes retain their attribution.

research/native-rounded-loop-defect/RECIPES.json

@@ -0,0 +1 @@
+[{"rank": 1, "left": {"matrix_rows": [2, 5, 9, 16, 32, 1, 64, 128, 256], "offset": 0, "quadratic_rows": [0, 0, 0, 0, 0, 0, 0, 0, 0], "linear_Z4": [2, 0, 0, 0, 0, 0, 0, 0, 0], "phase": 0}, "right": {"matrix_rows": [38, 1, 34, 36, 8, 16, 64, 128, 256], "offset": 1, "quadratic_rows": [0, 6, 6, 0, 0, 0, 0, 0, 0], "linear_Z4": [0, 3, 3, 0, 0, 2, 0, 0, 0], "phase": 1}}, {"rank": 1, "left": {"matrix_rows": [3, 5, 8, 1, 16, 32, 64, 128, 256], "offset": 0, "quadratic_rows": [0, 0, 0, 0, 0, 0, 0, 0, 0], "linear_Z4": [2, 0, 0, 0, 0, 0, 0, 0, 0], "phase": 0}, "right": {"matrix_rows": [11, 9, 10, 4, 16, 32, 64, 128, 256], "offset": 1, "quadratic_rows": [3, 3, 0, 0, 0, 0, 0, 0, 0], "linear_Z4": [3, 3, 0, 2, 0, 0, 0, 0, 0], "phase": 1}}, {"rank": 1, "left": {"matrix_rows": [2, 5, 9, 16, 32, 1, 64, 128, 256], "offset": 0, "quadratic_rows": [0, 0, 0, 0, 0, 0, 0, 0, 0], "linear_Z4": [2, 0, 0, 0, 0, 0, 0, 0, 0], "phase": 0}, "right": {"matrix_rows": [38, 1, 34, 36, 8, 16, 64, 128, 256], "offset": 1, "quadratic_rows": [0, 6, 6, 0, 0, 0, 0, 0, 0], "linear_Z4": [0, 3, 3, 0, 0, 2, 0, 0, 0], "phase": 1}}, {"rank": 1, "left": {"matrix_rows": [3, 5, 8, 1, 16, 32, 64, 128, 256], "offset": 0, "quadratic_rows": [0, 0, 0, 0, 0, 0, 0, 0, 0], "linear_Z4": [2, 0, 0, 0, 0, 0, 0, 0, 0], "phase": 0}, "right": {"matrix_rows": [11, 9, 10, 4, 16, 32, 64, 128, 256], "offset": 1, "quadratic_rows": [3, 3, 0, 0, 0, 0, 0, 0, 0], "linear_Z4": [3, 3, 0, 2, 0, 0, 0, 0, 0], "phase": 1}}]

research/native-rounded-loop-defect/RESULT.json

@@ -0,0 +1,120 @@
+{
+  "events": [
+    8160,
+    8148,
+    8196,
+    8197
+  ],
+  "directions": [
+    "inverse",
+    "forward",
+    "forward",
+    "inverse"
+  ],
+  "frames": [
+    29,
+    0,
+    2,
+    341,
+    29
+  ],
+  "witness_input": [
+    [
+      1,
+      [
+        1,
+        0
+      ]
+    ]
+  ],
+  "witness_output": [
+    [
+      1,
+      [
+        0,
+        1
+      ]
+    ],
+    [
+      10,
+      [
+        1,
+        0
+      ]
+    ],
+    [
+      39,
+      [
+        1,
+        0
+      ]
+    ]
+  ],
+  "defect_squared_norm": 4,
+  "cuts": [
+    [
+      [
+        1,
+        [
+          1,
+          0
+        ]
+      ]
+    ],
+    [
+      [
+        1,
+        [
+          0,
+          1
+        ]
+      ]
+    ],
+    [
+      [
+        1,
+        [
+          -1,
+          1
+        ]
+      ],
+      [
+        39,
+        [
+          1,
+          0
+        ]
+      ]
+    ],
+    [
+      [
+        1,
+        [
+          0,
+          1
+        ]
+      ],
+      [
+        10,
+        [
+          1,
+          0
+        ]
+      ],
+      [
+        39,
+        [
+          1,
+          0
+        ]
+      ]
+    ]
+  ],
+  "meter": {
+    "pairs": 1024,
+    "wrapper_values": 4096,
+    "wrapper_cycles": 512,
+    "wrapper_swaps": 4608
+  },
+  "claim": "Every dyadic grid has a scaled witness; exact child inverses do not imply native graph flatness."
+}

research/native-rounded-loop-defect/SOURCES.json

@@ -0,0 +1,48 @@
+{
+  "schema_version": 1,
+  "base_commit": "32890bc5de034ab8fc93ac88ead7279a6a416d04",
+  "files": [
+    {
+      "path": "certificates/selected-result.json",
+      "usage": "provenance",
+      "git_blob": "fc3d4ba105e1f097d0d7d051a308281e86ab1446",
+      "sha256": "66974efdced4083c00025f97d95d83909a226cdf801edb9301c195c6641f6903"
+    },
+    {
+      "path": "docs/research/agent-task-catalog.json",
+      "usage": "provenance",
+      "git_blob": "f126dd2e2dad2b669e75d1d0d0bd05c600725602",
+      "sha256": "f7a48bfa2659b88378282a8eee7d9fe52cdf505594124c4d1686b58510fffd72"
+    },
+    {
+      "path": "research/kappa-round3-warp-20261022/ACTUAL-WORD.json.gz",
+      "usage": "provenance",
+      "git_blob": "46d929df83817b85a5387bcdb9745e0627d6366e",
+      "sha256": "7679daa4ec6a40f56fc7f0202379a6f454310e94945aba4f48beaaaafb838d05"
+    },
+    {
+      "path": "research/coherent-frame-additivity/CERTIFICATE.json.gz",
+      "usage": "provenance",
+      "git_blob": "a90d2fd0441ecafda09d111237567a96f48d1dbd",
+      "sha256": "e69cd4db3a2bd6661d267be8a35a2f871cefe1ac03bdaf471c13ea627a705358"
+    },
+    {
+      "path": "research/coherent-frame-additivity/README.md",
+      "usage": "provenance",
+      "git_blob": "5c72c03ba7887aedad30acf4c20f40346da2fee5",
+      "sha256": "cf6889e806a9b4fa9a75beccefaa998627a9b35b77be529f0fe26718f60b9d67"
+    },
+    {
+      "path": "research/p104-reversible-lifting/lifting.py",
+      "usage": "provenance",
+      "git_blob": "524ed59c1e498f78134681bea49fac55e9541068",
+      "sha256": "9424ee08f22b717f6d58f7cc46f189c5549fa86778afcd0c0762ab2daf591160"
+    },
+    {
+      "path": "research/t74-native-fast/vendor/native/new/code/borrow/vendor/clifford/clifford_exact.py",
+      "usage": "provenance",
+      "git_blob": "166841a037f069249f6f7f6dedb89248812f59e2",
+      "sha256": "2982ead07721e83358dc67c6f49c2b4c16a236a6bebdfd72f58221be1f5d0962"
+    }
+  ]
+}

research/native-rounded-loop-defect/TASK.json

@@ -0,0 +1,74 @@
+{
+  "schema_version": 1,
+  "task_id": "uniform-transfer-audit",
+  "priority_revision": 7,
+  "base_commit": "32890bc5de034ab8fc93ac88ead7279a6a416d04",
+  "original_card": {
+    "id": "uniform-transfer-audit",
+    "question": "Does one quantified step of the proposed #4100 all-size construction hold at its actual caller?",
+    "starting_points": [
+      "docs/research/research-family-status.md",
+      "certificates/selected-result.json",
+      "research/unconditional-batched-crt/README.md"
+    ],
+    "methods": [
+      "Prove one missing implication with explicit quantified hypotheses.",
+      "Find an exact counterexample at the claimed interface boundary."
+    ],
+    "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_baseline.py"
+      ],
+      "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY",
+      "inspect": "Read PROOF.md and AUDIT.md in #4100. Select one distinct obligation: CRT total repair, native/free-algebra lifting, precision/conditioning, or complete fixed-tape cost. This is an author-submitted proof, not an accepted unconditional theorem.",
+      "scope": "Source-binding orientation only; no scientific replay, theorem acceptance or supplier admission. Budget any heavy replay separately."
+    },
+    "first_experiment": "Check live handoffs; name one proposition, its caller, quantified domain and dependency closure. Independently prove the implication or exhibit a precise gap/counterexample. Prioritize CRT.md total repair or COMPLEX.md free-algebra lift only if unclaimed. Stop at the chosen obligation; do not substitute finite samples or root arithmetic for an all-size proof, or launch the complete package by default.",
+    "bottleneck_link": "Finite supplier improvements are useful only under the retained transfer obligations.",
+    "allowed_variations": [
+      "One CRT repair, native lift, precision/conditioning or tape-cost proposition, with its exact caller."
+    ],
+    "scope_change_triggers": [
+      "Replacing a quantified obligation with another finite smoke test.",
+      "Treating archive intake, an author PASS receipt or a finite composed fixture as discharge of the universal hypotheses."
+    ],
+    "overlap_terms": [
+      "uniform transfer",
+      "all-size",
+      "precision",
+      "4100",
+      "unconditional-batched-crt"
+    ],
+    "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_status": "changed",
+  "actual_scope": "Existing reversible lifting through actual native signed adapters fails exact flatness on one paid graph cycle at every dyadic grid precision.",
+  "scope_change_reason": "Concrete native compatibility obligation left open by abstract coherence witnesses.",
+  "bottleneck_link": "Closes a specific missing interface obligation before another construction round; no selected-frontier change.",
+  "budget_minutes": 60,
+  "stop_rule": "20-minute source-bound proof gate, then finish exact quantified result and controls; stop if only an old theorem or finite extrapolation survives.",
+  "outcome": "negative-result",
+  "evidence": "PROOF.md; source-pinned verify.py; RESULT.json; VERIFY.json",
+  "author": "JoyboyBrian",
+  "ai_assistance": "OpenAI Codex substantial proof and implementation assistance",
+  "open_questions": [
+    {
+      "question": "Construct jointly coherent frame potentials and prove additive caller compatibility with full cost and precision.",
+      "why_it_matters": "A changed interface is necessary before claiming additional recursive savings.",
+      "first_step": "Write the complete changed producer/caller invoice before synthesis.",
+      "blocked_by": "Unproved changed-interface implementation"
+    }
+  ]
+}