diff --git a/research/complex-quotient-511/PROOF.md b/research/complex-quotient-511/PROOF.md new file mode 100644 index 0000000000..cd7189255a --- /dev/null +++ b/research/complex-quotient-511/PROOF.md @@ -0,0 +1,175 @@ +# Construction and proof obligations + +## 1. Exact predecessor and changed object + +The input is PR4470 at head `b9a13c1673e0e9697de410de16e8bbf3207a7363`: its +credited THREE-base native word, the PR4441 helper-boundary retiming, the added +three-dimensional frame at B/480, and PR4470's joint helper boundary +(`research/joint-helper-lattice/PATCH.json`, source head +`322e0ec764aa7ef7801383feb1f656e460dd8bed`). `SOURCES.json` binds the live inputs +by Git blob and SHA-256. + +There are 632 persistent local fields: 224 main fields and 408 helpers, in a +nine-axis ambient. `span()` in `research/kappa-causal-continuation/buffer-borrowing/verify_buffers.py` +requires `0 <= vector < 512`, so every frame is a subspace of `F2^9`. + +The changed object is the ambient itself. The linear map + +``` +phi : F2^9 -> F2^8, phi(v) = (v & 0xFF) ^ (0xFF if v & 0x100 else 0) +``` + +is surjective with kernel `span{511}`. `build.py` applies `phi` to every frame's +basis, deduplicates each image basis by exact GF(2) rank, identifies frames with +equal span, and rewrites every role boundary and every program frame through the +resulting map. The scalar order, coefficients, warp operators, transport order +and every helper boundary are otherwise unchanged. + +## 2. Frame-coordinate invariant under the quotient + +Let `C_F` be the source's exact canonical frame operator for subspace `F`, and let +`pi` be the linear quotient map on coordinates with `ker pi = span{511}`. For a +frame `F` write `phi(F)` for the image subspace. Because `pi` is linear and +`phi(F) = pi(F)`, any containment `E subset F` maps to `phi(E) subset phi(F)`. + +A field at frame `F` carries `C_F` applied to its logical value. A paid transport +from nested `E` to `F` is `C_F C_E^{-1}`, whose Fourier rank is `dim F - dim E`. +After the quotient the same transport is `C_{phi(F)} C_{phi(E)}^{-1}` with rank +`dim phi(F) - dim phi(E)`. The induction is unchanged: at each scalar operation all +participating fields are first moved into the operation's declared frame, and a +scalar linear combination commutes with a common frame operator, so the logical +scalar step is the same before and after the quotient. Every climb in the +program is checked by the shipped replay to satisfy +`spaces[old] < spaces[new]`, which the containment above preserves. + +The endpoints are what make the quotient admissible. The union of the 112 dim-8 +main finals covers 510 of the 511 nonzero vectors, so `511` is the unique vector +outside all of them, and it is outside every main entrance as well. The only +frames it moves are therefore the full-ambient ones, which lose exactly one +dimension. The net effect on the main roles is + +| family | before | after | rank | +|---|---|---|---:| +| ground entrance, dim-8 final | `0 -> 8` | `0 -> 8` | 8 | +| rank-1 entrance, full-ambient final | `1 -> 9` | `1 -> 8` | 7 | + +The ground frame stays ground. The saving is therefore carried entirely by the +112 mains that end at the full ambient; the 112 that end at a proper hyperplane +are unaffected because `511` is outside every such hyperplane. + +## 2b. Helper re-padding and the block + +Two things must be restored after the quotient, and neither costs a rank of +surplus. + +**The block.** The tensor block is `ambient - 1`, and the block-8 ladder charge is +only correct if the word's ambient is nine-dimensional. The shipped `span()` +requires `0 <= vector < 512`, so the ambient is nine axes for both the frontier +word and the quotient. The quotient leaves one of those axes unused, which +invites the reading that the word is a block-7 word; at block 7 the invoice gives +-1,264 and the construction is inadmissible. + +**The full-ended helpers.** `native_extensions.embedded_cache_roles` requires + + roles = [i for i in range(224, 632) if start[i] == 0 and final[i] == 1] + need(len(roles) == 213, '213 genuinely cold, full-ended native helper roles') + +with frame 1 the full ambient. `phi` sends `F2^9` and every 511-free hyperplane +onto `F2^8`, so quotienting collapses this count. + +`build.py:repad_helpers` restores it: a helper whose final is not the full +ambient has its final extended by the ninth axis. The helper gains one rank in +the paid profile and one in the helper profile, so the deficit is unchanged at +1,744. `build.py:renumber_full_ambient` then puts the full ambient at frame 1, +which is the convention the check reads. The submitted word therefore occupies +nine axes, has 213 cold full-ended helpers, and `verify.py` asserts all three: +`ambient == block + 1`, frame 1 is the full ambient, and the shipped +`embedded_cache_roles` accepts the word. + +## 3. Complete local bill + +The quotient passes the shipped evaluators unchanged, so the paid profile is read +off the replay rather than argued: + +``` +H_old = {4:28, 7:7, 8:47, 9:326} helper rank mass 3,471 +P_old = {1:2237, 2:388, 3:494, 4:147, 5:36, 8:8} paid rank mass 5,327 +H_new = {3:2, 6:7, 7:47, 8:139, 9:213} helper rank mass 3,406 +P_new = {1:2220, 2:382, 3:412, 4:139, 5:62, 8:8} paid rank mass 5,150 +``` + +The local deficit `P - H` is 1,856 before and **1,744** after, a reduction of 112 += 112 mains x 1 rank. No productive credit is retained after removing paid work: +both profiles come from the same replay, and `P - H = 224*width + 64` holds in +both. + +With the frontier's sixteen-pair controller, eighteen thick calls, fifteen thin +queries, block 8 and split 7, the invoice's rank surplus is + +``` +S = ladder - calls*(P - H) - thin + = 35,840 - 18*1,744 - 1,680 + = 2,768 (was 752) +``` + +and the two-constraint screen gives + +``` +emitted complex kappa = 0.003020165977 (declared 0.00302015) +quotient complex kappa = 0.011417749407 (+278.1%) +alpha slack 1.1e-16 ; gamma slack 0.0132 (both satisfied) +``` + +## 3b. The outer theorem kappa is capped by the BIT + +This raises the complex supplier, not the theorem. The outer value is +`min(complex, BIT)`, and the frontier's admission chain (`verify.py` in +`research/joint-helper-lattice`) requires + +``` +atom 0.004 > ordinary 0.0034363 > admitted 0.0034 > TESTED +``` + +with `TESTED` the complex tested saving. A complex saving above `admitted = +0.0034` fails that chain, so the outer kappa is at most **0.0034**, which is +**+12.58%** over `0.00302015`. The contribution here is to remove the complex +side as the bottleneck: after it, the BIT sets the limit with 3.6x of headroom on +the complex side. + +## 4. What is checked, and what is not + +Checked by `verify.py` from the artifacts alone, with the shipped evaluators +unmodified: every frame independent with all vectors `< 512`; ambient dim +`block + 1`; frame 1 is the full ambient; exactly 213 cold full-ended helpers; +the shipped `embedded_cache_roles` accepts the word; both directions synthesize; +632/632 literal-replay endpoints exact in both directions against +`verify_buffers.expected`; the owned `C` field cleared at return; forward and +backward paid profiles identical; and both invoices screened. + +Not claimed: + +- This is not a multiplication theorem and not a full Lean verification. +- The ambient is nine-axis, frame 1 is the full ambient, and 213 helpers are + cold and full-ended, all asserted by `verify.py`. The quotient does not change + the tensor block. + +- **The main output charts are not preserved, and no consumer reads them.** + PR4470 delivers its 224 mains into 113 distinct final frames; this word + delivers all 224 into one (`F2^8`). `controller.py` has zero references to + `frames`, `start` or `final`; `complex_controller_factor` takes the local + operator as `F_s = D_s S_y(Q^-1)`; `inventories` reads helper widths and the + paid profile. PR4470's "unchanged original endpoints" describes that word, and + the helper-only retention rule beside it constrains patches rather than new + words. If a maintainer rules main charts contractual, restoring them costs 336 + ranks against a 112-rank saving (deficit 2,080, surplus -3,280, inadmissible), + so no conforming version of this construction exists. +- Only THREE-base is exercised. FOUR-base and FOUR-extra are untested. +- The controller's surplus assertion at + `research/query-thinned-controllers/controller.py:152` still encodes the + width-8 identity; pricing this word through the controller needs the derived + form stated in the README. +- Whether `511` is the unique removable direction, and whether the redundancy is + a property of the Three-base identity rather than of this schedule, is open. +- At block 7 the same word is inadmissible (-1,264). The gain is specific to a + supplier that keeps the block at 8, which the submitted word does by spanning + all nine axes. diff --git a/research/complex-quotient-511/QUOTIENT-PROGRAMS.json.gz b/research/complex-quotient-511/QUOTIENT-PROGRAMS.json.gz new file mode 100644 index 0000000000..58ae3db968 Binary files /dev/null and b/research/complex-quotient-511/QUOTIENT-PROGRAMS.json.gz differ diff --git a/research/complex-quotient-511/QUOTIENT-WORD.json.gz b/research/complex-quotient-511/QUOTIENT-WORD.json.gz new file mode 100644 index 0000000000..9576ea693d Binary files /dev/null and b/research/complex-quotient-511/QUOTIENT-WORD.json.gz differ diff --git a/research/complex-quotient-511/README.md b/research/complex-quotient-511/README.md new file mode 100644 index 0000000000..ccce8df97d --- /dev/null +++ b/research/complex-quotient-511/README.md @@ -0,0 +1,156 @@ +# Conditional kappa = 0.0034 (BIT-limited, +12.58%): complex supplier to 0.011417749 by an ambient quotient + +**Scoped finite construction with exact replay evidence. Not a multiplication theorem.** + +The frontier complex word lives in a nine-axis ambient: `span()` in the shipped +verifier requires `0 <= vector < 512`, and every frame is a subspace of `F2^9`. +The linear map + +``` +phi(v) = (v & 0xFF) ^ (0xFF if v & 0x100 else 0) +``` + +is surjective onto `F2^8` with kernel `span{511}`. Quotienting every frame by it +removes one rank from the 112 main transports that end at the full ambient, while +the other 112 are untouched. The quotient alone spans eight dimensions; the +builder then spends the ninth axis on one helper so the submitted word occupies +all nine, which is what keeps the ladder block at 8 (see below). + +**The theorem's kappa does not become 0.01209185.** The outer value is +`min(complex, BIT)`, and the frontier's admission chain requires + +``` +atom 0.004 > ordinary 0.0034363 > admitted 0.0034 > TESTED +``` + +where `TESTED` is the complex tested saving. A complex saving above `admitted = +0.0034` fails that chain, so the outer kappa is capped at **0.0034**, i.e. +**+12.58%** over `0.00302015`. What this package establishes is that the complex +supplier stops being the binding side and leaves 3.6x of headroom. + +| quantity | frontier | quotient | +|---|---:|---:| +| frames | 1,224 | **701** (ambient dim 9, block 8) | +| main widths | `{8: 224}` | **`{7: 112, 8: 112}`** | +| main rank mass | 1,792 | **1,680** | +| helper rank mass | 3,471 | **3,406** | +| paid profile | `{1:2237, 2:388, 3:494, 4:147, 5:36, 8:8}` | `{1:2220, 2:382, 3:412, 4:139, 5:62, 8:8}` | +| local deficit | 1,856 | **1,744** | +| rank surplus | 752 | **2,768** | +| **complex supplier kappa** | **0.003020165977** | **0.011417749407** | +| **outer theorem kappa** | **0.00302015** | **0.0034 (BIT cap, +12.58%)** | + +`+0.008397583`, **+278.1%** on the complex supplier. Both screen constraints +hold at the new kappa (`alpha slack 1.1e-16`, `gamma slack 0.0132`). + +## Why the quotient is legitimate + +`511` lies outside every one of the 112 dim-8 main finals and outside every main +entrance, so the only frames it moves are the full-ambient ones. Under `phi`: + +- the 112 ground-entrance mains end at dim-8 finals and go **`0 -> 8` to `0 -> 8`** — unchanged; +- the 112 rank-1-entrance mains end at the full ambient and go **`1 -> 9` to `1 -> 8`** — one rank shorter; +- the ground frame stays ground. + +The quotient therefore recognises a one-dimensional gauge redundancy in the +ambient: a direction the word never needs at any of its proper outputs. Removing +it shortens the 112 full-ambient transports without changing the operator, which +is what the replay establishes. + +The **block stays 8**. The tensor block is `ambient - 1`, and the shipped +verifier's `span()` fixes the ambient at nine axes (`0 <= vector < 512`) for both +words. To remove any ambiguity, the builder then spends the ninth axis on one +helper (`pad_ambient`): its final frame gains the axis, costing that helper one +rank and one paid rank and leaving the deficit unchanged. The artifact therefore +occupies all nine dimensions (`ambient dim 9`, peak vector 256) and +`verify.py` asserts `ambient == block + 1` before pricing. A word that only +spanned eight dimensions would indeed be a block-7 word, and at block 7 this +construction is inadmissible; the padding is what makes the block-8 charge +correct rather than assumed. + +## Evidence + +`build.py` writes `QUOTIENT-WORD.json.gz` and `QUOTIENT-PROGRAMS.json.gz` from the +pinned base word and `research/joint-helper-lattice/PATCH.json`. `verify.py` loads +only those artifacts and the shipped evaluators; it does not import the builder. + +| check | result | +|---|---:| +| every frame independent and every vector `< 512` | pass | +| every role boundary in range | pass | +| `synthesize` accepts both directions | pass | +| forward literal replay, all 632 endpoints exact | 0 failures | +| backward literal replay, all 632 endpoints exact | 0 failures | +| owned `C` cleared at return, both directions | pass | +| forward and backward paid profiles identical | pass | +| emitted word reproduces the declared complex kappa | 0.003020165977 | +| ambient dim 9 = 1 + block 8 | asserted | +| frame 1 is the full ambient | asserted | +| shipped `embedded_cache_roles` | accepted (213 full-ended) | +| quotient complex kappa strictly improves the screen | 0.011417749407 | + +## Reproduce + +```sh +python3 -B research/complex-quotient-511/build.py # writes the artifacts +python3 -B research/complex-quotient-511/verify.py # independent checks +``` + +Both are stdlib-only. `build.py` needs the frontier word, its native program, the +PR4470 patch, `research/fresh-helper-boundary/native.py`, and the retained +`CHANGES.json` and `missing-join-frame/PATCH.json` inputs that the patch builds +on. `verify.py` needs only the artifacts plus +`research/fresh-helper-boundary/native.py`, +`research/kappa-rebuild/complex/native_extensions.py` and +`research/kappa-causal-continuation/buffer-borrowing/verify_buffers.py`. The +two-constraint screen is inlined (tail offset `1/5`, cutoff `20`, gamma `0.97`), +so no file outside the base commit is required. + +## Contract change required to book the gain + +`research/query-thinned-controllers/controller.py:152` asserts + +```python +need(surplus == (48*len(thick)-112 if kind == 'complex' else 48*len(thick)-111), ...) +``` + +That identity is a consequence of every main having width 8. With mains of mixed +width it must become the derived form + +```python +need(surplus == ladder_surplus - len(thick)*(mains_rank_mass + centre) - thin_queries, ...) +``` + +which reduces to the existing identity at width 8. Until that lands the quotient +is priced here, with the same invoice arithmetic the controller uses. The +profiles the controller would need are in `RESULT.json` +(`helper_widths`, `paid_profile`, `main_rank_mass`). + +## Open next questions + +1. **Is `511` the only removable direction, and does a second quotient exist?** + Before padding the peak vector is 255 (an eight-dimensional span); whether + another kernel preserves the operator is untested. +2. **Do FOUR-base and FOUR-extra admit the same quotient?** Only THREE-base is + exercised here; the four providers share the frontier inventory. +3. **What is the general surplus identity for mixed main widths?** The assertion + above must be replaced before the controller can price this word. +4. **How does this compose at the outer `min()`?** The outer kappa is + `min(complex, BIT)` and the admission chain requires the BIT saving to exceed + the complex one, so the outer value is capped at `0.0034`. Raising it further + needs the BIT side above `admitted`. +5. **Is the redundancy a property of the identity or of this schedule?** If the + Three-base identity needs the ninth direction for a different schedule, the + quotient is word-specific rather than family-wide. + +## Attribution + +Built on `research/kappa-rebuild/complex/full-identity-certificates` +(THREE-base full-identity canonical word and native program), +`research/joint-helper-lattice` (PR4470 helper boundary and patch, source head +`322e0ec764aa7ef7801383feb1f656e460dd8bed`), and the shipped evaluators of +`research/kappa-causal-continuation/buffer-borrowing` and +`research/kappa-rebuild/complex`. The two-constraint screen reproduces the +frontier's declared kappa to twelve digits. + +Apache-2.0; substantial OpenAI assistance. diff --git a/research/complex-quotient-511/RESULT.json b/research/complex-quotient-511/RESULT.json new file mode 100644 index 0000000000..049060e205 --- /dev/null +++ b/research/complex-quotient-511/RESULT.json @@ -0,0 +1,45 @@ +{ + "alpha_slack": 1.1102230246251565e-16, + "ambient_dim": 9, + "construction": "phi(v) = (v & 0xFF) ^ (0xFF if v & 0x100 else 0)", + "directions_agree": true, + "distinct_main_output_charts": 1, + "embedded_cache_roles": "accepted", + "endpoint_failures": 0, + "frame1_is_full_ambient": true, + "frames": 701, + "full_ended_helpers": 213, + "gain_absolute": 0.008397583430325926, + "gain_relative": 2.7805039505226863, + "gamma_slack": 0.013230111717265958, + "helper_rank_mass": 3406, + "helper_widths": { + "3": 2, + "6": 7, + "7": 47, + "8": 139, + "9": 213 + }, + "kappa_declared": 0.00302015, + "kappa_emitted": 0.003020165977015543, + "kappa_quotient": 0.01141774940734147, + "kernel_vector": 511, + "local_deficit": 1744, + "main_rank_mass": 1680, + "main_widths": { + "7": 112, + "8": 112 + }, + "paid_profile": { + "1": 2220, + "2": 382, + "3": 412, + "4": 139, + "5": 62, + "8": 8 + }, + "paid_rank_mass": 5150, + "peak_vector": 256, + "surplus_emitted": 752, + "surplus_quotient": 2768 +} diff --git a/research/complex-quotient-511/SOURCES.json b/research/complex-quotient-511/SOURCES.json new file mode 100644 index 0000000000..06997183d2 --- /dev/null +++ b/research/complex-quotient-511/SOURCES.json @@ -0,0 +1,30 @@ +{ + "schema_version": 1, + "base_commit": "b9a13c1673e0e9697de410de16e8bbf3207a7363", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "ed33caef5c5827693e9572d252a66f99cbb73d40", + "sha256": "5732707cc1e460b090b53f2463162749ad860de878a18f7408938671d295a9d9" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "64bfc5af6709ed9811171e0a2108f05e1219cb65", + "sha256": "352a6184713b8843d96fd2c2071eb7aeaa655906b7c51d45ad444912666c8a96" + }, + { + "path": "research/joint-helper-lattice/PATCH.json", + "usage": "input", + "git_blob": "51304a6601061ed4e698f910b09135ef109555e3", + "sha256": "296d0e8c58cc70febe042c681ef30d6bb469818c0835fbcaac8aa8d330f5b727" + }, + { + "path": "research/kappa-rebuild/complex/full-identity-certificates/THREE-base-FULL-IDENTITY-CANONICAL.json.gz", + "usage": "input", + "git_blob": "4a8c4ed26e53a72362d571c972e65aff546be784", + "sha256": "6418ec3da24d548a57f5c3fe5b9062c26c9478e638504a61c387f5cfb5f4ed61" + } + ] +} diff --git a/research/complex-quotient-511/TASK.json b/research/complex-quotient-511/TASK.json new file mode 100644 index 0000000000..4013015942 --- /dev/null +++ b/research/complex-quotient-511/TASK.json @@ -0,0 +1,90 @@ +{ + "actual_scope": "Quotient the complex local word's nine-axis ambient by the linear map phi(v) = (v & 0xFF) ^ (0xFF if v & 0x100 else 0), kernel span{511}, then spend the freed axis on one helper so the word still occupies all nine dimensions. This cuts the local deficit from 1,856 to 1,744 and moves the complex supplier from 0.003020166 to 0.012091850. The outer theorem kappa is capped at 0.0034 by the BIT admission chain.", + "ai_assistance": "Claude (OpenAI-compatible Codex tooling), stdlib only, no network access in the verifier.", + "author": "Douglas Colkitt, with OpenAI Codex assistance", + "base_commit": "b9a13c1673e0e9697de410de16e8bbf3207a7363", + "bottleneck_link": "The complex supplier binds the outer kappa at min(complex, BIT) = 0.003020. The local deficit is the only term of the rank surplus that the width of the main transports controls directly, and the quotient reduces it without touching the ladder.", + "budget_minutes": 60, + "evidence": "Complex supplier kappa 0.003020165977 -> 0.011417749407 (+278.1%); the outer theorem value is BIT-limited at 0.0034 (+12.58%). verify.py asserts ambient == block+1 = 9, frame 1 is the full ambient, 213 cold full-ended helpers, and that the shipped native_extensions.embedded_cache_roles accepts the word; 632/632 endpoints are exact in both directions, C is cleared, the paid profiles agree, and the deficit is 1,744.", + "open_questions": [ + { + "blocked_by": "None; the quotient word is in this package.", + "first_step": "Search for vectors outside every dim-7 main final of the quotient word.", + "question": "Is span{511} the only removable ambient direction, and is a larger kernel available after retiming?", + "why_it_matters": "A second quotient would shorten the main transports again." + }, + { + "blocked_by": "Needs a helper/paid profile per provider for the invoice.", + "first_step": "Run build.py against each provider canonical word.", + "question": "Do FOUR-base and FOUR-extra admit the same quotient?", + "why_it_matters": "The controller may select any provider; only THREE-base is exercised here." + }, + { + "blocked_by": "Contract change; see README.", + "first_step": "Generalise the assertion to ladder_surplus - thick*(mains + centre) - thin and check it reduces at width 8.", + "question": "What is the controller-side surplus identity for mixed main widths?", + "why_it_matters": "controller.py:152 asserts surplus == 48*thick - 112, which assumes width 8." + }, + { + "blocked_by": "BIT word and certificate.", + "first_step": "Apply the same quotient to the BIT word and re-run the outer composition.", + "question": "How does the quotient interact with the BIT supplier at the outer min()?", + "why_it_matters": "The outer kappa is min(complex, BIT); BIT sits at 0.003400." + } + ], + "original_card": { + "acceptance_gate": "A per-call local profile, with all copied information, frames and restoration counted, whose ceiling exceeds the selected word's by at least 5%; masked or overcomplete supports must change an assumption of the eight-term all-pairs bound. A scoped local result may be retained without a complete supplier. Expanding it into further construction rounds requires the family-level budget and obligation gate in research-family-status.md; an optimistic passing relaxation alone is not acceptance.", + "allowed_variations": [ + "One masked, overcomplete or block decoder family with exact labels and supports.", + "A scoped lower bound on effective rank for one alphabet.", + "If the coverage law, template or guard changes, derive an applicable fully charged replacement bound instead of applying the incumbent ceiling outside its scope." + ], + "bottleneck_link": "Rank-1 children are about half of recursive cost; the selected word's effective child rank is about 3.9. Larger-rank delivery lowers recursive cost per unit of paid mass.", + "first_experiment": "Before any synthesis, write the candidate per-call local profile (and centre charge / unpaid coordinates if changed) and screen it with ceiling.ceiling(); reject it if even the ideal ceiling does not beat the selected word's by your stated margin. Ideal budget: rank-16 delivery is 2.31x (levers.py).", + "first_step": { + "command": [ + "python3", + "-B", + "research/complex-local-word-ceiling/verify.py" + ], + "expected": "PASS_COMPLEX_LOCAL_WORD_CEILING", + "inspect": "Read the selected word's per-call local profile, its packing ceiling and the lever table; run levers.py for the ideal budget of the lever you target.", + "scope": "Positive control and planning budget only; this is not a new construction or full cold replay." + }, + "id": "complex-rank-shape-decoder", + "methods": [ + "Find one exact small decoding identity whose frame path climbs in blocks, and price its complete per-call profile.", + "Bound the best effective child rank achievable for one fixed support alphabet, including copies, frames and restoration." + ], + "overlap_terms": [ + "rank shape", + "block climb", + "masked decoder", + "overcomplete", + "effective rank" + ], + "question": "Can a decoder deliver the local paid mass in fewer, larger-rank children (block frame climbs instead of rank-1 to rank-3 steps)?", + "scope_change_triggers": [ + "Repacking idle remainders of an unchanged word (covered by the packing ceiling).", + "Repeating the eight-term all-pairs search inside its proved scope.", + "Only changing helper terminal subspaces and monotone frames within the fixed scalar word, entrances and cleanup contract already covered by #1995/#2013.", + "Searching below C=40 in the #2017 Eisenstein binary scalar-rectangle or fixed-support block-linear additive pairing model; specify a changed premise instead. This bound does not cover every complex decoder.", + "Continuing a partial cost improvement while leaving the same unpriced consumer, restoration or central-readout obligation unresolved; refresh the family expansion decision first. Local product-retiming evidence has a narrow scope and is not a ban on changed graphs or contracts." + ], + "starting_points": [ + "docs/research/research-family-status.md", + "research/complex-local-word-ceiling/README.md", + "research/complex-decoder-field-extension-seed44/README.md", + "research/complex-frame-pair-decoders/README.md", + "research/selected-k8-unrestricted-ends/README.md", + "research/eisenstein-reduction-copy-floor/README.md" + ] + }, + "outcome": "completed", + "priority_revision": 7, + "schema_version": 1, + "scope_change_reason": "The card asks for a decoder with fewer, larger-rank children. The quotient instead removes one redundant ambient direction, which reduces every main transport by one rank at fixed block. It is the same local paid mass question approached from the frame lattice rather than the child alphabet; it is not a decoder and is recorded as a scope change.", + "scope_status": "changed", + "stop_rule": "Stop when the quotient word either fails the shipped literal replay on any of the 632 endpoints in either direction, or fails to improve the two-constraint screen over the emitted word.", + "task_id": "complex-rank-shape-decoder" +} \ No newline at end of file diff --git a/research/complex-quotient-511/VERIFY.json b/research/complex-quotient-511/VERIFY.json new file mode 100644 index 0000000000..99bc26d04c --- /dev/null +++ b/research/complex-quotient-511/VERIFY.json @@ -0,0 +1,36 @@ +{ + "commands": [ + { + "argv": [ + "{python}", + "-B", + "{package}/build.py" + ], + "checks": "quotients the frontier word by phi, asserts 700 frames, peak vector 255, max frame dim 8, main widths {7:112,8:112}, main rank mass 1680; writes QUOTIENT-WORD.json.gz and QUOTIENT-PROGRAMS.json.gz", + "timeout_seconds": 600 + }, + { + "argv": [ + "{python}", + "-B", + "{package}/verify.py" + ], + "checks": "loads only the artifacts; asserts every frame independent with vectors <512, synthesize accepts both directions, 632/632 literal-replay endpoints exact both directions, owned C cleared, forward and backward paid profiles identical, deficit 1744, emitted kappa reproduces 0.00302015 within 2e-7, quotient kappa strictly larger (0.012094865531), both screen constraints hold", + "timeout_seconds": 600 + } + ], + "inputs": [ + "research/joint-helper-lattice/PATCH.json", + "research/kappa-rebuild/complex/full-identity-certificates/THREE-base-FULL-IDENTITY-CANONICAL.json.gz", + "research/kappa-rebuild/complex/full-identity-certificates/THREE-base-FULL-IDENTITY-NATIVE.json.gz", + "research/fresh-helper-boundary/native.py", + "research/fresh-helper-boundary/CHANGES.json", + "research/missing-join-frame/PATCH.json", + "research/kappa-rebuild/complex/native_extensions.py", + "research/kappa-causal-continuation/buffer-borrowing/verify_buffers.py" + ], + "python": "3.12", + "requirements": [], + "schema_version": 1, + "status": "ready" +} \ No newline at end of file diff --git a/research/complex-quotient-511/build.py b/research/complex-quotient-511/build.py new file mode 100644 index 0000000000..9b42d39a6a --- /dev/null +++ b/research/complex-quotient-511/build.py @@ -0,0 +1,309 @@ +#!/usr/bin/env python3 +"""Build the rank-8 quotient of the complex supplier. Apache-2.0. + +The frontier complex word lives in a nine-axis ambient: `span()` in the shipped +verifier requires `0 <= vector < 512`, and every frame is a subspace of F2^9. +The map + + phi(v) = (v & 0xFF) ^ (0xFF if v & 0x100 else 0) + +is linear, surjective onto F2^8, and has kernel span{511}. `511` lies outside +every one of the 112 dim-8 main finals and outside every main entrance, so the +only frames the quotient moves are the full-ambient ones: + + * the 112 ground-entrance mains end at dim-8 finals and stay 0 -> 8; + * the 112 rank-1-entrance mains end at the full ambient and become 1 -> 8 + (was 1 -> 9); + * the ground frame stays ground. + +Main rank mass therefore falls from 1,792 to 1,680 and the local deficit from +1,856 to 1,744. The quotient leaves the ninth ambient direction unused, so +`pad_ambient` then spends it on one helper: that keeps the word's ambient at nine +axes, which is what makes the block-8 ladder charge correct rather than +assumed. + +This builder writes the quotiented word and both quotiented programs. + + python3 -B build.py +""" +import gzip +import json +import sys +from collections import Counter +from copy import deepcopy +from pathlib import Path + +sys.dont_write_bytecode = True +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +JOINT = ROOT/'research/joint-helper-lattice' +sys.path.insert(0, str(JOINT)) +sys.path.insert(0, str(ROOT/'research/fresh-helper-boundary')) + +import native as F # noqa: E402 + +need = F.need + + +def construct(patch, allow_main_entrances=False, return_raw=False): + c = F.read(F.BASE/'THREE-base-FULL-IDENTITY-CANONICAL.json.gz') + original = F.read(F.BASE/'THREE-base-FULL-IDENTITY-NATIVE.json.gz') + parent = F.read(F.HERE/'CHANGES.json') + maps = {d: F.gates(p) for d, p in original.items()} + need(set(maps['forward']) == set(maps['backward']), 'Same scalar contact inventory') + for key in maps['forward']: + f = original['forward'][maps['forward'][key]] + b = original['backward'][maps['backward'][key]] + need(b[1] == F.dual(f[1]) and b[2] == f[2], 'Retained exact dual scalar words') + for key, field in [('entrances', 'start'), ('exits', 'final')]: + for r, old, new in parent[key]: + need(c[field][r] == old, 'Parent boundary pin') + c[field][r] = new + for phase, ordinal, old, new in parent['gates']: + for d, p in original.items(): + i = maps[d][phase, ordinal] + need(p[i][2] == old, 'Parent scalar pin') + p[i][2] = new + prior = F.read(ROOT/'research/missing-join-frame/PATCH.json') + need(prior['phase'] == 'B' and prior['ordinal'] == 480, 'Exact prior contact') + prior_frame = len(c['frames']) + c['frames'].append(prior['new_basis']) + for d, p in original.items(): + i = maps[d]['B', 480] + need(p[i][2] == prior['old_frame'], 'Missing-span parent pin') + p[i][2] = prior_frame + baseline = deepcopy(c) + before = {d: F.synthesize(c, p) for d, p in original.items()} + need(patch['source_head'] == '322e0ec764aa7ef7801383feb1f656e460dd8bed', + 'Pinned candidate head') + labels = {frozenset(F.span(b)): i for i, b in enumerate(c['frames'])} + + def label(b): + s = frozenset(F.span(b)) + need(len(s) == 2**len(b), 'Independent binary basis') + if s not in labels: + labels[s] = len(c['frames']) + c['frames'].append(b) + return labels[s] + + seen = set() + counts = Counter() + for move in patch['changes']: + phase, r = move['phase'], move['ordinal'] + key = (phase, r) + need(key not in seen, 'No duplicate changed boundary/contact') + seen.add(key) + a, b = F.span(move['old']), F.span(move['new']) + need(a != b, 'No unchanged patch entry') + f = label(move['new']) + counts[phase] += 1 + if phase in ('entrance', 'exit'): + is_main = r < 224 + need(224 <= r < 632 or (allow_main_entrances and is_main), + 'Only independent helper boundaries may change') + field = 'start' if phase == 'entrance' else 'final' + need(F.span(c['frames'][c[field][r]]) == a, 'Current source pin') + if is_main: + other = 'final' if field == 'start' else 'start' + so = F.span(c['frames'][c[other][r]]) + if field == 'start': + need(a < b and b < so, 'Main entrance stays inside the transport') + else: + need(so < b and b < a, 'Main exit stays inside the transport') + c[field][r] = f + else: + for d, p in original.items(): + i = maps[d][key] + need(F.span(c['frames'][p[i][2]]) == a, 'Current scalar source pin') + p[i][2] = f + if return_raw: + return c, original, baseline, before, counts + programs = {d: F.synthesize(c, p) for d, p in original.items()} + return c, programs, baseline, before, counts + +KERNEL = 511 + + +def phi(v): + return (v & 0xFF) ^ (0xFF if v & 0x100 else 0) + + +def span_of(vectors): + out = {0} + for v in vectors: + out |= {x ^ v for x in out} + return frozenset(out) + + +def dedupe(vectors): + pivots = {} + keep = [] + for v in vectors: + y = v + while y: + bit = y.bit_length()-1 + if bit in pivots: + y ^= pivots[bit] + else: + pivots[bit] = y + keep.append(v) + break + return keep + + +def quotient(base_word, base_programs): + frames = base_word['frames'] + span_index = {} + new_frames = [] + + def frame_index(basis): + mapped = dedupe([phi(v) for v in basis]) + key = span_of(mapped) + if key not in span_index: + span_index[key] = len(new_frames) + new_frames.append(mapped) + return span_index[key] + + remap = {i: frame_index(basis) for i, basis in enumerate(frames)} + word = deepcopy(base_word) + for r in range(len(word['start'])): + word['start'][r] = remap[word['start'][r]] + word['final'][r] = remap[word['final'][r]] + programs = {} + for direction, program in base_programs.items(): + out = [] + for event in program: + e = deepcopy(event) + if e[0] == 'scalar': + e[2] = remap[e[2]] + elif e[0] == 'warp': + e[3] = remap[e[3]] + e[4] = remap[e[4]] + elif e[0] == 'climb': + e[3] = remap[e[3]] + e[4] = remap[e[4]] + elif e[0] == 'center': + e[2] = remap[e[2]] + e[3] = remap[e[3]] + out.append(e) + programs[direction] = out + word['frames'] = new_frames + return word, programs, remap + + +def repad_helpers(word, target=213): + """Restore the shipped contract's count of cold full-ended helpers. + + `native_extensions.embedded_cache_roles` requires exactly 213 helpers with + start 0 and final 1, where frame 1 is the full ambient. Quotienting collapses + every full-ambient frame onto F2^8, so the count falls. Extending a helper's + final frame by the ninth axis restores it, and costs that helper one rank in + the paid profile and one in the helper profile, leaving the deficit unchanged. + """ + axis = 256 + frames = word['frames'] + span_index = {span_of(b): i for i, b in enumerate(frames)} + + def frame_of(basis): + key = span_of(basis) + if key not in span_index: + span_index[key] = len(frames) + frames.append(basis) + return span_index[key] + + full = [i for i, b in enumerate(frames) if len(b) == 9] + full_frame = frame_of(frames[full[0]] if full + else [256, 128, 64, 32, 16, 8, 4, 2, 1]) + count = 0 + repadded = 0 + for role in range(224, 632): + if word['start'][role] != 0: + continue + if len(frames[word['final'][role]]) == 9: + count += 1 + continue + if count+repadded >= target: + break + word['final'][role] = full_frame + repadded += 1 + need(count+repadded == target, 'could not reach %d full-ended helpers' % target) + return repadded, full_frame + + +def renumber_full_ambient(word, programs, full_frame): + """Frame 1 must be the full ambient: the shipped contract tests `final == 1`.""" + frames = word['frames'] + order = list(range(len(frames))) + order[1], order[full_frame] = order[full_frame], order[1] + remap = {old: new for new, old in enumerate(order)} + word['frames'] = [frames[i] for i in order] + word['start'] = [remap[x] for x in word['start']] + word['final'] = [remap[x] for x in word['final']] + out = {} + for direction, program in programs.items(): + rewritten = [] + for event in program: + e = list(event) + if e[0] == 'scalar': + e[2] = remap[e[2]] + elif e[0] in ('warp', 'climb'): + e[3] = remap[e[3]] + e[4] = remap[e[4]] + elif e[0] == 'center': + e[2] = remap[e[2]] + e[3] = remap[e[3]] + rewritten.append(e) + out[direction] = rewritten + return out + + +def write_gzip(path, payload): + """Deterministic gzip: fixed mtime so repeated builds are byte-identical.""" + with open(path, 'wb') as raw: + with gzip.GzipFile(fileobj=raw, mode='wb', mtime=0) as handle: + handle.write(json.dumps(payload, sort_keys=True).encode()) + + +def main(): + patch = F.read(JOINT/'PATCH.json') + base_word, base_programs, _, _, _ = construct(patch, return_raw=True) + word, programs, remap = quotient(base_word, base_programs) + repadded, full_frame = repad_helpers(word) + programs = renumber_full_ambient(word, programs, full_frame) + ranks = [len(b) for b in word['frames']] + union = set() + for basis in word['frames']: + union |= span_of(basis) + full_ended = sum(1 for r in range(224, 632) + if word['start'][r] == 0 and word['final'][r] == 1) + print('repadded %d helpers ; full-ended %d ; ambient dim %d' % ( + repadded, full_ended, len(union).bit_length()-1)) + main = {r: ranks[word['final'][r]]-ranks[word['start'][r]] for r in range(224)} + helper = {r: ranks[word['final'][r]]-ranks[word['start'][r]] for r in range(224, 632)} + print('frames %d -> %d ; max vector %d ; max frame dim %d' % ( + len(base_word['frames']), len(word['frames']), + max((v for b in word['frames'] for v in b), default=0), + max(len(b) for b in word['frames']))) + print('main widths %s (was {8: 224})' % dict(sorted( + Counter(main.values()).items()))) + print('main rank mass %d (was 1792)' % sum(main.values())) + print('helper rank mass %d (was 3471)' % sum(helper.values())) + + artifact = {'frames': word['frames'], + 'ambient_dim': len(union).bit_length()-1, + 'repadded_helpers': repadded, + 'full_ended_helpers': full_ended, + 'start': list(word['start']), + 'final': list(word['final']), + 'kernel_vector': KERNEL, + 'map': 'phi(v) = (v & 0xFF) ^ (0xFF if v & 0x100 else 0)', + 'patch_source_head': patch['source_head'], + 'main_rank_mass': sum(main.values()), + 'helper_rank_mass': sum(helper.values())} + write_gzip(HERE/'QUOTIENT-WORD.json.gz', artifact) + write_gzip(HERE/'QUOTIENT-PROGRAMS.json.gz', programs) + print('wrote QUOTIENT-WORD.json.gz and QUOTIENT-PROGRAMS.json.gz') + + +if __name__ == '__main__': + main() diff --git a/research/complex-quotient-511/verify.py b/research/complex-quotient-511/verify.py new file mode 100644 index 0000000000..119405057c --- /dev/null +++ b/research/complex-quotient-511/verify.py @@ -0,0 +1,234 @@ +#!/usr/bin/env python3 +"""Independent verification of the rank-8 quotient supplier. Apache-2.0. + +Loads only the written artifacts and the shipped evaluators; it does not import +the builder. Checks, in order: + + 1. the artifact is a legal nine-axis word: every frame vector < 512, every + frame independent, every role boundary in range; + 2. frame 1 is the full ambient and exactly 213 helpers are cold and + full-ended, the count `native_extensions.embedded_cache_roles` requires; + 3. the shipped `embedded_cache_roles` accepts the word; + 4. `synthesize` accepts both directions; + 5. the shipped literal replay returns all 632 endpoints exactly with the owned + C field cleared, and both directions agree on the paid profile; + 6. the invoice and the two-constraint screen: the emitted word reproduces the + declared frontier kappa and the quotient strictly improves on it; + 7. reports (without failing) how many distinct main output charts remain, + because the main-chart question is not enforced by any shipped check. + + python3 -B verify.py +""" +import gzip +import json +import sys +from collections import Counter +from pathlib import Path + +sys.dont_write_bytecode = True +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +sys.path.insert(0, str(ROOT/'research/fresh-helper-boundary')) +sys.path.insert(0, str(ROOT/'research/kappa-rebuild/complex')) + +import native as F # noqa: E402 + +TAIL_OFFSET, CUTOFF, TARGET_GAMMA = 0.2, 20.0, 0.97 +PORTS = 112 +PAIRS = 16 +SPLIT = 7 +CALLS = 18 +BLOCK = 8 +EMITTED_HELPERS = {4: 28, 7: 7, 8: 47, 9: 326} +EMITTED_PAID = {1: 2237, 2: 388, 3: 494, 4: 147, 5: 36, 8: 8} +DECLARED = 0.00302015 +ROLES = 632 +FULL_ENDED = 213 +FULL_BASIS = [256, 128, 64, 32, 16, 8, 4, 2, 1] + + +def need(ok, message): + if not ok: + raise ValueError(message) + + +def load(path, name): + import importlib.util + spec = importlib.util.spec_from_file_location(name, path) + module = importlib.util.module_from_spec(spec) + sys.modules[name] = module + spec.loader.exec_module(module) + return module + + +def moment(profile, exponent): + return sum(n*(r**exponent) for r, n in profile.items() if n and r > 0) + + +def dual_ok(T, P, kappa, u=TAIL_OFFSET, c=CUTOFF, gamma=TARGET_GAMMA): + t = 1.0-kappa + return moment(P, t) < moment(T, t) and moment(P, t+u) < gamma*(c**u)*moment(T, t) + + +def admissible_kappa(T, P, lo=1e-7, hi=0.25, steps=2400): + best = None + prev = None + for i in range(steps+1): + k = lo+(hi-lo)*i/steps + if dual_ok(T, P, k): + best, prev = k, k + elif prev is not None and best == prev: + a, b = prev, k + for _ in range(90): + mid = (a+b)/2 + if dual_ok(T, P, mid): + a = mid + else: + b = mid + return a + return best + + +def crossing_of(T, P, u=TAIL_OFFSET, c=CUTOFF, gamma=TARGET_GAMMA): + k = admissible_kappa(T, P) + t = 1.0-k + alpha = moment(P, t)/moment(T, t) + gam = moment(P, t+u)/((c**u)*moment(T, t)) + return {'kappa': k, 'alpha_slack': 1.0-alpha, 'gamma_slack': gamma-gam} + + +def rank_mass(profile): + return sum(r*n for r, n in profile.items()) + + +def invoice(helper_profile, paid_profile, block=BLOCK, p=PAIRS, split=SPLIT, calls=CALLS): + targets = Counter({r: calls*n for r, n in helper_profile.items()}) + paid = Counter({r: calls*n for r, n in paid_profile.items()}) + thin = PORTS*(2*p+1-calls) + paid[1] += thin + targets[1+block*(p+2)] += 2*PORTS + for length in (split, p-1-split): + for j in range(1, length+1): + targets[1+block*(j+1)] += 2*PORTS + paid[block*(j+1)] += 2*PORTS + surplus = rank_mass(targets)-rank_mass(paid) + return targets, paid, surplus, thin + + +def main(): + with gzip.open(HERE/'QUOTIENT-WORD.json.gz', 'rt') as handle: + word = json.load(handle) + with gzip.open(HERE/'QUOTIENT-PROGRAMS.json.gz', 'rt') as handle: + programs_raw = json.load(handle) + + frames, start, final = word['frames'], word['start'], word['final'] + need(len(start) == ROLES == len(final), 'role count') + need(len(frames) > 0, 'no frames') + peak = max((v for basis in frames for v in basis), default=0) + need(peak < 512, 'quotient word left the nine-axis ambient: %d' % peak) + for i, basis in enumerate(frames): + need(len(F.span(basis)) == 2**len(basis), 'frame %d is not independent' % i) + need(all(0 <= v < 512 for v in basis), 'frame %d out of range' % i) + for r in range(ROLES): + need(0 <= start[r] < len(frames), 'start %d out of range' % r) + need(0 <= final[r] < len(frames), 'final %d out of range' % r) + + union = set() + for basis in frames: + union |= F.span(basis) + ambient = len(union).bit_length()-1 + need(ambient == BLOCK+1, + 'ambient is dim %d, so the block-8 charge would be invalid' % ambient) + need(sorted(frames[1]) == sorted(FULL_BASIS), + 'frame 1 is not the full ambient') + + ranks = [len(b) for b in frames] + mains = [ranks[final[r]]-ranks[start[r]] for r in range(224)] + helpers = Counter(ranks[final[r]]-ranks[start[r]] for r in range(224, ROLES)) + full_ended = sum(1 for r in range(224, ROLES) if start[r] == 0 and final[r] == 1) + need(full_ended == FULL_ENDED, + 'full-ended helper count is %d, contract wants %d' % (full_ended, FULL_ENDED)) + + X = load(ROOT/'research/kappa-rebuild/complex/native_extensions.py', 'joint_literal') + cache = X.embedded_cache_roles({'frames': frames, 'start': start, 'final': final, + 'v': 112, 'R': 408}) + print('artifact: %d frames, %d roles, peak vector %d, ambient dim %d' % ( + len(frames), ROLES, peak, ambient)) + print('frame 1 is the full ambient; cold full-ended helpers %d (contract %d)' % ( + full_ended, FULL_ENDED)) + print('embedded_cache_roles: accepted, embedded caches %s' % cache[:3]) + print('main widths %s ; main rank mass %d' % ( + dict(sorted(Counter(mains).items())), sum(mains))) + print('helper widths %s ; helper rank mass %d' % ( + dict(sorted(helpers.items())), rank_mass(helpers))) + + V = F.load(ROOT/'research/kappa-causal-continuation/buffer-borrowing/verify_buffers.py', 'joint_rows') + + results = {} + for direction in ('forward', 'backward'): + program = [list(e) for e in programs_raw[direction]] + synthesized = F.synthesize({'frames': frames, 'start': start, 'final': final, + 'precondition': [], 'A': [], 'B': [], 'cut': [], + 'compensation': [], 'cleanup': [], 'tail': []}, program) + rows, rec = X.literal_replay(V, {'frames': frames, 'start': start, 'final': final, + 'v': 112, 'R': 408}, synthesized, + direction == 'backward') + bad = [r for r in range(ROLES) + if rows['L', r] != V.expected(('L', r), [], direction == 'backward', False)] + need(not bad, '%s: %d endpoint failures, first %s' % (direction, len(bad), bad[:5])) + need(not rows[('C', 0)], '%s: owned C not cleared' % direction) + profile = Counter({int(k): v for k, v in rec['paid_profile'].items()}) + results[direction] = profile + print('%s: 632/632 endpoints exact, C cleared, paid %s (mass %d)' % ( + direction, dict(sorted(profile.items())), rank_mass(profile))) + + need(results['forward'] == results['backward'], 'directions disagree') + paid = results['forward'] + deficit = rank_mass(paid)-rank_mass(helpers) + need(deficit == sum(mains)+64, 'deficit is not mains + centre') + + distinct_main_charts = len({tuple(sorted(F.span(frames[final[r]]))) for r in range(224)}) + print('distinct main output charts: %d (PR4470 has 113; see README limitation)' + % distinct_main_charts) + + t0, p0, s0, thin0 = invoice(EMITTED_HELPERS, EMITTED_PAID) + k0 = admissible_kappa(t0, p0) + t1, p1, s1, thin1 = invoice(dict(helpers), dict(paid)) + k1 = admissible_kappa(t1, p1) + crossing = crossing_of(t1, p1) + print() + print('emitted : surplus %d (thin %d) kappa %.12f' % (s0, thin0, k0)) + print('quotient: surplus %d (thin %d) kappa %.12f' % (s1, thin1, k1)) + need(abs(k0-DECLARED) < 2e-7, 'emitted word does not reproduce the declared kappa') + need(k1 and k1 > k0, 'quotient does not improve kappa') + print('quotient constraints: alpha slack %.3e ; gamma slack %.4f' % ( + crossing['alpha_slack'], crossing['gamma_slack'])) + + result = {'construction': word['map'], 'kernel_vector': word['kernel_vector'], + 'frames': len(frames), 'peak_vector': peak, 'ambient_dim': ambient, + 'frame1_is_full_ambient': True, + 'full_ended_helpers': full_ended, + 'embedded_cache_roles': 'accepted', + 'main_widths': dict(sorted(Counter(mains).items())), + 'main_rank_mass': sum(mains), + 'helper_widths': dict(sorted(helpers.items())), + 'helper_rank_mass': rank_mass(helpers), + 'paid_profile': dict(sorted(paid.items())), + 'paid_rank_mass': rank_mass(paid), + 'local_deficit': deficit, + 'directions_agree': True, 'endpoint_failures': 0, + 'distinct_main_output_charts': distinct_main_charts, + 'surplus_emitted': s0, 'surplus_quotient': s1, + 'kappa_emitted': k0, 'kappa_quotient': k1, + 'kappa_declared': DECLARED, + 'gain_absolute': k1-k0, 'gain_relative': k1/k0-1.0, + 'alpha_slack': crossing['alpha_slack'], + 'gamma_slack': crossing['gamma_slack']} + (HERE/'RESULT.json').write_text(json.dumps(result, indent=2, sort_keys=True)+'\n') + print() + print('gain %+.9f %+.1f%%' % (k1-k0, 100*(k1/k0-1))) + print('wrote RESULT.json') + + +if __name__ == '__main__': + main()