diff --git a/research/coherent-frame-additivity/CERTIFICATE.json.gz b/research/coherent-frame-additivity/CERTIFICATE.json.gz new file mode 100644 index 0000000000..a90d2fd044 Binary files /dev/null and b/research/coherent-frame-additivity/CERTIFICATE.json.gz differ diff --git a/research/coherent-frame-additivity/OVERLAP.json b/research/coherent-frame-additivity/OVERLAP.json new file mode 100644 index 0000000000..b9610a6137 --- /dev/null +++ b/research/coherent-frame-additivity/OVERLAP.json @@ -0,0 +1,40 @@ +{ + "base_commit": "b91956876e5b4122fd89179f1b57557ff8378f15", + "priority_revision": 7, + "terms": [ + "frame potential", + "holonomy", + "coherent frame" + ], + "coverage": { + "local": { + "head": "b91956876e5b4122fd89179f1b57557ff8378f15", + "records": 6638, + "head_records": 6636, + "complete_head_inventory": true, + "unsearched_head_paths": [] + }, + "open_prs": { + "fetched_at": "2026-10-23T05:16:29.496227+00:00", + "complete_pagination": true, + "records": 324 + }, + "discussions": { + "fetched_at": "2026-10-23T05:17:19.690420+00:00", + "complete_pagination": true, + "records": 4081 + } + }, + "nearest_work": [ + { + "pr": 4966, + "head": "039b6ea51ab7a7efb38fc6851f345839683251b0", + "adds": "Same-realization inverse recipes, independent paid-site precision census; final coherent-potential target is the audited boundary." + }, + { + "path": "research/coherent-transvection-neighborhood", + "adds": "Graph kernel constraints for binary symplectic axes; credited predecessor context, not the nonlinear ADD criterion or actual paid-frame census." + } + ], + "limits": "Open PR bodies, discussions and top-level local notes; no full diff/unpublished/closed-remote-body coverage. Not a novelty certificate." +} diff --git a/research/coherent-frame-additivity/PROOF.md b/research/coherent-frame-additivity/PROOF.md new file mode 100644 index 0000000000..67dd02c9d3 --- /dev/null +++ b/research/coherent-frame-additivity/PROOF.md @@ -0,0 +1,197 @@ +# Scalar compatibility of coherent frame potentials + +Prepared by Cinna Davis with substantial OpenAI Codex assistance. Apache-2.0. +These are written proofs with exact finite corroboration, not proof-assistant +theorems. No new κ or supplier admission is claimed. + +## 1. The actual proposed boundary + +Yiyang's PR4966 at `039b6ea51ab7a7efb38fc6851f345839683251b0` constructs +same-realization inverse recipes for both native orientations. Its final +paragraph proposes coherent frame potentials as a sufficient compatibility +target for a future caller: a paid transition a→b should realize +`A_b A_a^-1`, and a warp should realize `A_new W A_old^-1`. The proof also +explicitly warns that reversible rounded implementations can be nonlinear +and need not satisfy the controller's linear operator identities. This +contribution makes one part of that warning precise at the actual source. +The unchanged predecessor proof is vendored with its exact provenance. + +Consider a **gatewise** proof using one common bijection A_f per frame f, +shared by every register currently in that frame. It must also account for +unchanged scalar instructions. On two independent fields of that frame an +ADD has the map + +`G_c(x,y) = (x+c y,y)`. + +Commuting the product coordinate change `A_f × A_f` through that same ADD +is equivalent to + +`A_f(x+c y) = A_f(x)+c A_f(y)` for every x,y. (1) + +Transition and warp equations alone do not state (1). This observation is +about the described proof recipe. Global endpoint agreement might instead +follow from a different identity, changed scalar instructions, or a bound +on the resulting errors; none is excluded here. + +## 2. Exact local criterion + +Let D be a module over the dyadic rationals Z[1/2], with no nonzero element +killed by a power of two. Let c be a nonzero dyadic **unit**, so c=±2^k +for an integer k. An arbitrary map A:D→D satisfies (1) if and only if it +is additive. Bijectivity is unnecessary for this equivalence. + +For necessity put y=0 in (1). This gives c A(0)=0, so A(0)=0. Now put +x=0 to obtain `A(c y)=c A(y)`. For any z, choose y=c^-1 z. Equation (1) +then becomes `A(x+z)=A(x)+A(z)`. This proves additivity for every x,z. + +Conversely, an additive map commutes with integer multiplication. In a +dyadic module, `2 A(z/2)=A(z)` and the half is unique, hence +`A(z/2)=A(z)/2`. Induction gives dyadic homogeneity and therefore (1). +Thus any one such unchanged ADD forces the full dyadic-linear condition. +The theorem also holds on real or complex vector spaces viewed as dyadic +modules. Additivity by itself does **not** assert continuity, real +linearity, or complex linearity. With continuity, the usual dyadic-density +argument gives real linearity; that is a separate additional hypothesis. + +Coefficients such as 3/4 are allowed in the source, but the certificate +deliberately uses only unit dyadic coefficients. No division by three, no +finite-grid closure, and no rounding law is assumed in the argument. + +## 3. Binding to every active source frame + +The sole executed scientific input is Cao Yifan's round-three actual word, +`research/kappa-round3-warp-20261022/ACTUAL-WORD.json.gz`, at canonical base +`b91956876e5b4122fd89179f1b57557ff8378f15`. Its compressed SHA256 is +`7679daa4ec6a40f56fc7f0202379a6f454310e94945aba4f48beaaaafb838d05`. +This is the same actual word used by PR4966. The parser is independently +written and imports no predecessor verifier, native oracle, or inverse recipe. + +For **each** retained forward and backward orientation the exact replay finds: + +| Object | Count | +|---|---:| +| Source events | 21,449 | +| Persistent L fields | 632 | +| Active frames | 1,002 | +| Frames with a distinct persistent L-to-L unit-dyadic ADD | 1,002 | +| Owned-center macros | 8 | +| Paid occurrences including centers | 3,298 | + +Here active frames means frames occurring in the source's scalar, climb, +center, or warp records. Phase and adapter records are retained markers; +their physical action is not implemented by this audit. RESULT.json gives +the first qualifying ADD's exact event index, coefficient, register pair +and full record for **every frame in each orientation**. Witnesses occur +outside owned-center macros. Frame ids and dimensions are not conflated: +all used ids are checked, including the empty frame and the full frame. + +The parser replays scalar/paid/warp frame chronology and both persistent +endpoint lists. It verifies the actual paid profile +`{1:2201,2:412,3:510,4:127,5:40,8:8}` and all eight center macros, including +the separation of unchanged capture sources from modified destinations. +It does not evaluate their physical Gaussian matrices. + +Consequently a gatewise coherent-potential proof of this **unchanged** +word, with a shared all-input map per frame, must use additive potentials +on all 1,002 active frames in each orientation. There is no uncovered +transit-only frame where this recipe can hide a nonlinear potential. + +The all-input requirement is a contract, not something inferred from a +finite fixture. It is also compatible with arbitrary persistent dirt: +conditional on bijective persistent paid children and warps, each ordinary +persistent ADD/SCALE prefix is bijective. Each completed owned macro is a +shear from its unchanged capture sources into disjoint destinations, even +for a deterministic nonlinear center. It too is a persistent bijection. +Every witness is outside those macros. Thus under those explicit premises +the two persistent fields at a witness can vary independently. This does +not promote a test of one restricted input trajectory into (1). + +## 4. Exact distinctions from inverse and warp compatibility + +### Reversible rounded maps + +On Q² define `R(x,y)=(x+floor(y/2),y)`. Its exact inverse is +`R^-1(u,v)=(u-floor(v/2),v)`. It is a deterministic reversible rounded +shear and fixes zero. Yet at x=y=(0,1) and c=1, + +`R(x+y)=(1,2)` while `R(x)+R(y)=(0,2)`. + +Every local inverse round trip can pass while the unchanged ADD fails +equivariance. This example concerns a map that is itself proposed as a +potential; the theorem does not say that each internal rounded shear of +an otherwise additive complete realization is individually forbidden. + +### Even compatibility with all unitaries is insufficient + +On R^d or C^d define `P(v)=||v||² v`. It is a bijection: it maps each ray's +nonnegative radial parameter r to r³. The inverse is zero at zero and +`P^-1(w)=||w||^(-2/3) w` otherwise. For **every** unitary U, + +`P(Uv)=U P(v)`. + +Nevertheless at a unit vector e, +`P(e+e)=8e` and `P(e)+P(e)=2e`. Thus fixed unitary intertwining, zero +preservation, and exact two-sided inversion do not logically imply (1). +For an arbitrarily small positive t, the bijection +`P_t(v)=(1+t||v||²)v` gives the same distinction while being within t of +identity on the unit ball. Small error on a ball is not exact equivariance. + +For example, given unitary ideal frame maps C_f and unitary ideal warp +maps `C_b W C_a^-1`, choose `A_f=P C_f`. All pure transition and warp +conjugations then equal their ideal unitary maps, because P commutes with +every unitary. Their equations do not detect this nonlinear common gauge. +The unchanged ADD does detect it. This is a counterexample to sufficiency +of those equations as a **gatewise gauge proof**, not a counterexample to +the endpoint of the ideal native word. That ideal word is unchanged in +this example and may already have the desired endpoint. + +The verifier checks the rounded example, its two-sided inverses on 49 exact +rational points, the radial ADD discrepancy, and 147 exact rational +orthogonal-equivariance instances. The all-unitary statement follows from +norm preservation in the written proof, not from those 147 instances. +It also checks 12,005 rational ADD instances for an invertible linear map. + +## 5. Separate closed-walk obligations of the paid graph + +There is a second, independent distinction between inverse pairs and frame +potentials. Normalize paid transitions to maps H_e on a common field and +temporarily disregard warp edges. On any connected graph, specified +invertible H_e admit `H_e=A_b A_a^-1` if and only if every fundamental +closed-walk product is identity. Choose a root and a spanning tree. The +tree fixes each A_v from an arbitrary A_root. Every non-tree edge's equation +is exactly its fundamental closed-walk equation. This proves both directions +for arbitrary bijections, without commutativity or linearity. Reverse +traversal uses the actual inverse. Correct inverse pairs only check the +immediate edge/reverse walk and do not test other cycles. + +The source graph in each orientation has 1,002 vertices, one component, +3,298 paid occurrences, and hence 2,297 non-tree occurrence tests. If +parallel occurrences are identified by unordered endpoint pair, its 2,855 +simple edges instead have cycle rank 1,854. RESULT.json retains the full +deterministic forest/chord event partition; a separate BFS component count +cross-checks the union/find calculation. These are counts of **potential +tests**, not 2,297 proved failures or algebraically independent constraints +on a particular shared implementation. Warp constraints and scalar +compatibility remain additional conditions. + +The graph lemma is elementary and not claimed as new mathematics. Nick +Petalas's `coherent-transvection-neighborhood` uses related spanning-tree +holonomy constraints for binary symplectic axes. Its object is a restricted +geometric chart move, whereas this census binds actual paid occurrences +and the nonlinear numerical-potential boundary of PR4966. + +## 6. Constructive choices left open + +An additive family satisfying all paid and warp equations would clear this +local scalar obstruction. It still needs Gaussian/frame compatibility, +fresh independent D factors, an actual paired caller, and a complete +precision/storage/routing/recursive bill. This audit constructs no such +family and does not prove one impossible. + +Alternatively change each scalar gate to its literal conjugate under the +chosen nonlinear potentials, or prove and pay a quantitative error bound +for its failure to commute. Both change the present contract and require +a fresh caller and invoice. A global correlated-error construction may +also use an argument entirely outside this gatewise recipe. It is not +excluded by this theorem, the cycle census, or PR4966's independent-error +tariff. No selected frontier or multiplication theorem is changed. diff --git a/research/coherent-frame-additivity/README.md b/research/coherent-frame-additivity/README.md new file mode 100644 index 0000000000..5c72c03ba7 --- /dev/null +++ b/research/coherent-frame-additivity/README.md @@ -0,0 +1,124 @@ +# Coherent frame potentials need additive scalar compatibility + +**Scoped written theorem and independent source audit; no new κ.** + +PR4966 supplies exact inverse recipes for deterministic native realizations +and leaves a coherent-frame compatibility target for a future paired caller. +This contribution checks an additional requirement of that target: a shared +frame potential commuting through unchanged scalar ADDs on arbitrary inputs +must be additive. Inverses and unitary warp equations alone do not imply it. + +For a nonzero dyadic unit c, commuting a potential A through +`(x,y) -> (x+c y,y)` is equivalent to + +`A(x+c y)=A(x)+c A(y)` for all x,y. + +Putting y=0, then x=0, and finally y=c^-1 z proves additivity. The converse +follows from dyadic homogeneity. [PROOF.md](PROOF.md) states the exact domains +and the gatewise claim boundary; there is no proof-assistant claim. + +The independently written source parser checks both actual round-three +orientations, each with 21,449 events and 632 persistent fields. **All 1,002 +active frames in each orientation have a distinct persistent-register ADD +with a unit dyadic coefficient, outside every owned-center macro.** The +certificate retains one exact source event per frame per orientation, +including its register pair and coefficient. Both persistent endpoint frame +lists, all eight owned macros, and the retained paid profile are checked. + +Two exact distinctions prevent an invalid implication: + +- The reversible rounded map `(x,y) -> (x+floor(y/2),y)` has exact two-sided + inverses but fails ADD equivariance at x=y=(0,1). +- The radial bijection `v -> ||v||² v` commutes with **every unitary** but + still fails ADD equivariance. Its all-unitary property is proved from + norm preservation, rather than inferred from finite tests. + +Separately, each paid occurrence graph has 1,002 vertices, 3,298 edges, +one component and 2,297 fundamental closed-walk tests for a potential +assignment. Identifying parallel unordered pairs gives 2,855 edges and +cycle rank 1,854. These counts do not show that a particular implementation +fails any test. They identify obligations that inverse pairs alone leave. + +This closes one local implication in the **gatewise coherent-potential +recipe with unchanged scalar gates**. It does not exclude global correlated +error schemes, changed scalar circuits, additive coherent realizations, or +a different paired caller. Precision, independent fresh D factors, physical +Gaussian/frame compatibility, workspace, routing, recursive pricing and BIT +admission remain open. The selected conditional κ is unchanged. + +## Reproduce + +From the repository root, with standard-library Python 3.12: + +```sh +python3.12 -I -B research/coherent-frame-additivity/verify.py +python3.12 -I -O -B research/coherent-frame-additivity/verify.py +python3.12 -B scripts/research_package.py --package research/coherent-frame-additivity +``` + +Expected direct output: + +```text +PASS_COHERENT_FRAME_ADDITIVITY frames_per_orientation=1002 paid_cycle_rank=2297 controls=5 no_new_kappa +``` + +[RESULT.json](RESULT.json) records the recomputed summary and the SHA256 of +the canonical decompressed [certificate](CERTIFICATE.json.gz). Default replay +is read-only. `--write-result NEW_PATH` explicitly creates a new summary and +its sibling certificate, without overwriting either. Gzip headers and streams +are not mathematical evidence: replay compares exact canonical payload bytes. + +Finite corroboration includes 12,005 rational linear ADD cases, 98 rounded +two-sided inverse round trips and 147 rational radial/orthogonal cases. +Four semantic source mutations and a changed-source-byte control must fail +for their specified reasons. Conditions use exceptions and remain active +under `-O`. No native physical suite, selected cold replay, Lean build or +full multiplication theorem is part of this audit. + +## Sources and overlap + +Canonical base: `b91956876e5b4122fd89179f1b57557ff8378f15`, priority revision 7. +Assignment seed: `7497f9f029574287f7cf5b3d5415bf74`, independent-verification +track, `formal-interface-lemma` card. The scope change to a written local +boundary theorem is declared in [TASK.json](TASK.json). + +[SOURCES.json](SOURCES.json) pins the sole executed scientific input, +Cao Yifan's actual round-three word, and historical assignment context. +[VENDORED.json](VENDORED.json) authenticates Yiyang's exact PR4966 inverse +proof at `039b6ea51ab7a7efb38fc6851f345839683251b0`; no predecessor +implementation is imported or executed. + +The [overlap receipt](OVERLAP.json) records live open-PR/discussion and local +note coverage. PR4966 already distinguishes exact reversibility from linear +operator identities; the new evidence is the ADD criterion and complete +all-active-frame source binding. Nick Petalas's coherent-transvection +neighborhood proves geometric graph transport constraints, which receive +credit here; the elementary graph lemma is not claimed as new mathematics. +Coverage does not include every code diff or unpublished work and is not +a novelty certificate. + +Canonical investigation: +[Discussion4611](https://github.com/CrocSwap/integer-mult-bounds/discussions/4611#discussioncomment-19138553). + +## Open next questions + +- Can additive actual frame potentials satisfy the paid closed-walk and + unchanged warp equations at a charged precision? Start with one actual + non-tree paid edge and its forest path, including their true recursive + realizations. Such realizations and their full bill are not supplied here. +- If nonlinear potentials are retained, can a literal conjugated scalar + gate or a paid quantitative error bound replace unchanged ADDs? Start with + one emitted persistent-register witness and carry the correction through + the actual two-call caller. Unknown correction and storage costs are not zero. + +## Credit + +Yiyang (@Lyy-iiis), with OpenAI Codex assistance, supplies PR4966's paid-site +precision census and same-realization inverse construction. Cao Yifan supplies +the round-three actual word and its retained predecessor lineage. The +two-full Laurent-border, native E8/Clifford and PR4610 predecessor attribution +remains with the source authors. Nick Petalas supplies the related binary +symplectic graph-neighborhood result. No claim of independent human review +is made. Prepared by Cinna Davis with substantial OpenAI Codex assistance +in research, proof explanation, implementation, verification and writing. +New work is Apache-2.0; the vendored predecessor retains its original notice. diff --git a/research/coherent-frame-additivity/RESULT.json b/research/coherent-frame-additivity/RESULT.json new file mode 100644 index 0000000000..bd7e902cce --- /dev/null +++ b/research/coherent-frame-additivity/RESULT.json @@ -0,0 +1,134 @@ +{ + "certificate": { + "canonical_payload_sha256": "8c1f5ca6b7fc8c5493f5d57a6118fb4f726a10cdbf0d721c841fd7b71690de97", + "path": "CERTIFICATE.json.gz" + }, + "claim": "gatewise_frame_additivity_no_new_kappa", + "mathematical_checks": { + "linear_gate_cases": 12005, + "radial_counterexample": { + "coefficient": 1, + "left": [ + 8, + 0 + ], + "right": [ + 2, + 0 + ], + "x": [ + 1, + 0 + ], + "y": [ + 1, + 0 + ] + }, + "radial_unitary_cases": 147, + "rounded_counterexample": { + "coefficient": 1, + "left": [ + 1, + 2 + ], + "right": [ + 0, + 2 + ], + "x": [ + 0, + 1 + ], + "y": [ + 0, + 1 + ] + }, + "rounded_two_sided_round_trips": 98 + }, + "orientations": { + "backward": { + "active_frames": 1002, + "frame_dimension_histogram": { + "0": 1, + "1": 115, + "2": 169, + "3": 168, + "4": 66, + "5": 46, + "6": 146, + "7": 168, + "8": 122, + "9": 1 + }, + "owned_macros": 8, + "paid_graph": { + "components": 1, + "occurrence_cycle_rank": 2297, + "paid_occurrences": 3298, + "simple_cycle_rank": 1854, + "simple_edges": 2855, + "vertices": 1002 + }, + "persistent_roles": 632, + "scalar_counts": { + "add": 16273, + "clear": 16, + "scale": 1164 + }, + "source_events": 21449 + }, + "forward": { + "active_frames": 1002, + "frame_dimension_histogram": { + "0": 1, + "1": 115, + "2": 169, + "3": 168, + "4": 66, + "5": 46, + "6": 146, + "7": 168, + "8": 122, + "9": 1 + }, + "owned_macros": 8, + "paid_graph": { + "components": 1, + "occurrence_cycle_rank": 2297, + "paid_occurrences": 3298, + "simple_cycle_rank": 1854, + "simple_edges": 2855, + "vertices": 1002 + }, + "persistent_roles": 632, + "scalar_counts": { + "add": 16265, + "clear": 16, + "copy": 8, + "scale": 1164 + }, + "source_events": 21449 + } + }, + "predecessor_context": { + "credit": "Yiyang (@Lyy-iiis), with substantial OpenAI Codex assistance. Apache-2.0.", + "path": "vendor/PR4966-INVERSE-PROOF.md", + "sha256": "753f0e1e7f6305ed550cb7247204190d9f4f258e07744e16ee55a35ee42e3f85", + "source_blob": "7d939c4dc662af9cdbf306b7e5ab4f4acf21c35c", + "source_commit": "039b6ea51ab7a7efb38fc6851f345839683251b0", + "source_path": "research/two-full-border-paid-precision/inverse-interface/PROOF.md", + "source_repository": "https://github.com/CrocSwap/integer-mult-bounds", + "usage": "Quoted target and predecessor context; no predecessor implementation is executed." + }, + "rejection_controls": [ + "self_add", + "zero_coefficient", + "boolean_coefficient", + "wrong_frame" + ], + "schema_version": 1, + "source": "research/kappa-round3-warp-20261022/ACTUAL-WORD.json.gz", + "source_sha256": "7679daa4ec6a40f56fc7f0202379a6f454310e94945aba4f48beaaaafb838d05" +} diff --git a/research/coherent-frame-additivity/SOURCES.json b/research/coherent-frame-additivity/SOURCES.json new file mode 100644 index 0000000000..504e70d52e --- /dev/null +++ b/research/coherent-frame-additivity/SOURCES.json @@ -0,0 +1,24 @@ +{ + "schema_version": 1, + "base_commit": "b91956876e5b4122fd89179f1b57557ff8378f15", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "c35482cd9035843b15a634cc8276a7e1e40e8395", + "sha256": "6fe0a099b89aa2aed796a13c3a21dafc63f3388ebf397464e44e0451893b9375" + }, + { + "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": "input", + "git_blob": "46d929df83817b85a5387bcdb9745e0627d6366e", + "sha256": "7679daa4ec6a40f56fc7f0202379a6f454310e94945aba4f48beaaaafb838d05" + } + ] +} diff --git a/research/coherent-frame-additivity/TASK.json b/research/coherent-frame-additivity/TASK.json new file mode 100644 index 0000000000..bebb2d2b78 --- /dev/null +++ b/research/coherent-frame-additivity/TASK.json @@ -0,0 +1,113 @@ +{ + "schema_version": 1, + "task_id": "formal-interface-lemma", + "priority_revision": 7, + "base_commit": "b91956876e5b4122fd89179f1b57557ff8378f15", + "original_card": { + "id": "formal-interface-lemma", + "question": "Can one uncovered interface implication be formalized with exact caller and certificate bindings?", + "starting_points": [ + "docs/research/research-family-status.md", + "certificates/selected-result.json", + "research/gate-operand-parity-lean/README.md", + "research/staged544-certified-endpoint/README.md", + "research/unconditional-batched-crt/README.md" + ], + "methods": [ + "Formalize a missing boundary lemma identified by the selected review.", + "Audit a formal theorem-to-certificate binding independently." + ], + "acceptance_gate": "State the exact formalized proposition and remaining assumptions; avoid duplicate arithmetic formalizations already present.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Inventory the gate-operand parity lemma (#3807) and certified endpoint arithmetic (#3857). Neither is a full multiplication proof. For #4100, audit the compact-switch statement and its hypotheses before formalizing it.", + "scope": "Source-binding orientation only; no scientific replay, theorem acceptance or supplier admission. Budget any heavy replay separately." + }, + "first_experiment": "Write one missing statement with quantified hypotheses, actual caller and existing coverage. A compact-switch lemma is a candidate only after its mathematical contract is reviewed. Establish a bounded proof plan before a separately budgeted proof-assistant build; do not rerun large Lean jobs as orientation.", + "bottleneck_link": "A missing interface proof can reduce the conditional gap even if it does not change kappa.", + "allowed_variations": [ + "Narrow to one formal lemma or one theorem-to-certificate binding." + ], + "scope_change_triggers": [ + "Formalizing already-covered arithmetic and claiming the full multiplication theorem." + ], + "overlap_terms": [ + "hyperplane end", + "formal interface", + "Lean binding", + "3807", + "3857", + "4100", + "gate-operand-parity-lean", + "staged544-certified-endpoint", + "unconditional-batched-crt" + ], + "existing_checks": [ + { + "scope": "PR #3807: scoped gate-operand parity formalization.", + "evidence": "research/gate-operand-parity-lean/README.md", + "remaining": "Exact theorem-to-caller binding and genuinely uncovered interface lemmas.", + "status": "author-checked", + "source_commit": "4c3530f42a6abcc48e7a6bcffd6c901911dc8269", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "PR #3857: certified real-power moment/endpoint arithmetic.", + "evidence": "research/staged544-certified-endpoint/README.md", + "remaining": "Uniform algorithmic implications, not another endpoint digit.", + "status": "author-checked", + "source_commit": "ef4315b8caa605e47a2515004845eb2d2ed71a86", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "PR #4100: compact-switch formalization proposed as future validation.", + "evidence": "research/unconditional-batched-crt/README.md", + "remaining": "Audit the statement and assumptions before a formal proof campaign.", + "status": "author-checked", + "source_commit": "337d04939571a637aeab54a0f58f54fde811663a", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + } + ] + }, + "scope_status": "changed", + "actual_scope": "Prove the all-input ADD equivariance criterion for shared frame potentials and bind its necessity to all active frames in both actual round-three orientations.", + "scope_change_reason": "The selected proof retains precision/frame premises. PR4966 proposes coherent potentials as a future compatibility target; this is a written boundary theorem with exact source checks, not a proof-assistant formalization or an endpoint-digit calculation.", + "bottleneck_link": "A two-full Laurent controller needs a correlated precision implementation. The theorem identifies scalar compatibility missing from a gatewise nonlinear-potential proof and prevents inverse/warp equations from being mistaken for a complete caller.", + "budget_minutes": 60, + "stop_rule": "Finish this single local implication, source census, counterexamples, registered replay and focused PR; then refresh canonical main and choose a new campaign round.", + "outcome": "completed", + "evidence": "Written PROOF.md; RESULT.json; exact canonical CERTIFICATE.json.gz with 2,004 source witnesses and two paid-graph forest/chord partitions; independently written verify.py with positive cases and five specified controls.", + "author": "Cinna Davis, with OpenAI Codex assistance", + "ai_assistance": "Substantial OpenAI Codex assistance in research, proof explanation, implementation, testing and writing; no independent human review claimed.", + "open_questions": [ + { + "question": "Can additive actual frame potentials satisfy paid and unchanged warp equations with a complete precision bill?", + "why_it_matters": "This would address the scalar compatibility boundary without changing the retained word.", + "first_step": "Evaluate one actual fundamental paid closed walk with the proposed recursive realizations.", + "blocked_by": "Actual coherent child realizations and their precision/storage bill are not supplied." + }, + { + "question": "Can changed scalar gates or a quantitative defect bound support nonlinear coherent potentials?", + "why_it_matters": "A changed caller can use an argument outside unchanged-gate equivariance.", + "first_step": "Implement the literal conjugate of one certificate ADD and price its full two-call use.", + "blocked_by": "No such paid scalar correction/caller is constructed here." + } + ], + "assignment": { + "seed": "7497f9f029574287f7cf5b3d5415bf74", + "track": "independent-verification", + "base_commit": "b91956876e5b4122fd89179f1b57557ff8378f15", + "priority_revision": 7, + "selected_record_sha256": "6fe0a099b89aa2aed796a13c3a21dafc63f3388ebf397464e44e0451893b9375", + "candidate_task_ids": [ + "formal-interface-lemma", + "independent-moment" + ], + "selected_task_id": "formal-interface-lemma" + } +} diff --git a/research/coherent-frame-additivity/VENDORED.json b/research/coherent-frame-additivity/VENDORED.json new file mode 100644 index 0000000000..97b0069108 --- /dev/null +++ b/research/coherent-frame-additivity/VENDORED.json @@ -0,0 +1,14 @@ +{ + "files": [ + { + "path": "vendor/PR4966-INVERSE-PROOF.md", + "source_repository": "https://github.com/CrocSwap/integer-mult-bounds", + "source_commit": "039b6ea51ab7a7efb38fc6851f345839683251b0", + "source_path": "research/two-full-border-paid-precision/inverse-interface/PROOF.md", + "source_blob": "7d939c4dc662af9cdbf306b7e5ab4f4acf21c35c", + "sha256": "753f0e1e7f6305ed550cb7247204190d9f4f258e07744e16ee55a35ee42e3f85", + "usage": "Quoted target and predecessor context; no predecessor implementation is executed.", + "credit": "Yiyang (@Lyy-iiis), with substantial OpenAI Codex assistance. Apache-2.0." + } + ] +} diff --git a/research/coherent-frame-additivity/VERIFY.json b/research/coherent-frame-additivity/VERIFY.json new file mode 100644 index 0000000000..2ab45d0f1e --- /dev/null +++ b/research/coherent-frame-additivity/VERIFY.json @@ -0,0 +1,32 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/kappa-round3-warp-20261022/ACTUAL-WORD.json.gz" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 30, + "checks": "All 2,004 active-frame ADD witnesses, scalar/paid/warp frame chronology, both endpoint lists, eight macros per orientation, exact graph ranks, linear positives, nonlinear counterexamples and five specified controls." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 30, + "checks": "Identical exact source and certificate replay with optimization enabled; all rejection checks remain active." + } + ] +} diff --git a/research/coherent-frame-additivity/vendor/PR4966-INVERSE-PROOF.md b/research/coherent-frame-additivity/vendor/PR4966-INVERSE-PROOF.md new file mode 100644 index 0000000000..7d939c4dc6 --- /dev/null +++ b/research/coherent-frame-additivity/vendor/PR4966-INVERSE-PROOF.md @@ -0,0 +1,220 @@ +# A same-cost inverse for the actual owned-center macros + +Yiyang (@Lyy-iiis), with substantial OpenAI Codex assistance. Apache-2.0. + +This is a positive inverse-interface construction for both actual serialized +orientations of the round-three native word in the PR4610 lineage. It removes +the owned-CLEAR obstruction to a particular coherent +inverse construction without adding paid calls. It does not prove a new +Gaussian supplier, a recursive approximation theorem, or an improved bound. + +The source is Cao Yifan's round-three native word at +`research/kappa-round3-warp-20261022/ACTUAL-WORD.json.gz`. Its SHA-256 is +`7679daa4ec6a40f56fc7f0202379a6f454310e94945aba4f48beaaaafb838d05`, and its +Git blob is `46d929df83817b85a5387bcdb9745e0627d6366e`. Identical bytes are +present at revisions `0ce1b5c9fb7163d0b2f0ac3db95fc418dbbcec62`, +`1eb8da6cfb35512c0cc2533413e5ca42f48e13c6` and the current base below. +Our initial copy came unchanged through PR4694, head +`2add42d1edf14a263abe90a3bcde67fc1ba30768`, at +`research/retained-center-extension/inputs/round3-native.json.gz`. +No frozen source has been modified. Current research coordination is based +on refreshed main `cef4b52f2a59009865bf8eabde1be3f159063703`. + +## The local identity + +Let x_i be persistent capture sources, let y_j be persistent target roles +disjoint from every x_i, and let A be a deterministic function. Fix capture +coefficients b_i and fanout coefficients a_j. Consider the macro + +``` +c = 0 +c = sum_i b_i x_i +c = A(c) +for j: y_j += a_j c +c = 0 +``` + +Writing s for the captured linear form, the persistent endpoint is +`x_i'=x_i`, `y_j'=y_j+a_j A(s)`. On arbitrary fresh persistent inputs, +its inverse is + +``` +c = 0 +c = sum_i b_i x_i +c = SAME_A(c) +for j: y_j -= a_j c +c = 0 +``` + +Both directions use one invocation of the same realization A. The inverse +does not call A^-1, reconstruct discarded data from completed outputs, or +reverse a CLEAR. Every capture source remains unchanged, so both the captured +linear form and the second evaluation are identical. This identity does not need A to be linear, +invertible, unitary, or numerically exact. It needs repeatable evaluation on +the same input and exact adding/subtracting of the same increments. + +Literal reversal of the extended circuit with fresh zero garbage would +attempt to recover a discarded, generally nonzero C0 value from zero. The +present construction instead computes a different straight-line program +for the inverse of the persistent map. + +## Binding to both retained source orientations + +Each retained program has 21,449 records, 632 persistent L roles and one +reused C0. Each contains eight consecutive 26-record center macros with +sixteen CLEARs. The forward program has eight COPYs; the backward program +gathers by ADD and has no COPYs. Every COPY/CLEAR lies inside these macros. +There is no other explicit owned or zero-buffer role in this serialized layer. + +Every macro clears C0, captures a linear form, calls its paid center, +performs its fanout and clears C0 again. The two source shapes are: + +| Retained orientation | Capture | Paid center frames | Fanout | +| --- | --- | --- | --- | +| Forward | Copy one persistent source | rank 8 to rank 0 | 22 ADDs, each coefficient ±1/4 | +| Backward | Sum 22 persistent sources, each coefficient ±1/4 | rank 0 to rank 8 | One ADD, coefficient -1 | + +The forward sources, and corresponding backward destinations, are +`92,57,81,224,11,240,9,256`. In each backward macro the 22 capture sources +are disjoint from its single destination. In both orientations all capture +sources remain unmodified between capture and final clear. The generator +checks every record, frame, coefficient and capture/destination intersection. + +Separately for each retained word, reverse the order of these macros and all other +operations. Invert persistent ADDs, invert nonzero dyadic-unit SCALEs, +invert each actual warp/adapter, and call the actual inverse of the same +persistent paid-child realization. Replace each center macro by the +same-A/negative-fanout macro above. Each inverse center macro retains its +source macro's paid orientation: rank eight to zero in the forward source, +zero to rank eight in the backward source. Neither is the literal reverse +frame itinerary. The retained backward program is not assumed to be the +actual inverse of an approximate forward program; it gets its own inverse. + +The resulting persistent input frames are the source's final frames and +the resulting output frames are its start frames. Every intermediate scalar +source/destination frame and every paid/warp boundary has been checked. + +## Exact paid bill + +Each retained complete word and its constructed actual inverse have this +same paid profile: + +``` +{1:2201, 2:412, 3:510, 4:127, 5:40, 8:8}. +``` + +Each orientation retains all eight paid rank-eight jobs; no erased buffer +is credited as an independent output. There are no extra paid rank-one +reconstruction calls. In particular, the initially considered final-center +reconstruction is unnecessary: the forward macro's actual discarded value +is in frame zero, not frame eight. + +The inverse has the same scalar gate count inside each center macro. +Negating a fanout coefficient preserves its magnitude and denominator. +Other inverse scalar/route implementation constants must still be included +in any compiler allowance; they are not paid recursive calls. + +After the established disjoint-axis splitting, a two-full forward or +coherently inverted recipe therefore retains the optimistic paid invoice +`{1:4656,2:920,3:1386}`. At the declared rank-call level the macro replacement +adds no paid calls; it makes no assertion about additional precision costs. +It does not establish that the +full approximate algorithm can attain the raw `.0048568755...` crossing. + +## Workspace and exact arithmetic contract + +Each persistent paid child is required to be a bijection on its declared +field, with an implementation of the inverse of that SAME realization. +The unchanged invoice assumes this inverse is available at the same declared +rank charge. Both directions must restore any private workspace. A statement only about +the child's projected productive output is insufficient. Center children +need only be deterministic on their field and privately clean, since they +are recomputed in the same orientation. + +Under these hypotheses the complete persistent program is a composition +of bijections. It is therefore a bijection, and the constructed inverse is +its exact two-sided inverse. This structural closure survives finite +composition, permutation routing and the finite precompiler's fixed +schedule. It does not assert that the resulting bijection equals, or is +close to, its intended Gaussian operator. + +Exact dyadic arithmetic on a sufficiently fine grid makes ADD/subtract and +nonzero dyadic SCALE mutually reversible without quantization at return. +A finite dyadic word always has such an exact grid for finite dyadic input; +its necessary width and magnitude are not automatically the inherited +linear semantic guard bound. A fully charged uniform precision proof is +still required as the word and accuracy vary. + +There is also a narrowly reversible rounded-shear implementation: compute +the deterministic increment `round_grid(a_j A(s))` and then add it exactly +to y_j. The inverse recomputes and subtracts that identical increment. +The capture may itself be evaluated by a fixed deterministic rule, provided +the identical rule sees the identical unchanged sources in both directions. +This does not justify rounding `y_j+a_j A(s)` as a whole, rounding a SCALE, +overflowing an accumulator, changing the child rounding policy between +directions, or dropping private garbage. + +A rounded bijection can be nonlinear. Its exact reversibility alone does +not supply the linear operator-ring identities used by the Laurent border +controller. Those identities require their own proof for the chosen +actual realization. + +## Executed checks + +`verify.py` authenticates the actual source bytes and Git blob, extracts +all sixteen macros, and recomputes `INVERSE-RECIPE.json.gz`, an explicitly typed +inverse IR for both orientations with source event IDs. It distinguishes +`same_retained_orientation` center +children from `actual_inverse` persistent children. It is a reviewable +recipe, not an already admitted native compiler format. + +The checker passes under isolated optimized Python: + +``` +PYTHONDONTWRITEBYTECODE=1 python3 -I -B -O verify.py +``` + +The frozen receipt is `RESULT.json`. Default verification is read-only and +compares both the canonical inverse recipe and the recomputed receipt. Use +`--regenerate` explicitly to update them after reviewing a construction +change. The recipe hash covers its exact decompressed canonical JSON; +gzip headers and compression streams are not mathematical evidence. + +For each source orientation, the checker verifies both full 632-role round +trips on two sets of independent two-coordinate rational inputs: eight +whole-word round trips in total. Each persistent query site is assigned its own near-identity +dyadic shear, deliberately without imposing Gaussian/frame relations; +each center uses a deterministic nonlinear rounded function. Thus this is +a stress test of the inverse contract, not another ideal native endpoint +replay. Five controls in each orientation reject a changed center realization, +an unnegated fanout, a fresh nominal inverse instead of the actual inverse, +a changed captured linear form, and a source-overwriting fanout. + +An independent native-integration check previously confirmed the eight +forward macros and 48 local round trips. The present checker does not import +that check; its generalized source parser and whole-word round trips cover +both source orientations separately. + +## What this does not yet supply + +The inverse of a complete native word reverses its productive D orientation. +It is not automatically a second fresh-D supplier with opposite central +shear. Approximate internal children may also destroy the source's +`D U(q)` factorization and other Gaussian/frame relations. Same-word +invertibility does not recover those identities. + +Consequently the remaining constructive task is a caller/compiler whose +*actual* two orientations use this coherent inverse and whose complete +main/helper endpoints still match the intended jobs. Error correlation, +private-workspace cleanup, scalar range, exact or rounded execution and +the full paid invoice must be proved together at that caller. The macro +result supplies one concrete piece of this task without a paid-call +surcharge; it does not stand in for the rest. + +A concrete sufficient compatibility target is a family of coherent frame +potentials A_f: an actual paid climb from a to b would equal A_b A_a^-1, +and an actual warp W would equal A_new W A_old^-1. Inverse pairs alone do +not imply these relations. The inherited physical warps would need the +corresponding intertwining without new paid calls, together with the +fresh-D caller and precision bounds above. Testing that requirement on +the actual paid-site realization is an open next step. diff --git a/research/coherent-frame-additivity/verify.py b/research/coherent-frame-additivity/verify.py new file mode 100644 index 0000000000..f87085ce50 --- /dev/null +++ b/research/coherent-frame-additivity/verify.py @@ -0,0 +1,330 @@ +#!/usr/bin/env python3 +"""Source witnesses for gatewise coherent-frame additivity; no new kappa. + +Cinna Davis, with OpenAI Codex assistance. Apache-2.0. +""" +import argparse +from collections import Counter, defaultdict, deque +from fractions import Fraction as F +import gzip +import hashlib +import json +from pathlib import Path + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +SOURCE = 'research/kappa-round3-warp-20261022/ACTUAL-WORD.json.gz' +SOURCE_SHA = '7679daa4ec6a40f56fc7f0202379a6f454310e94945aba4f48beaaaafb838d05' + + +class Rejected(ValueError): + pass + + +def need(ok, reason): + if not ok: + raise Rejected(reason) + + +def power_two(x): + return type(x) is int and x > 0 and x & (x - 1) == 0 + + +def coefficient(g): + need(type(g[-2]) is int and type(g[-1]) is int and g[-1] != 0, + 'rational coefficient') + return F(g[-2], g[-1]) + + +def unit_dyadic(c): + return power_two(abs(c.numerator)) and power_two(c.denominator) + + +def graph_counts(edges): + parent = {} + + def find(v): + parent.setdefault(v, v) + while parent[v] != v: + parent[v] = parent[parent[v]] + v = parent[v] + return v + + tree, chords = [], [] + for event, a, b in edges: + ra, rb = find(a), find(b) + if ra == rb: + chords.append(event) + else: + parent[ra] = rb + tree.append(event) + components = len({find(v) for v in parent}) + simple = {tuple(sorted((a, b))) for _, a, b in edges} + # Independent component/rank count by breadth-first search. + adjacency = defaultdict(set) + for a, b in simple: + adjacency[a].add(b); adjacency[b].add(a) + unseen = set(adjacency) + bfs_components = 0 + while unseen: + bfs_components += 1 + queue = deque([unseen.pop()]) + while queue: + for v in adjacency[queue.popleft()]: + if v in unseen: + unseen.remove(v); queue.append(v) + need(bfs_components == components, 'independent component count') + need(len(tree) == len(parent) - components, 'spanning forest size') + need(len(chords) == len(edges) - len(parent) + components, 'fundamental cycle count') + return {'vertices': len(parent), 'components': components, + 'paid_occurrences': len(edges), 'simple_edges': len(simple), + 'occurrence_cycle_rank': len(chords), + 'simple_cycle_rank': len(simple) - len(parent) + components, + 'forest_event_ids': tree, 'chord_event_ids': chords} + + +def census(src, orientation): + canonical = src['canonical'] + frames = canonical['frames'] + p = src['programs'][orientation] + now = {('L', i): f for i, f in enumerate(canonical['start'])} + used, witnesses, paid = set(), {}, [] + scalar_counts, paid_counts = Counter(), Counter() + macros, macro, macro_open = [], [], False + + def frame(f): + need(type(f) is int and 0 <= f < len(frames), 'valid frame id') + used.add(f) + + def role(r): + need(isinstance(r, list) and len(r) == 2 and type(r[1]) is int, 'role shape') + need((r[0] == 'L' and 0 <= r[1] < len(canonical['start'])) or + r == ['C', 0], 'declared role') + return tuple(r) + + for i, e in enumerate(p): + k = e[0] + if k == 'scalar': + g, f = e[1:] + frame(f) + op = g[0]; scalar_counts[op] += 1 + d = role(g[1]) + if op == 'clear': + need(d == ('C', 0), 'only owned center is cleared') + if not macro_open: + macro_open, macro = True, [i] + else: + macro.append(i); macros.append(macro) + macro_open, macro = False, [] + now[d] = f + continue + if op == 'copy': + s = role(g[2]) + need(d == ('C', 0) and now.get(s) == f, 'center COPY input frame') + now[d] = f + elif op == 'add': + s, c = role(g[2]), coefficient(g) + need(d != s and c != 0, 'nonzero distinct-register ADD') + need(now.get(d) == now.get(s) == f, 'ADD frame chronology') + if d[0] == s[0] == 'L' and unit_dyadic(c): + need(not macro_open, 'persistent witness outside owned macro') + witnesses.setdefault(f, {'frame': f, 'dimension': len(frames[f]), + 'event': i, 'record': e, + 'coefficient': [c.numerator, c.denominator]}) + elif op == 'scale': + c = coefficient(g) + need(d[0] == 'L' and now.get(d) == f and unit_dyadic(c), + 'invertible dyadic persistent SCALE') + else: + raise Rejected('unknown scalar operation') + elif k == 'climb': + _, tag, a, old, new, rank = e + frame(old); frame(new) + need(tag == 'warp_retimed' and now.get(('L', a)) == old, 'paid entrance frame') + need(type(rank) is int and len(frames[new]) - len(frames[old]) == rank > 0, + 'paid rank increment') + now[('L', a)] = new + paid.append((i, old, new)); paid_counts[rank] += 1 + elif k == 'center': + _, a, old, new, rank = e + frame(old); frame(new) + need(macro_open and a == 0 and now.get(('C', a)) == old, 'owned center entrance') + need(type(rank) is int and abs(len(frames[new]) - len(frames[old])) == rank, + 'owned center rank') + now[('C', a)] = new + paid.append((i, old, new)); paid_counts[rank] += 1 + elif k == 'warp': + _, r, op, old, new = e + frame(old); frame(new) + a = role(r) + need(type(op) is int and op != 0 and abs(op) <= len(canonical['warps']), + 'declared warp id') + need(now.get(a) == old and len(frames[old]) == len(frames[new]), + 'warp frame chronology') + now[a] = new + else: + need(k in ('phase', 'adapter'), 'supported event kind') + if macro_open: + macro.append(i) + need(not macro_open and len(macros) == 8, 'eight closed owned macros') + need([now[('L', a)] for a in range(len(canonical['start']))] == canonical['final'], + 'persistent endpoint frames') + need(set(witnesses) == used, 'every active frame has a unit persistent ADD witness') + for ids in macros: + block = [p[i] for i in ids] + need(len(block) == 26 and sum(e[0] == 'center' for e in block) == 1, 'owned macro shape') + captures, destinations = set(), set() + for e in block: + if e[0] != 'scalar' or e[1][0] == 'clear': + continue + g = e[1] + if g[1] == ['C', 0]: + need(g[0] in ('add', 'copy') and g[2][0] == 'L', 'center capture') + captures.add(g[2][1]) + else: + need(g[0] == 'add' and g[2] == ['C', 0], 'center fanout') + destinations.add(g[1][1]) + need(captures and destinations and not captures & destinations, + 'capture sources disjoint from destinations') + need(dict(sorted(paid_counts.items())) == + {int(k): v for k, v in canonical['local_profile'].items()}, 'paid profile binding') + return {'source_events': len(p), 'active_frames': len(used), + 'persistent_roles': len(canonical['start']), 'owned_macros': len(macros), + 'scalar_counts': dict(sorted(scalar_counts.items())), + 'frame_dimension_histogram': dict(sorted(Counter(len(frames[f]) for f in used).items())), + 'witnesses': [witnesses[f] for f in sorted(witnesses)], 'paid_graph': graph_counts(paid)} + + +def plus(x, y): + return tuple(a + b for a, b in zip(x, y)) + + +def times(c, x): + return tuple(c * a for a in x) + + +def commute(A, c, x, y): + return A(plus(x, times(c, y))) == plus(A(x), times(c, A(y))) + + +def rounded_shear(v, inverse=False): + x, y = v + increment = y // 2 + return (x - increment if inverse else x + increment, y) + + +def radial(v): + return times(sum(x*x for x in v), v) + + +def mathematical_checks(): + points = [(F(a, 2), F(b, 2)) for a in range(-3, 4) for b in range(-3, 4)] + coeffs = [F(1), F(-1), F(1, 2), F(-1, 4), F(2)] + linear = lambda v: (v[0] + 2*v[1], v[0] + 3*v[1]) + checked = 0 + for x in points: + need(rounded_shear(rounded_shear(x), True) == x, 'rounded forward/inverse') + need(rounded_shear(rounded_shear(x, True)) == x, 'rounded inverse/forward') + for y in points: + for c in coeffs: + need(commute(linear, c, x, y), 'linear ADD positive control') + checked += 1 + x = (F(0), F(1)) + need(not commute(rounded_shear, F(1), x, x), 'nonlinear rounded ADD counterexample') + u = (F(1), F(0)) + need(not commute(radial, F(1), u, u), 'radial ADD counterexample') + unitary_checks = 0 + for a, b in [(F(0), F(1)), (F(3, 5), F(4, 5)), (F(5, 13), F(12, 13))]: + W = lambda v: (a*v[0] - b*v[1], b*v[0] + a*v[1]) + for v in points: + need(radial(W(v)) == W(radial(v)), 'radial unitary equivariance') + unitary_checks += 1 + S = lambda v: (v[0] + v[1], v[1]) + Sinv = lambda v: (v[0] - v[1], v[1]) + need(all(Sinv(S(v)) == S(Sinv(v)) == v for v in points), 'edge inverse pairs') + need(S(x) != x, 'nontrivial triangle holonomy') + return {'linear_gate_cases': checked, 'rounded_two_sided_round_trips': 2*len(points), + 'radial_unitary_cases': unitary_checks, + 'rounded_counterexample': {'x': [0, 1], 'y': [0, 1], 'coefficient': 1, + 'left': [1, 2], 'right': [0, 2]}, + 'radial_counterexample': {'x': [1, 0], 'y': [1, 0], 'coefficient': 1, + 'left': [8, 0], 'right': [2, 0]}} + + +def controls(src): + tests = [] + + def reject(name, change, expected): + altered = json.loads(json.dumps(src)); change(altered) + try: + census(altered, 'forward') + except Rejected as e: + need(str(e) == expected, 'specified rejection: ' + name + ': ' + str(e)) + tests.append(name) + else: + raise Rejected('mutation accepted: ' + name) + + event = census(src, 'forward')['witnesses'][0]['event'] + def gate(s): + return s['programs']['forward'][event][1] + reject('self_add', lambda s: gate(s).__setitem__(2, gate(s)[1]), + 'nonzero distinct-register ADD') + reject('zero_coefficient', lambda s: gate(s).__setitem__(3, 0), + 'nonzero distinct-register ADD') + reject('boolean_coefficient', lambda s: gate(s).__setitem__(3, True), 'rational coefficient') + reject('wrong_frame', lambda s: s['programs']['forward'][event].__setitem__(2, 1), + 'ADD frame chronology') + return tests + + +def result(raw): + need(hashlib.sha256(raw).hexdigest() == SOURCE_SHA, 'source bytes') + src = json.loads(gzip.decompress(raw)) + need(set(src['programs']) == {'forward', 'backward'}, 'two source orientations') + return {'schema_version': 1, 'claim': 'gatewise_frame_additivity_no_new_kappa', + 'source': SOURCE, 'source_sha256': SOURCE_SHA, + 'orientations': {o: census(src, o) for o in ('forward', 'backward')}, + 'mathematical_checks': mathematical_checks(), 'rejection_controls': controls(src)} + + +def main(): + ap = argparse.ArgumentParser(description=__doc__) + ap.add_argument('--write-result', type=Path) + args = ap.parse_args() + raw = (ROOT / SOURCE).read_bytes(); actual = result(raw) + vendor = json.loads((HERE / 'VENDORED.json').read_text())['files'][0] + context = (HERE / vendor['path']).read_bytes() + need(hashlib.sha256(context).hexdigest() == vendor['sha256'], 'predecessor context bytes') + blob = hashlib.sha1(b'blob ' + str(len(context)).encode() + b'\0' + context).hexdigest() + need(blob == vendor['source_blob'], 'predecessor context Git blob') + actual['predecessor_context'] = vendor + certificate = {} + for orientation, data in actual['orientations'].items(): + certificate[orientation] = {'witnesses': data.pop('witnesses')} + for key in ('forest_event_ids', 'chord_event_ids'): + certificate[orientation][key] = data['paid_graph'].pop(key) + payload = (json.dumps(certificate, sort_keys=True, separators=(',', ':')) + '\n').encode() + actual['certificate'] = {'path': 'CERTIFICATE.json.gz', + 'canonical_payload_sha256': hashlib.sha256(payload).hexdigest()} + try: + result(raw + b'changed') + except Rejected as e: + need(str(e) == 'source bytes', 'source-byte rejection reason') + else: + raise Rejected('changed source accepted') + if args.write_result: + with args.write_result.with_name('CERTIFICATE.json.gz').open('xb') as stream: + stream.write(gzip.compress(payload, mtime=0)) + with args.write_result.open('x') as stream: + json.dump(actual, stream, indent=2, sort_keys=True); stream.write('\n') + else: + need(gzip.decompress((HERE / 'CERTIFICATE.json.gz').read_bytes()) == payload, + 'canonical certificate payload equality') + expected = json.loads((HERE / 'RESULT.json').read_text()) + need(json.loads(json.dumps(actual)) == expected, 'committed result equality') + print('PASS_COHERENT_FRAME_ADDITIVITY frames_per_orientation=1002 ' + 'paid_cycle_rank=2297 controls=5 no_new_kappa') + + +if __name__ == '__main__': + main()