From e20ea62d4be79609802279950b062abb9097624f Mon Sep 17 00:00:00 2001 From: Ali Romman <226877337+aliromman@users.noreply.github.com> Date: Sun, 25 Oct 2026 01:52:24 -0500 Subject: [PATCH 1/2] Bound exact numerator width in the retained two-full caller --- .../two-full-exact-width-gate/OVERLAP.json | 71 ++ research/two-full-exact-width-gate/PROOF.md | 209 ++++ research/two-full-exact-width-gate/README.md | 108 ++ .../two-full-exact-width-gate/RESULT.json | 959 ++++++++++++++++++ .../two-full-exact-width-gate/SOURCES.json | 60 ++ research/two-full-exact-width-gate/TASK.json | 96 ++ .../two-full-exact-width-gate/VERIFY.json | 30 + .../WITNESSES.json.gz | Bin 0 -> 65448 bytes .../test_mutations.py | 65 ++ research/two-full-exact-width-gate/verify.py | 305 ++++++ 10 files changed, 1903 insertions(+) create mode 100644 research/two-full-exact-width-gate/OVERLAP.json create mode 100644 research/two-full-exact-width-gate/PROOF.md create mode 100644 research/two-full-exact-width-gate/README.md create mode 100644 research/two-full-exact-width-gate/RESULT.json create mode 100644 research/two-full-exact-width-gate/SOURCES.json create mode 100644 research/two-full-exact-width-gate/TASK.json create mode 100644 research/two-full-exact-width-gate/VERIFY.json create mode 100644 research/two-full-exact-width-gate/WITNESSES.json.gz create mode 100644 research/two-full-exact-width-gate/test_mutations.py create mode 100644 research/two-full-exact-width-gate/verify.py diff --git a/research/two-full-exact-width-gate/OVERLAP.json b/research/two-full-exact-width-gate/OVERLAP.json new file mode 100644 index 0000000000..f403569c61 --- /dev/null +++ b/research/two-full-exact-width-gate/OVERLAP.json @@ -0,0 +1,71 @@ +{ + "schema_version": 1, + "publication_base": "32890bc5de034ab8fc93ac88ead7279a6a416d04", + "coordination": "Assigned continuation of the released exact-execution source scope. The coordinator handles external posts and final publication checks.", + "cache_coverage": { + "fetched_through": "2026-10-25T06:43:44Z", + "open_prs": 383, + "closed_prs": 4682, + "discussion_records": 4804, + "complete_pagination": true + }, + "later_coordinator_checks": "The coordinator fetched canonical main at 2026-10-25 06:39 UTC. Main, selection and guidance remain at the publication base. The complete overlap refresh and a focused reading of the four new related PR bodies found no duplicate of this fixed-cut two-band tariff.", + "distinct_scopes": [ + { + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/4966", + "relationship": "Source caller, moving-frame checker and independent-error precision tariff. This package changes the premise to ideal exact operators and independent input amplitudes." + }, + { + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/4983", + "relationship": "Additivity required by unchanged scalar gates, not a two-band integer width census." + }, + { + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/5106", + "relationship": "Coherent rank-gauge countermodel, not exact input-width charging." + }, + { + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/5444", + "relationship": "Rounded inverse fibers, relative output precision and repeated history, not literal source-cut numerator width." + }, + { + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/3854", + "relationship": "Integer upper inequalities for a Gaussian interval routine, not this lower width gate." + }, + { + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/5450", + "relationship": "Coordinator checked the standalone bit-flip paid-return span threshold; different input and cost model." + }, + { + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/5454", + "relationship": "Coordinator checked cube-zero multiplication outer-product cost with free GL2; different representation and tariff." + }, + { + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/5492", + "relationship": "Actual fixed-grid reversible-lifting frame-cycle defect. This tests a rounded operator interface, not exact independent input-band width." + }, + { + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/5479", + "relationship": "Uniform conditioning for the production-scale untruncated Gaussian cell. This does not count the retained caller register ranges." + }, + { + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/5500", + "relationship": "Rounded old-H Schur elimination and source LU factor growth. This uses a different source and boundary model." + }, + { + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/5518", + "relationship": "Authentication of native scientific-product commitments. This is a verifier-normalization audit, not a width theorem." + } + ], + "historical_local_evidence": { + "path": "work/exact-coefficient", + "status": "Preserved unchanged in the originating worktree; not a runtime dependency of this package.", + "sha256": { + "EXACT-LATTICE.md": "174f8d996cccff7425d26f60592c96754bab7da6d22c4d5fae3eb4ecff6a0d3d", + "exact_lattice.py": "25ff2e768fde4c2c9c827a215a51f45c76e541ea2eb0399698796ca90bff12fb", + "exact_lattice.json": "e5e25dfe2523898e45d29d8e8cf89f07c91c1e91276f088fe52969cebdf7a329", + "invariant_screen.py": "623ea96fb548aafb25b5dda7c2c975957b87081470cffa9e8d420f682fa47139", + "invariant_screen.json": "b16ba37b7e2b4ad045559ba28a46a052b0165b3245f99be07902c9cdca4127c0" + } + }, + "limits": "No match is not a worldwide novelty proof. This is a source-specific application of classical valuation and counting." +} diff --git a/research/two-full-exact-width-gate/PROOF.md b/research/two-full-exact-width-gate/PROOF.md new file mode 100644 index 0000000000..59e9498b32 --- /dev/null +++ b/research/two-full-exact-width-gate/PROOF.md @@ -0,0 +1,209 @@ +# An exact width gate for one two-FULL caller + +This is a source-specific negative result. It concerns a literal exact integer +representation and a uniform width tariff. It does not exclude every exact +implementation, every BIT controller, or the two-FULL idea itself. It gives no +new kappa. + +## Declared model + +Use the retained round-three source at base +`32890bc5de034ab8fc93ac88ead7279a6a416d04`. Its decompressed payload SHA256 is +`cfcd36b40326d7a5815e1db5313444379b3fb756b27d5201c561574c085cc0dd`. +The two calls use the forward and backward source orientations. Each call keeps +all 632 persistent roles, 408 independent helper inputs and outputs, and the +single reused owned center C0. Each orientation has 3,298 paid occurrences. +The two helper banks are distinct. + +The caller is read from right to left: + +```text +S_e D2 U(Q) D1 L(-Q^-1) B S_e^-1, +B = [[1,-1],[1,0]], S_e = diag(1,e), e = 2^-k. +``` + +Q is the common one-axis Gaussian. D1 and D2 act on separate fresh eight-axis +blocks. The operators and the retained boundary maps are ideal and exact. +The source charts and the declared target invoice are inherited from +[PR #4966](https://github.com/CrocSwap/integer-mult-bounds/pull/4966). +No independent operator errors are introduced. + +The width policy has four premises: + +1. At each paid occurrence, store the full exact register value as integer + numerators. A fixed denominator or one shared exponent is permitted. +2. Choose that occurrence's width before the data is known. It must hold for + every permitted input at that occurrence. Different occurrences can have + different widths. +3. The raw invoice funds leading width `k+o(k)` at each occurrence. The leading + recursive charge is linear in this width. +4. Take `k -> infinity` at fixed native rank and fixed fiber/column + multiplicity f. A separately funded width comparable with k is outside + this comparison. + +The multiplicity f is fixed as well as the rank. A tensor frame can add a +denominator-width offset of order f. Thus this proof does not infer the same +leading charge when f grows with k. No growing-multiplicity limit is claimed. + +These are cost-model premises, not conclusions about every arithmetic method. +In particular, the sum below is a sum of uniform site charges. A separate +worst-case witness for each site does not prove the same sum for an adaptive +per-input width policy. + +## The two-band lemma + +Let p and q be fixed, nonzero dyadic rational numbers. Let + +```text +c = max(0, v2(p) - v2(q)). +z(A,B) = p A / 2^k + q B, +0 <= A < 2^(k-c), 0 <= B < 2^k, k > c. +``` + +There are exactly `2^(2k-c)` distinct values z. For if two values are equal, + +```text +p (A-A') = -2^k q (B-B'). +``` + +If `B=B'`, then `A=A'`. Otherwise the 2-adic valuation gives +`v2(A-A') >= k + v2(q) - v2(p) >= k-c`. Thus `A-A'` is a multiple of +`2^(k-c)`. Its absolute value is smaller than this number. It is zero, and +then `B-B'` is zero. This proves injectivity for every integer `k>c`. + +Any injective exact encoding of this scalar range needs at least `2k-c` +information bits. This is a classical counting argument applied to the two +independent source amplitudes. It is not a new general information theorem. + +For literal integer numerators, a shared exponent cannot remove the leading +width. Write `p=2^a u` and `q=2^b v`, where u and v are odd integers. Take +`A=1` and `B=2^(k-1)`. For all sufficiently large k, + +```text +z = 2^(a-k) [u + v 2^(2k-1+b-a)]. +``` + +The quantity in brackets is an odd integer. Its bit length is `2k-O(1)`: +the nonzero second term has this bit length and the first term is fixed. +For `k>a`, the displayed numerator is already reduced. Any other integer +numerator for the same dyadic value, with a power-of-two denominator, is at +least as wide. A common exponent for more than one component can add zeros; +it cannot shorten this reduced numerator. Thus a uniform literal numerator +width at this site is at least `2k-O(1)`. + +Multiplication by a fixed nonzero Gaussian dyadic vector preserves the number +of distinct values. At least one real or imaginary component is a fixed +nonzero dyadic multiple of z, so the same leading numerator bound holds there. +At fixed multiplicity, boundary denominators change only the constant term. They are not +set to zero or granted for free. + +## Binding the lemma to the source + +The live dependency +`research/two-full-border-paid-precision/independent-review/invariance/check_invariance.py` +checks every one of the 42,898 source events. It checks all common-frame scalar +contacts, paid frame changes, warp incidences, final frames, owned-center +rules, and boundary markers. It verifies all 72 binary warp matrices and all +four signed/oriented zero-address phases. + +Under its inherited exact moving-frame semantics, a paid transition changes +the physical frame and leaves the logical value unchanged. Each logical warp +has a homogeneous binary address map and a quadratic phase with no constant +term. It fixes `delta_0` with phase one. The `phase` records are section labels. +Boundary adapters change the physical reference, not the logical value. +The audit retains the 82 early, identity X-exit markers per orientation. It +does not silently assume that these markers occur in their final frame. + +It follows by induction that logical multiples of `delta_0` follow the exact +rational scalar program. This is a logical-frame invariant. It does not say +that every physical map fixes physical `delta_0`. The inherited interpretation +of the primitives as exact Gaussian operations is not a new physical replay. + +Set the original main X input to zero. The first call has a main input channel +scaled by `e^-1`. At one port, a suitable original Y input is a scalar multiple +of `Q delta_0`; it makes source logical X a multiple of `delta_0` and logical +Y zero. For the second call, use a scalar multiple of `Q D1^-1 delta_0`. +It makes both source logical main inputs equal multiples of `delta_0`, up to +a common sign. These are the retained unitary boundary substitutions from +PR #4966. Each is a separate allowed input choice. + +Choose that main amplitude as B after the `e^-1` scaling. The original main +amplitude is then `B/2^k`. Choose one fresh helper input in that call's entrance +frame with logical amplitude `A/2^k`. The helper boundary has no e factor. +The two amplitudes vary independently. Other input channels can be zero. +A fixed rescaling puts their joint norm below one if required and leaves the +leading width bound unchanged. + +For each source orientation, the new checker propagates 520 independent +columns: 112 main channels in this restricted caller pattern and all 408 +helper inputs. It checks the complete endpoint on this subspace and every +helper return. This is not a new full 632-input endpoint proof. +Immediately before each paid occurrence, it records the first nonzero main +coefficient q and helper coefficient p, when both exist. The logical value +on this input slice is `p A/2^k + q B`. The physical frame is invertible, so it +does not identify two such values. + +The census gives: + +| Source orientation | H1 | H2 | H3 | H4 | H5 | H8 | +| --- | ---: | ---: | ---: | ---: | ---: | ---: | +| Forward | 1587 | 258 | 362 | 70 | 28 | 8 | +| Backward | 1576 | 148 | 380 | 95 | 12 | 0 | +| Total | 3163 | 406 | 742 | 165 | 40 | 8 | + +The certificate contains all 4,524 witnesses, with source event, owner, input +indices, exact coefficients and c. In all of them, `c<=2`. A single input is +not claimed to maximize all these occurrences. The uniform site-width premise +is what permits the sum of their separate required widths. + +## Complete declared invoice + +Both source calls retain all their productive helper targets. Their combined +helper profile is twice `{4:28,7:7,8:47,9:326}`. The declared main target adds +224 rank-17 outputs. The disjoint-axis splits are `4=3+1`, `5=3+2` and +`8=3+3+2`. They give: + +```text +targets = {4:56,7:14,8:94,9:652,17:224}, mass 10750; +raw paid = {1:4656,2:920,3:1386}, mass 10654; +width-charged = {1:7819,2:920,3:1386}, mass 13817. +``` + +The extra charge is only one leading H1 at each of the 3,163 witnessed +original rank-one occurrences. No width claim for an internal factor of a +higher-rank split is needed. The other wide-cut counts remain information +only. Scalar work, storage and routing cannot reduce this lower invoice. + +For the power tariff `r^t`, `0<=t<=1`, every target rank is at least four and +every charged paid rank is at most three. Therefore + +```text +T_t <= 4^(t-1) * 10750, +P_t >= 3^(t-1) * 13817, +T_t/P_t <= (4/3)^(t-1) * 10750/13817 <= 10750/13817 < 1. +``` + +This rejects every such moment for the stated uniform width policy. It does +not depend on a numerical root or an independent-error model. + +## Evidence and limits + +The written valuation and numerator arguments cover every sufficiently large +k under the stated premises. The verifier gives finite corroboration for all +75 coefficient pairs in the source certificate. It checks injectivity at k=5, +exact reduced numerators at k=32 and k=64, and six separate paid-cut executions +with four scalar inputs each. Removing all independent helper inputs removes +every two-band witness. Four in-process controls reject a false valuation +loss, a zero band, a missing final owned clear and a float in an exact receipt. +Isolated normal and optimized processes reject changed source bytes and a +changed witness coefficient. + +The result leaves open adaptive widths, joint symbolic state, changed scalar +words, changed helper boundaries, another cost law, and already funded larger +widths. It does not prove Gaussian/frame compatibility for recursively +substituted approximate children. No full physical Gaussian implementation, +uniform compiler, outer multiplication replay, or new kappa is supplied. + +Prepared by Ali Romman, with substantial OpenAI Codex assistance. The actual +source, caller, moving-frame audit and earlier contributors retain their credit +as stated in README.md and the pinned source files. Apache-2.0. diff --git a/research/two-full-exact-width-gate/README.md b/research/two-full-exact-width-gate/README.md new file mode 100644 index 0000000000..06f3cf2735 --- /dev/null +++ b/research/two-full-exact-width-gate/README.md @@ -0,0 +1,108 @@ +# Exact numerator width at two-FULL source cuts + +Exact arithmetic does not make the declared two-FULL border affordable under +one uniform width policy. The actual source has 4,524 paid cuts with two +independent integer bands. At each such cut, a literal exact numerator needs +leading width 2k rather than the budgeted k. Charging only the 3,163 original +rank-one cuts gives paid mass 13,817 versus target mass 10,750. Every power +moment with exponent in [0,1] then fails. **The complete kappa calculation +does not improve.** + +Read [the proof](PROOF.md), [exact result](RESULT.json), +[all occurrence witnesses](WITNESSES.json.gz), and [source pins](SOURCES.json). +The publication base is `32890bc5de034ab8fc93ac88ead7279a6a416d04`. + +## Exact scope + +The source operations are ideal and exact. The two integer amplitudes are +independent inputs; there are no independent operator faults. Each paid +occurrence has a width fixed for all its permitted inputs. The raw bill funds +`k+o(k)` bits and charges linearly in width, at fixed native rank and fixed +fiber/column multiplicity. Tensor-frame denominator offsets can grow with that +multiplicity; no limit with growing multiplicity is claimed. + +This is a source-specific gate for literal numerators, including a shared +exponent. It is not a lower bound for adaptive per-input width charges, joint +symbolic storage, different words, or a baseline that already funds a larger +leading width. Separate worst-case site witnesses do not prove one input +incurs their sum under an adaptive policy. + +The new census uses the retained moving-frame audit as a pinned live input. +That audit checks all 42,898 events and the zero-address phase of all 72 warp +matrices. The new code checks the 520-column restricted caller input space, +all independent helper returns, all 4,524 recorded cuts, and the full declared +helper and main target debit. It does not rerun physical Gaussian compilation. +The rank-split wide profile is informational; the rejection uses original H1 +cuts only. + +## Reproduce + +Use Python 3.12 and its standard library: + +```sh +python3 -B research/two-full-exact-width-gate/verify.py +python3 -O -B research/two-full-exact-width-gate/verify.py +python3 -B research/two-full-exact-width-gate/test_mutations.py +python3 -B scripts/research_package.py --package research/two-full-exact-width-gate +``` + +Expected direct output: + +```text +PASS_TWO_FULL_EXACT_WIDTH_GATE wide_sites=4524 extra_H1=3163 ratio_upper=10750/13817 new_kappa=false +PASS_TWO_FULL_WIDTH_MUTATIONS checks=4 normal_and_optimized=true +``` + +Default replay is read-only. `verify.py --write` rebuilds the certificate and +receipt. Regeneration compares decompressed canonical JSON, not gzip headers. +The source archive and inherited frame checker have exact byte pins. The two +live input paths in VERIFY.json must be present in a standalone export. No +Git or network access is needed by either direct scientific check. + +The controls reject an understated valuation loss, a zero band coefficient, +a missing final C0 clear, a float in an exact receipt, changed source bytes, +and a changed witness coefficient. The last two use isolated normal and +optimized subprocesses. The finite checks support the written proof; they +do not replace its all-k argument. + +## Related work and credit + +Cao Yifan supplied the retained round-three source and its full profile in the +[PR #4610 lineage](https://github.com/CrocSwap/integer-mult-bounds/pull/4610). +The [pinned source proof](https://github.com/CrocSwap/integer-mult-bounds/blob/32890bc5de034ab8fc93ac88ead7279a6a416d04/research/kappa-round3-warp-20261022/PROOF.md) +retains the native, helper and compiler lineage. + +Yiyang (@Lyy-iiis) supplied the actual caller, source boundary calculation and +moving-frame audit in [PR #4966](https://github.com/CrocSwap/integer-mult-bounds/pull/4966). +The [pinned caller proof](https://github.com/CrocSwap/integer-mult-bounds/blob/32890bc5de034ab8fc93ac88ead7279a6a416d04/research/two-full-border-paid-precision/paid-sensitivity/PROOF.md) +rejects a different, independent-error policy. Its +[pinned invariant audit](https://github.com/CrocSwap/integer-mult-bounds/blob/32890bc5de034ab8fc93ac88ead7279a6a416d04/research/two-full-border-paid-precision/independent-review/invariance/REVIEW.md) +supplies the exact logical-frame semantics reused here. Dillon's earlier +[PR #4623](https://github.com/CrocSwap/integer-mult-bounds/pull/4623) retains +credit for the border and recovery question. + +Cinna Davis's [PR #4983](https://github.com/CrocSwap/integer-mult-bounds/pull/4983) +concerns additive scalar compatibility. JoyboyBrian's +[PR #5106](https://github.com/CrocSwap/integer-mult-bounds/pull/5106) concerns a +coherent rank gauge. Neither argument is used as an exact width lower bound. +The rounded inverse and history frontier in +[PR #5444](https://github.com/CrocSwap/integer-mult-bounds/pull/5444) concerns +output-grid fibers and repeated recoding, not this source-cut numerator bill. +[OVERLAP.json](OVERLAP.json) records these distinctions and coverage limits. + +The new source census, width proof, checker and package were prepared by +Ali Romman (@aliromman), with substantial OpenAI Codex assistance. Parallel +agents are part of the author process, not independent human review. +Classical valuation, injective counting and rank separation are not claimed +as new general mathematics. New files are Apache-2.0. The source notices and +retained contributors remain unchanged. + +## Open next questions + +A changed exact representation needs a literal caller and a complete cost +comparison. Start with one paid cut and state where both independent bands +are stored, how its Gaussian action is computed, and what the input and return +costs are. Joint symbolic state, adaptive widths and larger funded baselines +are outside this theorem and need their own proofs. Recursive child +compatibility remains a separate obligation. [TASK.json](TASK.json) gives the +scoped follow-up and stop rule. diff --git a/research/two-full-exact-width-gate/RESULT.json b/research/two-full-exact-width-gate/RESULT.json new file mode 100644 index 0000000000..a46e31c12e --- /dev/null +++ b/research/two-full-exact-width-gate/RESULT.json @@ -0,0 +1,959 @@ +{ + "all_power_moments_ratio_upper": "10750/13817", + "baseline_paid": { + "1": 4656, + "2": 920, + "3": 1386 + }, + "charged_paid": { + "1": 7819, + "2": 920, + "3": 1386 + }, + "complete_targets": { + "4": 56, + "7": 14, + "8": 94, + "9": 652, + "17": 224 + }, + "direct_cut_checks": [ + { + "direction": "forward", + "event": 8200, + "samples": 4 + }, + { + "direction": "forward", + "event": 13513, + "samples": 4 + }, + { + "direction": "forward", + "event": 19172, + "samples": 4 + }, + { + "direction": "backward", + "event": 8148, + "samples": 4 + }, + { + "direction": "backward", + "event": 12436, + "samples": 4 + }, + { + "direction": "backward", + "event": 15235, + "samples": 4 + } + ], + "entropy_constant_max": 2, + "finite_injectivity": [ + { + "coarse": "-1", + "constant_loss": 0, + "distinct_values": 1024, + "fine": "-1", + "k": 5, + "reduced_numerator_bits": { + "32": 64, + "64": 128 + } + }, + { + "coarse": "-1/2", + "constant_loss": 1, + "distinct_values": 512, + "fine": "-1", + "k": 5, + "reduced_numerator_bits": { + "32": 63, + "64": 127 + } + }, + { + "coarse": "-2", + "constant_loss": 0, + "distinct_values": 1024, + "fine": "-1", + "k": 5, + "reduced_numerator_bits": { + "32": 65, + "64": 129 + } + }, + { + "coarse": "1", + "constant_loss": 0, + "distinct_values": 1024, + "fine": "-1", + "k": 5, + "reduced_numerator_bits": { + "32": 63, + "64": 127 + } + }, + { + "coarse": "1/2", + "constant_loss": 1, + "distinct_values": 512, + "fine": "-1", + "k": 5, + "reduced_numerator_bits": { + "32": 62, + "64": 126 + } + }, + { + "coarse": "-1", + "constant_loss": 0, + "distinct_values": 1024, + "fine": "-1/2", + "k": 5, + "reduced_numerator_bits": { + "32": 65, + "64": 129 + } + }, + { + "coarse": "-1/2", + "constant_loss": 0, + "distinct_values": 1024, + "fine": "-1/2", + "k": 5, + "reduced_numerator_bits": { + "32": 64, + "64": 128 + } + }, + { + "coarse": "-1/4", + "constant_loss": 1, + "distinct_values": 512, + "fine": "-1/2", + "k": 5, + "reduced_numerator_bits": { + "32": 63, + "64": 127 + } + }, + { + "coarse": "-2", + "constant_loss": 0, + "distinct_values": 1024, + "fine": "-1/2", + "k": 5, + "reduced_numerator_bits": { + "32": 66, + "64": 130 + } + }, + { + "coarse": "-3/2", + "constant_loss": 0, + "distinct_values": 1024, + "fine": "-1/2", + "k": 5, + "reduced_numerator_bits": { + "32": 65, + "64": 129 + } + }, + { + "coarse": "1", + "constant_loss": 0, + "distinct_values": 1024, + "fine": "-1/2", + "k": 5, + "reduced_numerator_bits": { + "32": 64, + "64": 128 + } + }, + { + "coarse": "1/2", + "constant_loss": 0, + "distinct_values": 1024, + "fine": "-1/2", + "k": 5, + "reduced_numerator_bits": { + "32": 63, + "64": 127 + } + }, + { + "coarse": "1/4", + "constant_loss": 1, + "distinct_values": 512, + "fine": "-1/2", + "k": 5, + "reduced_numerator_bits": { + "32": 62, + "64": 126 + } + }, + { + "coarse": "2", + "constant_loss": 0, + "distinct_values": 1024, + "fine": "-1/2", + "k": 5, + "reduced_numerator_bits": { + "32": 65, + "64": 129 + } + }, + { + "coarse": "-1", + "constant_loss": 0, + "distinct_values": 1024, + "fine": "-1/4", + "k": 5, + "reduced_numerator_bits": { + "32": 66, + "64": 130 + } + }, + { + "coarse": "-1/2", + "constant_loss": 0, + "distinct_values": 1024, + "fine": "-1/4", + "k": 5, + "reduced_numerator_bits": { + "32": 65, + "64": 129 + } + }, + { + "coarse": "-1/4", + "constant_loss": 0, + "distinct_values": 1024, + "fine": "-1/4", + "k": 5, + "reduced_numerator_bits": { + "32": 64, + "64": 128 + } + }, + { + "coarse": "1", + "constant_loss": 0, + "distinct_values": 1024, + "fine": "-1/4", + "k": 5, + "reduced_numerator_bits": { + "32": 65, + "64": 129 + } + }, + { + "coarse": "1/2", + "constant_loss": 0, + "distinct_values": 1024, + "fine": "-1/4", + "k": 5, + "reduced_numerator_bits": { + "32": 64, + "64": 128 + } + }, + { + "coarse": "1/4", + "constant_loss": 0, + "distinct_values": 1024, + "fine": "-1/4", + "k": 5, + "reduced_numerator_bits": { + "32": 63, + "64": 127 + } + }, + { + "coarse": "-1/2", + "constant_loss": 0, + "distinct_values": 1024, + "fine": "-1/8", + "k": 5, + "reduced_numerator_bits": { + "32": 66, + "64": 130 + } + }, + { + "coarse": "-1/4", + "constant_loss": 0, + "distinct_values": 1024, + "fine": "-1/8", + "k": 5, + "reduced_numerator_bits": { + "32": 65, + "64": 129 + } + }, + { + "coarse": "1/2", + "constant_loss": 0, + "distinct_values": 1024, + "fine": "-1/8", + "k": 5, + "reduced_numerator_bits": { + "32": 65, + "64": 129 + } + }, + { + "coarse": "1/4", + "constant_loss": 0, + "distinct_values": 1024, + "fine": "-1/8", + "k": 5, + "reduced_numerator_bits": { + "32": 64, + "64": 128 + } + }, + { + "coarse": "-1", + "constant_loss": 1, + "distinct_values": 512, + "fine": "-2", + "k": 5, + "reduced_numerator_bits": { + "32": 63, + "64": 127 + } + }, + { + "coarse": "-2", + "constant_loss": 0, + "distinct_values": 1024, + "fine": "-2", + "k": 5, + "reduced_numerator_bits": { + "32": 64, + "64": 128 + } + }, + { + "coarse": "1", + "constant_loss": 1, + "distinct_values": 512, + "fine": "-2", + "k": 5, + "reduced_numerator_bits": { + "32": 62, + "64": 126 + } + }, + { + "coarse": "-1/2", + "constant_loss": 0, + "distinct_values": 1024, + "fine": "-3/2", + "k": 5, + "reduced_numerator_bits": { + "32": 64, + "64": 128 + } + }, + { + "coarse": "-3/2", + "constant_loss": 0, + "distinct_values": 1024, + "fine": "-3/2", + "k": 5, + "reduced_numerator_bits": { + "32": 65, + "64": 129 + } + }, + { + "coarse": "-1/2", + "constant_loss": 0, + "distinct_values": 1024, + "fine": "-3/4", + "k": 5, + "reduced_numerator_bits": { + "32": 65, + "64": 129 + } + }, + { + "coarse": "1/2", + "constant_loss": 0, + "distinct_values": 1024, + "fine": "-3/4", + "k": 5, + "reduced_numerator_bits": { + "32": 64, + "64": 128 + } + }, + { + "coarse": "1/2", + "constant_loss": 0, + "distinct_values": 1024, + "fine": "-3/8", + "k": 5, + "reduced_numerator_bits": { + "32": 65, + "64": 129 + } + }, + { + "coarse": "-1", + "constant_loss": 2, + "distinct_values": 256, + "fine": "-4", + "k": 5, + "reduced_numerator_bits": { + "32": 62, + "64": 126 + } + }, + { + "coarse": "1", + "constant_loss": 2, + "distinct_values": 256, + "fine": "-4", + "k": 5, + "reduced_numerator_bits": { + "32": 61, + "64": 125 + } + }, + { + "coarse": "-1", + "constant_loss": 0, + "distinct_values": 1024, + "fine": "1", + "k": 5, + "reduced_numerator_bits": { + "32": 63, + "64": 127 + } + }, + { + "coarse": "-1/2", + "constant_loss": 1, + "distinct_values": 512, + "fine": "1", + "k": 5, + "reduced_numerator_bits": { + "32": 62, + "64": 126 + } + }, + { + "coarse": "-2", + "constant_loss": 0, + "distinct_values": 1024, + "fine": "1", + "k": 5, + "reduced_numerator_bits": { + "32": 64, + "64": 128 + } + }, + { + "coarse": "-5/2", + "constant_loss": 1, + "distinct_values": 512, + "fine": "1", + "k": 5, + "reduced_numerator_bits": { + "32": 65, + "64": 129 + } + }, + { + "coarse": "1", + "constant_loss": 0, + "distinct_values": 1024, + "fine": "1", + "k": 5, + "reduced_numerator_bits": { + "32": 64, + "64": 128 + } + }, + { + "coarse": "1/2", + "constant_loss": 1, + "distinct_values": 512, + "fine": "1", + "k": 5, + "reduced_numerator_bits": { + "32": 63, + "64": 127 + } + }, + { + "coarse": "2", + "constant_loss": 0, + "distinct_values": 1024, + "fine": "1", + "k": 5, + "reduced_numerator_bits": { + "32": 65, + "64": 129 + } + }, + { + "coarse": "3/2", + "constant_loss": 1, + "distinct_values": 512, + "fine": "1", + "k": 5, + "reduced_numerator_bits": { + "32": 64, + "64": 128 + } + }, + { + "coarse": "5/2", + "constant_loss": 1, + "distinct_values": 512, + "fine": "1", + "k": 5, + "reduced_numerator_bits": { + "32": 65, + "64": 129 + } + }, + { + "coarse": "7/2", + "constant_loss": 1, + "distinct_values": 512, + "fine": "1", + "k": 5, + "reduced_numerator_bits": { + "32": 65, + "64": 129 + } + }, + { + "coarse": "-1", + "constant_loss": 0, + "distinct_values": 1024, + "fine": "1/2", + "k": 5, + "reduced_numerator_bits": { + "32": 64, + "64": 128 + } + }, + { + "coarse": "-1/2", + "constant_loss": 0, + "distinct_values": 1024, + "fine": "1/2", + "k": 5, + "reduced_numerator_bits": { + "32": 63, + "64": 127 + } + }, + { + "coarse": "-1/4", + "constant_loss": 1, + "distinct_values": 512, + "fine": "1/2", + "k": 5, + "reduced_numerator_bits": { + "32": 62, + "64": 126 + } + }, + { + "coarse": "-2", + "constant_loss": 0, + "distinct_values": 1024, + "fine": "1/2", + "k": 5, + "reduced_numerator_bits": { + "32": 65, + "64": 129 + } + }, + { + "coarse": "1", + "constant_loss": 0, + "distinct_values": 1024, + "fine": "1/2", + "k": 5, + "reduced_numerator_bits": { + "32": 65, + "64": 129 + } + }, + { + "coarse": "1/2", + "constant_loss": 0, + "distinct_values": 1024, + "fine": "1/2", + "k": 5, + "reduced_numerator_bits": { + "32": 64, + "64": 128 + } + }, + { + "coarse": "1/4", + "constant_loss": 1, + "distinct_values": 512, + "fine": "1/2", + "k": 5, + "reduced_numerator_bits": { + "32": 63, + "64": 127 + } + }, + { + "coarse": "3/2", + "constant_loss": 0, + "distinct_values": 1024, + "fine": "1/2", + "k": 5, + "reduced_numerator_bits": { + "32": 65, + "64": 129 + } + }, + { + "coarse": "-1", + "constant_loss": 0, + "distinct_values": 1024, + "fine": "1/4", + "k": 5, + "reduced_numerator_bits": { + "32": 65, + "64": 129 + } + }, + { + "coarse": "-1/2", + "constant_loss": 0, + "distinct_values": 1024, + "fine": "1/4", + "k": 5, + "reduced_numerator_bits": { + "32": 64, + "64": 128 + } + }, + { + "coarse": "-1/4", + "constant_loss": 0, + "distinct_values": 1024, + "fine": "1/4", + "k": 5, + "reduced_numerator_bits": { + "32": 63, + "64": 127 + } + }, + { + "coarse": "-5/8", + "constant_loss": 1, + "distinct_values": 512, + "fine": "1/4", + "k": 5, + "reduced_numerator_bits": { + "32": 65, + "64": 129 + } + }, + { + "coarse": "1", + "constant_loss": 0, + "distinct_values": 1024, + "fine": "1/4", + "k": 5, + "reduced_numerator_bits": { + "32": 66, + "64": 130 + } + }, + { + "coarse": "1/2", + "constant_loss": 0, + "distinct_values": 1024, + "fine": "1/4", + "k": 5, + "reduced_numerator_bits": { + "32": 65, + "64": 129 + } + }, + { + "coarse": "1/4", + "constant_loss": 0, + "distinct_values": 1024, + "fine": "1/4", + "k": 5, + "reduced_numerator_bits": { + "32": 64, + "64": 128 + } + }, + { + "coarse": "3/8", + "constant_loss": 1, + "distinct_values": 512, + "fine": "1/4", + "k": 5, + "reduced_numerator_bits": { + "32": 64, + "64": 128 + } + }, + { + "coarse": "5/8", + "constant_loss": 1, + "distinct_values": 512, + "fine": "1/4", + "k": 5, + "reduced_numerator_bits": { + "32": 65, + "64": 129 + } + }, + { + "coarse": "-1/2", + "constant_loss": 0, + "distinct_values": 1024, + "fine": "1/8", + "k": 5, + "reduced_numerator_bits": { + "32": 65, + "64": 129 + } + }, + { + "coarse": "1/2", + "constant_loss": 0, + "distinct_values": 1024, + "fine": "1/8", + "k": 5, + "reduced_numerator_bits": { + "32": 66, + "64": 130 + } + }, + { + "coarse": "1/4", + "constant_loss": 0, + "distinct_values": 1024, + "fine": "1/8", + "k": 5, + "reduced_numerator_bits": { + "32": 65, + "64": 129 + } + }, + { + "coarse": "-1", + "constant_loss": 1, + "distinct_values": 512, + "fine": "2", + "k": 5, + "reduced_numerator_bits": { + "32": 62, + "64": 126 + } + }, + { + "coarse": "-2", + "constant_loss": 0, + "distinct_values": 1024, + "fine": "2", + "k": 5, + "reduced_numerator_bits": { + "32": 63, + "64": 127 + } + }, + { + "coarse": "1", + "constant_loss": 1, + "distinct_values": 512, + "fine": "2", + "k": 5, + "reduced_numerator_bits": { + "32": 63, + "64": 127 + } + }, + { + "coarse": "-2", + "constant_loss": 0, + "distinct_values": 1024, + "fine": "3", + "k": 5, + "reduced_numerator_bits": { + "32": 64, + "64": 128 + } + }, + { + "coarse": "-1/2", + "constant_loss": 0, + "distinct_values": 1024, + "fine": "3/2", + "k": 5, + "reduced_numerator_bits": { + "32": 63, + "64": 127 + } + }, + { + "coarse": "1", + "constant_loss": 0, + "distinct_values": 1024, + "fine": "3/2", + "k": 5, + "reduced_numerator_bits": { + "32": 65, + "64": 129 + } + }, + { + "coarse": "-1/2", + "constant_loss": 0, + "distinct_values": 1024, + "fine": "3/4", + "k": 5, + "reduced_numerator_bits": { + "32": 64, + "64": 128 + } + }, + { + "coarse": "1", + "constant_loss": 0, + "distinct_values": 1024, + "fine": "3/4", + "k": 5, + "reduced_numerator_bits": { + "32": 66, + "64": 130 + } + }, + { + "coarse": "-1/4", + "constant_loss": 0, + "distinct_values": 1024, + "fine": "3/8", + "k": 5, + "reduced_numerator_bits": { + "32": 64, + "64": 128 + } + }, + { + "coarse": "1", + "constant_loss": 2, + "distinct_values": 256, + "fine": "4", + "k": 5, + "reduced_numerator_bits": { + "32": 62, + "64": 126 + } + }, + { + "coarse": "1", + "constant_loss": 0, + "distinct_values": 1024, + "fine": "5/4", + "k": 5, + "reduced_numerator_bits": { + "32": 66, + "64": 130 + } + } + ], + "frame_audit": { + "all_contacts_and_transports_checked": true, + "events": 42898, + "status": "PASS_INDEPENDENT_LOGICAL_ZERO_ADDRESS_AND_FRAMES", + "warp_matrices": 72 + }, + "negative_controls": [ + { + "name": "understated_valuation_loss", + "reason": "The declared two-band map is not injective", + "result": "REJECT" + }, + { + "name": "zero_band_coefficient", + "reason": "The valuation needs a nonzero number", + "result": "REJECT" + }, + { + "name": "removed_final_owned_clear", + "reason": "The owned center does not return to zero", + "result": "REJECT" + }, + { + "name": "integer_to_float_receipt", + "reason": "The retained exact receipt differs", + "result": "REJECT" + } + ], + "new_kappa": false, + "no_helper_controls": [ + { + "direction": "forward", + "wide_sites": 0 + }, + { + "direction": "backward", + "wide_sites": 0 + } + ], + "omitted": [ + "Adaptive-width sum bound", + "Joint symbolic-state lower bound", + "A limit with growing fiber/column multiplicity", + "Full physical Gaussian execution", + "Recursive child compatibility", + "Compiler and outer multiplication replay" + ], + "original_paid_sites": 6596, + "original_wide_profile": { + "1": 3163, + "2": 406, + "3": 742, + "4": 165, + "5": 40, + "8": 8 + }, + "policy": { + "baseline_width": "k+o(k)", + "limit": "k tends to infinity at fixed native rank and fixed fiber/column multiplicity", + "representation": "Literal exact per-register numerator; one shared exponent is allowed", + "site_width": "Uniform over all permitted inputs at each paid occurrence", + "width_tariff": "Linear in the leading width" + }, + "rank_masses": { + "baseline": 10654, + "charged": 13817, + "target": 10750 + }, + "restricted_independent_columns_per_call": 520, + "schema": "two-full-exact-width-gate/v1", + "source_payload_sha256": "cfcd36b40326d7a5815e1db5313444379b3fb756b27d5201c561574c085cc0dd", + "split_wide_profile_information_only": { + "1": 3328, + "2": 454, + "3": 963 + }, + "status": "PASS_TWO_FULL_EXACT_WIDTH_GATE", + "wide_sites": 4524, + "witness_payload_sha256": "a1247f0c63c5687c048d18210cc215a269d5b46fce6590baa03f2817329da838" +} diff --git a/research/two-full-exact-width-gate/SOURCES.json b/research/two-full-exact-width-gate/SOURCES.json new file mode 100644 index 0000000000..a09a4cd39c --- /dev/null +++ b/research/two-full-exact-width-gate/SOURCES.json @@ -0,0 +1,60 @@ +{ + "schema_version": 1, + "base_commit": "32890bc5de034ab8fc93ac88ead7279a6a416d04", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "fc3d4ba105e1f097d0d7d051a308281e86ab1446", + "sha256": "66974efdced4083c00025f97d95d83909a226cdf801edb9301c195c6641f6903" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "f126dd2e2dad2b669e75d1d0d0bd05c600725602", + "sha256": "f7a48bfa2659b88378282a8eee7d9fe52cdf505594124c4d1686b58510fffd72" + }, + { + "path": "research/kappa-round3-warp-20261022/ACTUAL-WORD.json.gz", + "usage": "input", + "git_blob": "46d929df83817b85a5387bcdb9745e0627d6366e", + "sha256": "7679daa4ec6a40f56fc7f0202379a6f454310e94945aba4f48beaaaafb838d05" + }, + { + "path": "research/two-full-border-paid-precision/independent-review/invariance/check_invariance.py", + "usage": "input", + "git_blob": "0c0206973d92113e117bab4370202b7113d47451", + "sha256": "7d134b9a2d16eae37654da5877353a70bb5a9bbde5bf368d8f6ceed0adef1433" + }, + { + "path": "research/kappa-round3-warp-20261022/PROOF.md", + "usage": "provenance", + "git_blob": "97f1d19ad423fe5540cc2986fb51af24a251d57c", + "sha256": "19178996b776a33f94c8df905b2ef07cc3069e4b6004180f8ec58e140f0c7f7c" + }, + { + "path": "research/two-full-border-paid-precision/paid-sensitivity/PROOF.md", + "usage": "provenance", + "git_blob": "f2260e452a301c86238ac88976fba16fae69456a", + "sha256": "8b47f2a6c6bd8e6ef035e0faeced6877037a6beac3b8cb535617988d0c3088b3" + }, + { + "path": "research/two-full-border-paid-precision/independent-review/invariance/REVIEW.md", + "usage": "provenance", + "git_blob": "5db51dcfa27f6b67ce246edfdfd42caac2d53395", + "sha256": "3bb8701b7b032c6350736ca418b0f22c69a9ea816ddeaa64d0d000199cbe008d" + }, + { + "path": "research/coherent-frame-additivity/PROOF.md", + "usage": "provenance", + "git_blob": "67dd02c9d31d77be390a9e3fdfc09c7dd8de56c2", + "sha256": "0f72ad943e6f1803d6cdc5749f6b6880463fc8dba8ce57e8de3c3550a8eaea79" + }, + { + "path": "research/two-full-fresh-d-coherent-pair/PROOF.md", + "usage": "provenance", + "git_blob": "d2325a97a7bc67428111b016b3c4f2adcca84f42", + "sha256": "300da0c914c097c4ea2e3a26d071221a5b25f652f1191ed25098ed189ae99f6e" + } + ] +} diff --git a/research/two-full-exact-width-gate/TASK.json b/research/two-full-exact-width-gate/TASK.json new file mode 100644 index 0000000000..3a8ac50c3a --- /dev/null +++ b/research/two-full-exact-width-gate/TASK.json @@ -0,0 +1,96 @@ +{ + "schema_version": 1, + "task_id": "joint-query-controller", + "priority_revision": 7, + "base_commit": "32890bc5de034ab8fc93ac88ead7279a6a416d04", + "original_card": { + "id": "joint-query-controller", + "question": "Can the installed QQ16 caller win a complete matched protocol bill, or can a changed demand eliminate actual paid work?", + "starting_points": [ + "docs/research/research-family-status.md", + "certificates/selected-result.json", + "research/qq16-caller-install/README.md" + ], + "methods": [ + "Derive the matched whole-caller physical bill for installed and baseline protocols.", + "Change the actual demanded observations and prove a cheaper legal producer/consumer contract." + ], + "acceptance_gate": "Name the changed premise of the fixed F0/B1 observation obstruction. Show exactly which query is recovered, legal native reads and restoration, and a full favorable budget including cover maps, helpers and endpoints. Local inverse identities alone do not close the global controller. 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.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read #4166 COST.md and ADMISSION.json. An actual caller connection is now proposed. Its native-component profile loses; parent park/restore versus external-call costs remain unresolved. Retain the producer and recovery lineage rather than rebuild it.", + "scope": "Source-binding orientation only; no scientific replay, theorem acceptance or supplier admission. Budget any heavy replay separately." + }, + "first_experiment": "At the actual installed cut, compare matched complete parent park/restore and external input/return protocols at the same bank/packet geometry, including every later root call and service cost. Alternatively pin both bridge observations and derive a genuinely smaller source-compatible demand. Stop if the complete necessary inequality fails or an essential cost is unknown; no larger decoder scan from a local tape-action saving.", + "bottleneck_link": "The native local words exist; retained query information and its physical access are the missing link to a composed recursive interface.", + "allowed_variations": [ + "One paid query, one changed first pair, or one precisely specified affine helper state.", + "A counterexample or lower bound for that exact proposed repair.", + "One unresolved obligation of a newer local decoder, with exact source heads and a distinct claim/domain." + ], + "scope_change_triggers": [ + "Retaining the fixed first pair and ordinary schedule while allowing only homogeneous selected-only control, already excluded by the witness.", + "Treating cover-map counts as zero-cost physical address operations.", + "Recreating the pending complete local decoder or early-record/output-bank coalescing already under investigation without a distinct audit or changed premise.", + "Treating a completed-output defect inequality as a producer-interior, dirty-range or physical-cost certificate.", + "Recreating completed-output recovery or caller wiring already supplied by #4166 without new independent coverage.", + "Dropping retained later root calls or claiming native-profile dominance from the isolated publication saving." + ], + "overlap_terms": [ + "QQ16", + "joint-query", + "changing-chart controller", + "selected observation", + "1969", + "2540", + "early record", + "output-bank retention", + "complete native decoder", + "2965", + "producer defect", + "dirty-helper range", + "F17 consumer", + "4166", + "qq16-caller-install" + ], + "existing_checks": [ + { + "scope": "PR #4166: author-checked installed producer/service/return/bridge connection; native-component comparison loses.", + "evidence": "research/qq16-caller-install/README.md", + "remaining": "Complete matched physical protocol bill, or changed source-compatible demand/circuit; no affordable supplier yet.", + "status": "author-checked", + "source_commit": "0b082d22a0e9a442d264ab0633e35ef26c790630", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + } + ] + }, + "scope_status": "changed", + "actual_scope": "Prove the exact two-band numerator width gate for the retained two-FULL caller under uniform per-occurrence linear width charges, at fixed rank and fixed fiber/column multiplicity.", + "scope_change_reason": "The user assigned publication of a saved source-specific exact-execution result. This package does not pursue the historical QQ16 installation card or start another search.", + "bottleneck_link": "Exact arithmetic removes independent rounding faults, but a literal register still combines independently scaled input bands. The source census tests whether the declared k-bit budget pays for that exact value.", + "budget_minutes": 60, + "stop_rule": "Complete the uniform-site width theorem, exact source census, rejected controls and portable replay. Do not infer an adaptive-width or universal arithmetic lower bound.", + "outcome": "negative-result", + "evidence": "PROOF.md, WITNESSES.json.gz, RESULT.json, and the registered source-bound checks.", + "author": "Ali Romman, with substantial OpenAI Codex assistance", + "ai_assistance": "Substantial OpenAI Codex assistance in the original census, proof, code and writing. Parallel agent review is part of the author process; no independent human or proof-kernel review is claimed.", + "open_questions": [ + { + "question": "Can a changed exact representation or adaptive policy close one actual paid caller at a favorable complete bill?", + "why_it_matters": "The present rejection applies only to literal exact numerators and uniform site widths.", + "first_step": "Choose one marked source cut and specify its two-band representation, Gaussian action, input access, return and complete width cost.", + "blocked_by": "No such complete alternate caller or adaptive sum bound is supplied." + }, + { + "question": "Can recursively substituted approximate children preserve the exact frame and fresh-D identities at this caller?", + "why_it_matters": "One ideal exact execution does not prove the recursive compatibility needed by the border.", + "first_step": "State one concrete child contract and check the actual common-frame scalar and free-warp relations.", + "blocked_by": "The package uses inherited ideal operator semantics and performs no recursive physical replay." + } + ] +} diff --git a/research/two-full-exact-width-gate/VERIFY.json b/research/two-full-exact-width-gate/VERIFY.json new file mode 100644 index 0000000000..16e876aa8c --- /dev/null +++ b/research/two-full-exact-width-gate/VERIFY.json @@ -0,0 +1,30 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/kappa-round3-warp-20261022/ACTUAL-WORD.json.gz", + "research/two-full-border-paid-precision/independent-review/invariance/check_invariance.py" + ], + "commands": [ + { + "argv": [ + "{python}", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 180, + "checks": "Retained moving-frame audit; exact 4524-cut census; 75 coefficient pairs; six direct cut checks; four internal rejection controls; full declared target and uniform width bill." + }, + { + "argv": [ + "{python}", + "-B", + "{package}/test_mutations.py" + ], + "timeout_seconds": 300, + "checks": "Changed source bytes and witness coefficients are rejected in isolated normal and optimized processes." + } + ] +} diff --git a/research/two-full-exact-width-gate/WITNESSES.json.gz b/research/two-full-exact-width-gate/WITNESSES.json.gz new file mode 100644 index 0000000000000000000000000000000000000000..f8e0a762bde9d6610b5ef9bf6b6fee91ec6553cd GIT binary patch literal 65448 zcmXtfbzD=A_xCnn3>YwaBL^E@qf23QOGt+_0+Nc9AfratKuV+$2`N#!8$?P(R2mde zQYjJm@%g@<=l*l=>z>=^yidH(xg3cQz<&#f?tSOi6!d61_nGK1Ym5;CP3LhPl#w{w zHd$EcIr?)x8x;I|zq({6z4in2bPDCV*2MHlI0nI+I%>Lk)E$04%W?hh$MxUM<*SS9 ztIg%`>kFUozr*|Cm*b+>C*$G&j`y#Br-omj+9^Ig|H^T*q4aNl|N89pHP=fsrKhcz zs@Z3|qSt2^cGoA}R|gf{SDW2ehr`|f)~Um#F6eb)~1*v-|7a|7gR{4>_J*k1tyMw zxVrcF$)N}kYVrrVQz^1&W{knA_FXVY6% z#eHd+iTGA#_J^Puo=PS?d#S@H!?G2x*PctN`Xao@aGk>vns$5}oHoGdWF1%sj?X8? zKAaef{JsfKVOl8iBx;>LO`>-?P}Bw*fBhqgx`mHPiM6`BO(QfBpX2-LkAxBi*+0=6 zn=u%=V0`S}0Ym$PQFcf3+|9hr=jhd=ko?;T%3;)7V)UDNe&(sINY>*Y5DFoyylM>0o$ysC~1{Bib!p*Aakx(jj%$Q@tKw4X1?u@?A9Y9(f zyhfijZ!^?`bp1;&2OAI%dW2+@|BNLykQWCK$1%(nup|Z2)65@=&>BJGmOm#3e)V_- z-K!gS+bE#GfkNcJJ!a`x!JwOOvDKp(rd<{_(wt!Ur&<77v13J-`d|C0Ll}ak|NS@ z9o5z&m`s)%MMMEv4@1Ru+5?5wFC}c%+VhYwhM7ZsX)|%C+>>l05n4bgaHrFfyv_Ps z(nXI*$uvVG=k)pVtWI<>NA)-#4FUj+j&+&EF7DEK7ieHWKme=y((lDDk4{Eaq|e$# zN`;@k1@I+QC>lyTH`=Ns}!`F>2eku4zU<_;ml!(p+T1YUvDVA7m|UR;jA3 z2;;maFiWpaWQaz)eBoAQWW`(5k0)WsdyT>tFlD;78VhbfEKt^4J!#NTl~}__lRl>C z)vCY9n4btes2S4Z8|U`b;Ze0Tc~o!38^2pcbB1Z@Nyq98^H)Y}29{ED{k|K5A(T>Y zzv0v>vjjDMFn@8xd@#to1M!g(*m!sSIp5mXjLMo!`K}L?^kc{|@rZf9;I?nQq8#vO z9{<>GH!9dL(ArmOjt!WR-y>v~`?^n}TMSw1wXn^ikeO{T9@F#cKIVvobGUyH;RcNN zda#uFS;tI5Yk}0bey;LsKI^2{{V59|dZX^(-QT}SEik@^mVEk!6LbJ>TN5LzUfe*? zgj*L)TvQz*NDAm@Gt2)D+V?8^y$-VzhR>$)V2TTZvXupSlY#Cwyta!u{Q}QQt%i#S z?k;3glM%1rY~t=*?yt0nlE$?R?r=3k@KwpM;F(L`{S;(@uDDToZk_$4jCBY%VoJvq zV_#a0?R}e{Q8a_{x1a2sit2!h))6-At(B}1*-O6ClCgmT@=%Bl8N0_7HlcV|N8y;1 zAAyaGPH=fN`2HbrZ#{XP+bWPKViWlsEGYc^VL~r;0Ag2|j08aFFm?W=sgmxWTge5< z+$rLs&V)yvib(KP0#d$LAx$Xl%(4*zpdM_tw%6aja{W^Hm}N+Aq(T}P;J_yxfvRZ; zpx}viO^R6=*^7oB@e7{^sNkfG-!hV_WFa4TQb&=c)3|cV_7L_jAV&1GC|sHC?4PP$ z6&o*VgNext z0h<(7Sw8Qr=x0QQh_p76M1LjTZ!R6ZkhFske)W$shgdp|(1b7mbp2*7q}&>^T3x3i zi`@6?9p4cLfio@;zNIU*f8Xu=gZAD;3{$j`-8U9obX|=|1J3P>y3;=`I4p&UvcCj} z75RyF0;g{z@(89YBbi=PJa7PkxI!0R$?_2EOmY;jsd+tj$&$Jf-}oah{L(cCf?e~~ zvf8U1sK=;{rx8cu{5#Ev*zh`KDT$QwaIEo%3e?iqyIfSIiG~AM6MI^}jHD*L11VL; zWtX;5Ivqg5Z=c2CC+Ui7e_uB^0>or(gr64mO|{LrfEf_Dh+F*cI>C}%4@lOndaX2i zv68=({l2;j8I`O)owb;y4OzQGg6k`&Ql3a#@p#}0FmfifzQD$Ey3M;cC~K17=aq3%ushdPGvaP8Tk+<(A5pd*0CGMC&m;|#kI;07Y=js?q-y8_#@XNo?<;^J zEh^6eQ<+F*nLbD*j8&}A$M36yG<_ud`-Rw5*wRA1x@c!2&T|w$2N~d@4$+j-dW(_(T*Sveon6L( zuW{J?7^^8ZWyHgV02tru672fj3%)(C$_Gz^lykM8BxIjQ+rtgF#BbYw%$T~smehs# zN|v?Sy7ECHRd3O6M8H&6zPf-p832S6qM>5_q7XQ(>N5m+WX~(AWm8)}xQ>S*ee_ntVtqU&VnnzPl$I}^dO%2b1JIJ9_yMw?`=f+_jGC&>B`?+xM15=65h5xU zPI8sW&-+B$Om90q8ZhX=1s3M0d&vykG=Q=Y!-py<)!LlVYFl|JYF>3{WGQXHG{Ijs zdcKEAmB7j;$9Xb`Ga>-6jgM-*U(35yrEmtbd(WxPw))>9aMS==_Y$rCiD9U%d=lGU zej>6rzD4w&N!KNnG5R|%xU568fH4Iim)~aaI|e`#s8hqa0qw*!oeuKMq6|~!n>BhO z0sKA~`*$A$HPW$r&#N+k)@z~<9G(u@0dkl~Pp^*c|HK&sxUyMAt3=xBSV6|M%*(u> z^rq?|du?%`>!f?qbgU&5vJYc;lia3)lO!jO1K-@QwF)+GrM$M+9m*A|la(?W**bXR>naj^)F@b6u2VQD%+4 z-7&k=>3;8D@oKv@0^`3d#O7HP#mk1k8r^8# zDj$62`^Hf*?QQlg%s_{& z>y#0Ye&mgUSQYDf19i-_3qAyi**Ujk5XFob&hLol#cY6kaQ7Aiz2<1&z2U_E5=XUw zd?9kP4kM*)Ni#+uK-BHfVdi^cERnP?KFuAFM?@Y!>rSQ_L~?^>e=Ae_6e4E`_-;1;;GYFI^>XyE~ zS$LidJohS==xPuRlFNH#upWb?;V}E;HV&8i;6^dxH=XEnVZY&f`@xU^Bxmg^-g0&k zp#(Y?3F`h}Kj>+Ch6n~?JzDr+x33rhyq4=Rrsec7y;f%nJ4p1j2qK)J*S=}|?+`&5 z{c!YO83ux~YlIka5u;**77Sa^5FLjtmlvmh*^VOn(|Q7Py+Z_nd@vOY>E)n39~4<2 zhb@{E79;z}fln#`u^9=ZAB~`}qK;*jE)9Ll{iJTDtx&8jM2*YvhSNsEOTQw#QP9*I~R+oG6 z*o>j8MMb%I$W}QcK z1b!VS*pTUXw-vr8t?4JeUs%~94|^QfBm+0g9*%L=+Gy9KHZ?{9NQdIDOcY8Pb=Mm= z2c}5rz(j364ki7DLBGVKsKCDUq-^JRG>5jgxNDa)j!a zE$j9YGTWDWM*XirOmWb6r87VRskG47`!micBH6V0{-$P&7oQUO@hB7rt1@ir)yTVI zE1s`}USL3O6%#!5+(3hS+p!lHwA~>w0DUKeDxn6jF2R2 zzkV4BC+rk)Q)4~vspEjpfm$PSn$3(X zlIon zYzYy^`O=U}99O&6bt4x3`1<_z{_gU~xXTwuNL!m8FFGBGIhmjJU0{iCHyBuDUQ%5K zaJ|~ljV|`99*1(#f{22xzd1){b%omqwn0qk)$vP9G7}$XAV$!uy74XJqoftS6c4dG z>pjRL6G~zd*%$}=epp)|!i6Ya-O7KCvKF6uqxoH&Z(J<3osy8ML-n}iWxW6heLiGj z1MR&@*o+v6%R(d^Z#?*W`!Y^!o{!1k94yU0m&P23L&UkP^xJKvw(H^065|L&3SMIM17U7)_rYP3jm?%Rp3h@PG zUo=&gz@IJLrv9+1fsXxdD<92Cf9p^G=giG%QO^_;_WvWds@n|0tt)8bwiP&!!&0LN zhuA*>&z81cG&#UBcW#uNls|o=WJ!*DDW=UgiTTRPmiIu?_I?sdFfyhi$wJm5rH~UI ztuB%nbG*scM-ZtLw865{iZZWA6lZCEoCTNC*9Wdpcg{* zYw0t4T0l73D=1c<$(=G9nBM^}{QJSTUj@(kY+w8~I4c^*$KE!*_q1$PwoR)VPDR$c z`rK+8ve_rDS_WN)O}diM1b^QG4S( zn{Ut?k!C_l5?nL@>kG_P)>g+!nlr4ro;9_-H>4%jMBh|b{6Ag!ZmvtI!we$Qp?sj~ zBZBoa7_4d@t!7k4PlIL$?t8pR zdS_0_h>tEMtMHbafnKNGqo@!PO;|T|YC!)F$eBib=XsX8j`Uic zZn<3QFzwZ!Lqq%y_76W7^07_YE6lI&l|gA>v10>QF)k|h*x{!`PX_Pgu01X2^(8f! zTp>$9UChu>`VVN6qA(}CY#Pboq#7;j@Nnui!(6x_a&p+MYsJaORx>k(y5GF~J~ZSN zfewTMVonlH9x4$WT2709D8fmMfUu-TyOiN@(UT!Nn-~KSU9IKzrwXXOp#6-tWV8*ja=QKulzxuch(m^G;=>;# zyk&3*e^eSR3?8SH>KiJRPo+mXaYhc}I`>E3KPa}X;O3GYk)wY_`Ivg}-g6{>Jv^@Jgu`2|rTGSsH= zLs9Gbjo|#%@a6F2wAy`KRoNwTu?s$?*}bf z?XZUNXlXio!Ldm`Xs>afLIW&P-LGj%(Tzhdv|ne%sF}~TUaD(=M)OldU6-5 zVTgU%3kR2V&0ErL2+bKq`fljQQz*wL@(3f-0vTe-stny8gNSC<6o_0RK`xX8PRVCD z74>hr2kXpn2-?uw4j*$Xu`fz!HOO~6Nd`Cd$6@S&tPF#kUHiko%dQ`wq$rmU&%i*$PUH6?T!CiczZZf+$fjJ`-#?>VVs z_6)|din{ILn|?P)(sx$tc!$cIv7{|><;V_Kn)PUSDCZ%vjD#4xG94)Vsf5EBqSyAH zqev3!!X$Za`T8V6QvB7&t6!227~M$?G}m-X3Y5B|M>$&ju+vfJhN#7tM$aw|M@>t$ zQNOTs(_%mV2U+MA516+0J`?fx(qB3U}{uG&Z^wJ`!$U<)&1JR<`Kh7i$);T61SwrrA zP%->aa!wA}uyt{WOrW#M0Yo$f4vi2Gjxcke-2C;=6oosozy1bAQ?_<4O}yfePvbas z0NAQFnj4m1kik?nzNyPo!y!Qb7lHbnku-3u=}ln}%ydHmi-kkTLAlRYJ7d9C z0)IS5SlXd}vFR{4c2xJIMx-uqhEh{pv8^@|37GFC`_YHF`^g2&gopqRBs7}8OFZ;0 zD{*+G?Ba-~hpb6R-)|V}i&gG#PujX~dISAQ$SZFsO^YP`%K#)sd`*h{1HL%niwpQa zzY>%TeGqH$4`1K}{{jR8t9m;Y%;|1wwpX6p>FuvhsyMN@OhZU=<$(B`DHjcsm>%rC zx)#J4=GKLOZm%X30vpJtU^UOxSrF$EglLq{o?AG;w+*3k8pNb_(|c8~L4IX|8aK)Q z_c&(*Ejy+4?_)Wm9$?7YtBQ+MQda5HVrdyobX3)Df>FCh8$5;4AT{7TsHs}4M8t*2 z*QT+p$WktjNdC!jCZW&=#gV$m%dh3}wVqdINij3z)>IxdbwqC)Y0#6k9mU5!YXK!bx@WGPR&62^->VExr`{AM-W1MzgTpSF!g*d{iwDVITEX|z z^bFH#fJe=4Zpx|#FE-2tf1e(WDx_T43N0v}Dsz03iXnuKD8^L;k2CQdeRulArr`?L zU@E2}i8cbj-S@-(blv9EWL5vgH*?CjMwIaGHZ`_sltg&qjx0hz^>u{j0HnU5lG$(j zOO-5D=N4UeEDgK;!PWMLt)iQ|*BuOW+6kW2m<~{QYZ+_PEkMMgybUu{D7d$CsiQ#L z)Lhxa_os>Q$|md6Q!<2J*H_TQJDI}rbaUJUB4xn2OTCh&$yO>Qx&_Qu{Gs++V0uk!IxX9G*L3O)raOixVF zjL|FwATRLb+n?_Tksn>H4ENAo2eA=3H1(gH#I)Y@UTVclKU)&P5^i;89Xt~1doGnO z)ip>FGa%7*Ni{^o=Ar~Iwwg9a4E>D$_PrX4SFxe<>vNcT{Vl#1Ku8vNg2_5#JY5ZD zw<0zA*w1)6pFK|uVqe{PdmNzJ_f`Jh>1^`-U9E0!{Q`+8l(YhESN~xT1oKQ{&Ec0V z*x+)gT90Rg8vq}1AorDv7&UxQih+ti&_L>upg09JLu=D5#tjwhm?G@%u|zuOk0Q(K zfiy_~nGFkqmM_J|r&uJiw3QK?-6;#*4dviAe9h_ob#W+mcaP#tdlQSeq^?qwEf6YN zue_7HdU@Qs$;S1nHZb>)=UzIxiqq6k`T0HBxYc4+R~q_$BcT4U#3R>y*fYdUw*mH4 z?6;rBD_J!|HAp$}&Nfrz7 zc)Ro3ocixONB>am@j#UwCd^;Ei@Lu#ubWp(_x>unPNuxuUQI%0t z+DO7H?Zj<4a=GD;bLCI$gbc2GoOt>b?fy=2TlEzAmoQZ*Z=(4I0p;+bIHgS2&yC+) zq>FAnwMTr`x%&968{}vqSR{_&J%--7hZ3tvV2a=m{$dis%+0{@#|)84_`%EC?YL1H zenB=W&Y4@?8!#8421BorIDKC00U{%Gyxw;Kx27 z)aZs+a~>zTcT3y-Kq8ww&U_yQEIX+72k*}=;u+sUEpVaM6U9T|=x?uFJAwF~Vw9!X zG|amtp+)oeD2$l*7Ubz;+h1rjH}gkyUocrfN@9UGX~^MYlBm4sXcSFNm9ccXkaE4U z0ax#8=+k@HTf+HuV3Z9@Qdt4bt*4KFxsNVWGK~dQr+DZPBzKbx_*C~=n zNEOx3b||hK!)0cEz9UfDb=H>03G? z^i;J38cC|Q&1kf7X}Q__HdW|>*0fB%H1x##xAfLXhR06gr(!g>xU~HLg^~<*w=F}O z?G1d=uBxpQ-ezXU(eUk-=nvA7!wlcS>f}8n>Id-l4n9KkLfM>egUW~=eH|=i+%bKk z)NB#lLmMT-cr$sTv*56~dXaEd8d=WVM%@&pLkY)~*}P?fHrr1x!p&6&gFFSb;@wIR@dL+@JcFIIN(t zloL_A#tn{p$luthz_E6XL_+Vpsl?`RGB_#C_^nuXC70TRe61B;WbAZI`CpO zG6a!-2lY#vOomOgDuT(PO|;4S@LsP)ZSp)ddtK$?&vC`PAS1^k_@60-=?jarGR3zo zx_Xu@D$vtk?a=vNDC)iJYwtL_?Qpd};agYOH~aQhimM723D4gKpz+pj9w4yH#q$Gx z;=-tGKzoc zg^4qt_0*Qk2Z$i;@@cTxQSkQgv)QXK0+qVRSiCsxVAq7xtKXEIBlw;mpGn;tnxCJmdW~F@1s-8b#&qs9Ts`bfrTlK8tF6#* zg%bU|Hrkg($$(dsK}>MT0XmxeExn9voBjo?mEDY;HKI6Ur%zi5;*Uj2Bn(SMqew zPG{vOqb-s>7~NaL_q&YY{X?DaQIk*zt)k0=twhO;k^0%2`5{TV&y0FTw2^})LTcb; zgIo9hf?)QMq)AJa0=Mug6i3PBCmLQ3YSt#^5B0Hx_!nX!KV)9oS$uRsT?}k&G~EyM z>TPR21K?q`Ih}N&=CBNl%5ETeuj;@|5S%~JNJY@3%Kaf36Jcr1SF&hlf<|QtN79M0 zX+7GH*T?&9WKPTIkss#ASDX9fjMjhBSRR#ZRqGNZ4~?wta2-5&n!a;~X`3jGkI6Js ztfGu&^oogb-1M=!l)8a4aKN6_X6Y=ZTpK#Ip}BF_Y=+xRDWQJw;HAl5b4EoSgA12J zrdB@DsEo+Wi#U;LjH;zh90cC{8-FfHii(Re`caaNK2?&SVtPB?&m))>c6Z1JI>Z&J z?vUAoTmG>@8AExQZL7h+!Mwv6Q24IIZRFUAHH2Eqo-iQ8+!zNJA2bG~857PF;MSQn zUqH7l2$`qnV{vCXb6K>wrzAQHoo+_ZH=op}=5@wa^BtDVrMf&{S$uy1UM5AW*WTdJ zn2R>y*+Wya%naIet(p*FOFjyCsEv(FkPy!+hwk_!j}8Heu`vLV;rd$_2kk+fKBoLiIDv8y&|5`iz z_yt0Kt!dS`yTRu<14r*i83BE@OjjI#&&+87cRR}u_4`~U5~_AZnu=6M8U}PU1`__? zzv`U>^_=&$2c0n!+5v5K>=Ecf(|bP)Vw|V0L?o7kja4lU>(0`PL$wdK7#?+Ook}Ux zrD-a&pnCwWpE=`WyCpG8WG!?(K&f2mfQm#gy|30*Xen9jMp(kV`|Uk$W! zRu*csT2~=C8`+>tWP~1feHtPKd!g1hy4*MskqsiH%k#~5F{y?#7k{|9{+1Y$qa0k0 zWSoZ1)TKyv*k+ApPjffoayR~j6<^aNh95^lA3TWlUOxyyy9g3rt7z$kAP+aftY>hI2Y)KIp6dn8w~SA!-wdacB_6~HGeHOzs!br z9NRIW)}2t|CQ2y5dh`*Cm!+C#uH(6MXXwBYSkx&g$JC(+0gvB(AtJ#g^2iN3^9F5@ z3L7X)8+k)Mq}1Os?+^=-b$KoBBE(be5>D4}i+b#aGJZ$m?9ROkSvN%7p&6P6s05|L ztRN0VoVOq5)?Ga2&>{yS)!yNRfJb4^cN96xl69ijv@T@Jygjr!=^SOJOT}FjIb?{n z{6E54MPn9*r(L|6L91E-&L_+zk3Vrl!zI<6E~fLRKp?b&N8GndPOMhDJ0ubn8^$_w zA{ou7lBcZNrnl`XlfvH+hIA=}Euo^#cxj<`)L8BzNN7<#BLxWuYifDQ>TP<6(+BcW z02m0)`8nPsiq7acH(yHAwM%)uCS;LJ8_28XqQlbm0g|>;$wlyGFv@+NfW(RelYRj$ zcLcVVf*_cg*#T)B1Qg9?s%9(+qg65`?lA(064t(FKTdt~-=1e_tLn6%vV7muv&6>5 zC_&CB!ELZEOCLrOC#Ws98`Di8INGDLQv)?1(6CP7IGO&nP&|E9@gv45g#iRoOO8J( zDEOxEJA<>qIG0({$%h2ER>w<#HaPt)=7r=zx5%D#{_;5F#V6hoxI3JrTn&K*s;4{0 zanOYePyk+n4xMJqx+u*U3;Tlpy%K*W`NNB{H-aIG;+vSZC*P}jMicTRlDL@QI;sXf zav37t*NlFra6~Jm`M2 zb>)Kazvt43KZEAf4vl2LwT$c#U6>ZGImj+|O1oW7>gR00>Ii8!ab3eEWg+bt_d^D` zA8jO6@Cjs8Y7Rg%_r6pwPuZXjq*O#YFUzjr3YoRXJi2LpJP?k3I@D0CVM z&xwX|dMkFDn*(bnn#^nhwrdR|d$$9v{QJ*8Gqy}p(8hCj zXvEi%8RfDDgBC7(WQpr8y2s_oqbPrhtM1P}<@?ltE&lu_<()YPoW;L)o+cXBR89gH z2ElBU@DvwaVSac?!<4>dp4*91Q_crD+23Qm=%^@dnafEWKhXtEj<3)lte^gIR+R+F z6rzs`=+$j5G*pB5^)NfVYN!UZ437_l-aX9qf0kZSXrWp}zY+XUX5Q|LKSiyOEqZpV zW(0>Q4J2`*Asf;_N~aBYp;tW>-g4)CrOrv zUl057?~}+h1u=#?i-2?+JVFqsoYg$^j3!=CQ%`Q?S9Lc!@VM?Qv3gAJSQDhX;1l8S zCG2CxlSvVlI~!F=d#9#oKMu0bjn)UW;h0~fJL2xLaJ1T;C7kI$Xq zU?aq|Swq{h*o+^>P_1f9kvRoVlOR(1fCkH|#izX`fDypEmX%Csee`oCCQVbqcg8=q z)D3B=s!sY493_ie{l(%37%Q zdpir25SjM_`1n892z+rMu6FZ_2lS;A2FEAnwG(8q1tVgc z*`AtAfU!32D-?7|{QIr=-i3Yh9Ich=Pq7shB zRcNih&(ih19Y!(V3dx>kxQk5L=owMHA-;akyEI*yvk<;K3=qyGR(FiO3BJ7j^|_fMw5xu+Y*jU_!wjMYAGLiY;L@)y#wrnjY<4Ya^F@(rIB{KKRnol=p1@JhyMO$@J3{D8HI|jItUazj zCmbE`(ZZryjS+7spps7Zpk}xvZ>qvj< zE~aLO(gnSRgdvreh544wF#~M^rOk@g*rPAM@(OuX_lm{y3ZrC;P!*H6{*Eg{8C6$m zqvmawt+B?|D^)$RCarWWqD*Q~`4VyWGZlztpVq=&`lK!std{RDl%PP5Zl37j>8n3~ z_pasG-s0Jk%ZzU{ajxVoRJ1A%5cFHy*?mO3=GR>W zdjvUQD{EuHmk{ZY>X@Crs)uCV{1d&wsVw<%`LST8h5(JWzwYA{9Hop}6H3>XjJOPh zcv9s?oKH#Sn7#Vx7{wLuom{ZbIRmYhvu5AtL{cd#acWa=-~(zz`mLrDv`VZ8n{kde zY+|c^q@VNq%Ka4XnlLJ`v57{V?Ati!_P2ml(e>3jW$iXSwC)I5MCP9) zG#A2$;>Ue-;-dJssk^z7|2U(g@(BY{k7P_5%Bco@Xhwrr(prZ*f6M#jevxP*-1wP0 zG<^{+dy^Gv1^4$nTXagrXF@b+)AO5M=98kK_a)kIuujuwbh}V%;Gm#dd_5k`we9_& zpj5;$$SzyV3b;1)KqbWhO@OBB2>gymn-P-+r?kZtuUonJeS{5A zQ0MRR;)|r1LbwHV z9`nI^0AUB@^8pf*zMo8v zM=_IS;%!nS(Gi=+1~SN*-${d*;u_|r1e_m#4LTrJH(B6Z9SSR+P&cDJO4 z4H1{(f64N@-@!Oy>o32%%)h8fG=XyFjKxWZiV^6D*7fl;na*2#Cb?pfpw*Gj!ljo7 z544ko+gtowljZ5r=VKdkQ3R+2PC&xd5W{K_X%~3+S$Wnl{>6$wY4t}IRIvG-0yewR z`WILijbSD{k$ijC#OO?551y0v+4NUE{j_`vx%L#9&~it^%)U3P6n#eZKaEv_FnXg? z_Y3`D?Scu&1+&9%HrY^&iH6L41m-ipvZZU(ji$$ZjntJ3b`pO6l}~=)XB-40TI&%% z@30+zl7qw4i!Ygm{NmQ4g6hd5PN=#2cSxR1U#cQg0yMIY#2-o4NX-wivRyNv$-u5J z4j9x%>#fXP{7GmaQ8xMi`aenb+mwD#a6ipP%K5rXre``&1w2Eb_~9uPt+zN(<-#(D zP|{ANKku#S&_uNhkI>wRd&Z`&NoDr3Rd;7v?m1)rgx@&vKuKlel^uERLTC)vGsN8^ zSPFR2rrNW$+u1GI4DkZv6S>io9D0{t^>NF15`Qo>wxzo`&Y|Rv%MeS#&5d{W>I7z@#CXo2j%M<4-QUc_4BFu~a~SETM;z}sScCZ& zSgc-}XlM|94txSwBg$V>C?`NO*aS-N3M{JzJAA5+1w`At?(rmx;$|r#wH) za8NBC+q#)K);Qb)(W$a&yJ#?3XdF3JrTje0Cndftf8o#ANyO!+nrW&qI z)F!>Tr577I;wC~Su6Jtf-Oi!`=M)}6+k(=!-uNSOrxn+@EdSj%Clvb@i$4k=iON{~ zts`w>XR0By<1ZOk?R+YB;S5hUL9o5i>}?99cY;dm-*#oTV_p;I?m&f$IbYgp@a`JP zZY(_%!hcN`_m+9Nr;zS^(;R55IWWN6dI?CFojKVP!j~K1ZFVNE{_OV$f*muAU#efl zLytE_B+Sm8?5hIllHj#GmG9jmN8^5Ee(!RYMvOfbkjQ$kVqZ{jN4}0uqe|Ij=QR@# zDus^axwu!}T*|F{L_xc&7-o%wWF%~nYS+iLc3oSe^vM^^jBnXRE}y&ta#0od9EKhfGDGbRN$=yJulCPh_Oh?EBoK3FCPI$eZBNuhU5TH zy~jS!rZs(T0pdzcHI#maRm4wNSbkFE79(~g41eK;>L%~K7T;bvC55S$mQ==s0idn> zVLFbGiMFJ@Fi>yY6GCnzr|YNquwCJJts$F?i#tCut2o_iQNG|_`s*=0a`1ysE<;}y zb6}ElVbzax@MW#zWo#Jgb0yy*cfDsmc=2)RoC~hVmhRG6B@gN!*4Gcd#e!<|1xCe# z9`BzM6_uq{Q8?VR1#lv*^%r5nq}Q@5S|%@D)d?r*T3D(l8XXC}r%btFXxo=3YF+LI z{fe~q91p#M<_h;ruP^JW$4y?a&Y5L+p?kCw#3oxR`F@5<-ANcTVe6RrkYsBuw8Fe} znNyhc`AE^HHCe;u6-(J)HnCJUapPW0BtICl34RH(L+t<5{c=Z$Bh7?}5TZH*u!_D@ zys6GTRPb9~)TPt-zjEBQgcG2DSal}4J>FT{WT2nD%EzXs(sMv&dX#IcLpYD7?tXh zAWPJumG1GU1K?HzyN)$CUWZ32+q_R48)VY&elm-uKK*cTQ~2}1dfL&RY5w6t0lR&k zV6!&8kGoE9#c(`B5>x;FdK7Bvf-&24Nl5#%=-O+a95Lcc`L8m)XyT;VLrTjfVHEq| ztM`=p8dI4vlAE=oj9q1R};3 zcefVT5iVskbs_0^8uNdK4$MqgBOzQ8vIvU+Wpz<$mdbG~jE;^{Lo~*A{?J}hLh)_F zXJwke}+oEXCa`j=`rjs-zJ4RzPQ}yVC8&myZh0YuasSkIA)PjX6I>K^ysfE}f zqQVMGo3Ac7s9B?(bsZ{IncoSGW#rm3as>CurvjnZYeKx|5+pXS91VZsV5vjvkKc(} zy(dI~pEj}8ZOk!?1=lSO2gdvuX!`8=3)I5?u*njpQSBQBn8QbyXnd4Erne6zpg7J$ zt>sU5L0Q2>18AkIVTM?0l0k&~3nuRkF%tujsK9tH&yIzZiiQfx$q4P>8Icgi6mV0J zx4H%oiHUNkluCF)D{=Y8Pmg}ZtI2L)k&%M-^Dd=H5x)@7Fgf1Hcdho_$J>u*IfP^~ z+{l1eN|ViRe%VPx3vEho?57cSj&OTNqPEZC;Uk%?l{^zB`Q3Yc6wekT{SE*5W}>Q`u6gn(I*Mkfo=tRIW3Gv=y&cM%H(Mlz(+_| z&+Uzzl{G^n_DFkqY^iDy8;fJRP0UD&HnaMS&s&(>whizh{-az~fyI^orga1GfMWTT zOg(NynI!D~i)5&x1JxxVVe(Oy+~YVfb{OiWmKx^XEJuEqpJ z;8Fo{cX43vbS@Q>;+4WV9BUXEcjn3G|Kj}%MG|9oar_A6-!W#S%2-^1 z66`sug7vbpLy2iOySL+ z${V|Bk+6R2%b@}^z^8v4$4Co=?K>Sb|aGA7$!aIxsv82-yBj)wrl zMolzoLB&kvhE&*nYFl4Zf2k_No%CVs04TN+0bUj4rQ4^>PiyTyb)lc!cmuvwH7CvY zsV1sM{rHamBIZ78k(La*Kj3;Q?lTpw^cb608i()FQX_QrlVy@77hZPMzoMGlH7fU_F?C|l#Lnrt?(;XRbARk%x{ua7 z`2A9!w(&z`gcJv!bzBwLsPB4xw^!&n=#K5h2@Wj#IsLb~2sB)qcM4cZKaI*=t_`vE zKdX4%mG)l%a^q}76tXJkBjOO5WrC0gkP}4G zZDyL@SVgXKz>(RU?tB>i9%l(r@l3K@EV5jfLoYcXC%LR(zjS(kJYU`(^wPnjVY~(# zdAcDK4J*8Oa6|^^ph!K*FcVrg57bLLq5{xdy|03NDkY*tWBVZm8^76C%&1)Z(V9uZ z=Uh8b`31Joi>JG#Edk6ap@C>nP8acEV|ZM^?Yn@fw=?P^ND9nl zFOAuQvHTwm(irQth?iAF{_=@zolGT3evnm|j~F2Z*{9!%<6g&Kx715VAy&+NWAP1Y z=#ukK2ugE5E*z`TXrE{FiX`u|AI9@VRgW3IH&cm7875YEb9oW*{Mp_bBVl+) zl@c>Jgl+NSCLx;=y0~d;_;V02gKdnjUll}Q(iN9HLK5#wHSHWh@>~HTBdcI_8cLII z=ELCk+LL+7u?)x2xOmH{7WJ0Vg-7~zV%Y^148=rl6|n_1MjRErej!=dU|DafXs>vV z0@~@Vy3yM72ZWSFUpea{wDGkV(YTgAk_&b;`yg_J1u4{w;#jzpew;1p%c{#e99p<> zxXlOH^fqo4eI1))<>cdo63Onc*^?^XDswRzQ6%K5oa~Y)N6tP8+mr75%TrEK4_ErV zD34#Qh$Ru(&z<0?yLhm7BGI&TyZADGzeLai{biQ>Z%wMKD5v^ZZJZ|YXUfNe?}QwR zGX-t)O2UTj69qKiZ)~YEzIiq=2x#Iiif_$wZbm5+z|AuGOE?`$)_*s0F(6Ofxalaw*8#crBwx7p*%ny_rbu$tFD%=6}Z%UwnZwr_l2b1Zjp{?HV{aYu^I+GEXGIo&qBwWD*S0+=-Pth#4G zv81A_uKVB&XJn^z1;H)HQv=m%h(RmEv@T-t7Z?0gChN7h#3!(rJNM?@$WwDS5P#f~ zeZN=22;~KjJ`Mn{us%bs@0}IU{mw&AC=~^p#^$OS%*0Ob6B%eegJFXG_I_zaI__#{ z?pAaQ;+1bIsj9%14#KwBabe#<-y8(tzH{8O&Ld=aa`9hhz23Cp*zV04IlRxtssM=E zz(#D({xk;7Fu$MD|6aI9bNa@Q{}Ak({wQcw6}T^J1ZD*b&wnKrzDIAu3U$X1;ZlOx za*N3-u7sB>L4oWisJc~cuiTt`+eQc{n$Y9g!wcEkBCyB??_~%(%eM8cST0Jx#G7Jn zLhUMP96;LS)K5DdV>U{&ZV%v~F>>&_w4D3rgw}&0*UNDasDW{ph%J=hSlq9chVj<% z1dbhMz8(Yx7lG-ta&@o#)psWdusaee!6Jt&IL{cd)J)Y|dR&#*VvD+XWwY_ZL^Rja z{++M);g*6eb$n>r%FV<2{1PuX6ho^=ee|6$(A7K(_5|P`g4zz)4>55>lq_=Y-no~Rva4P@FFO6sjLorc!E=!1AKU%r0~wM#$M=33)(A5rePT<5TL|&>a`BR_rapeEZ8-SeN1CgIym^Yu&>+t?n~}e~x!c zg#y)g&!@z{DSaZe_jDep^7{sXxvw%dc-cIeextq{l@tT_fcie%`~<<#AsMj^&3M?G zZ0)}?2XqH{T{2bQn}t^ZXnMiBAbUS6V}y=Fve@`c2XfCv?G6QbrZwcEMOF3+MGGp~ zbCWrD3}8GHks`TZXQQUhYJ>2xF!O}97+!Vj+SJ<%tBxSwW9p`LELa;M?|AYq_`nTE z(e@(u0_;j(L9*vnd%J@XmjoHW_GC&j?$(BL~nF6Q!tQ($_8nd$i z(*rPg>H~+AM&NeW(;`Q0Yci!*rCE@qtOH())CETzF}|+~`<4roCy@CsYR0jD(l) zfNRP4-@u-uBAJS|m@Ok{cq!d{%QC;2damnjGsC4u&m}O@o1mTjwZzUST&PwC@EJ={ zy-PQ>H>`5}J^H@P3kJ*E)U22@aIc(pYGkBD`44)r$d)gUv6YiL=r{e@I$?dXpVH$A zg>or&8ie%2<>cA!(}%kp*qO&6pk#Rm=zvb;??f;-S4$sJ^~qN;4mbJX+Cj?R$*0Ja^tTFjL|g@618sx=sx5!La9o#)pu`?)EhDzGoFd1M$= zmHg^g^-L-ejiE9JbS_94m%u;O_Mr`jiIGIYhOPIII~zS=wBn&Ste=O=KNM>0hUkYv z(e8g-(f`SM26BPV9$S_t=4dKN+harsh=j72$O~ zUsfB%!gL;)%{O_(A9MKO*{MTAO$VRP`=o zWpJ=B>UU-FcstYkF6I3oPoK^ z3u2Yt^z*uEzghGk6%H-^wr|Uz8C)yyw5{{HKBB1iYWXzMY~}^HgE-CDBH%gR0KdrH zIQ^wf2I3$hT*9$=?UGyB1)kE$@2z=q8R9LD`T4lOh~4@yz6e_n<~}fzFon?!r~Id6 zD}1D5jIbGI{u5=y@Z%S7g(N~B%L9sxAs<ARCG{i@Ls@ z0QDSgPjnq)#lggMqgV{Ww4mrT5E730ZI*s+pG#^mj$Wbbeo|{DE{JuFs(>M60^mw{ zDBOZLFmWhaK`lX{_cj+;w(d?Ou&r&maU@OG7CPh*YUk*y@?5QA+O%g$O_X;-A0b)$ zOkTWRWykW~H#;R9!#id3<*u8Ng!UMgVvin&|8gM>v2=ZZGuXKzn7FmrELg?GKUKyK z#3X&FkFbCO(4E&kHSL2$^z5VZELxhEG(#;DeN02!N8Iq1817V~NQ1z~*Rz{w)WKhj(l5j3H>ArsW z!cGSyx~S8jP~=h0(mO1>v_b=(R<#* zURme8CS3TO`6yL$=7Ll8ID}O<+j^Ob`tk=(>&`AfJUg_q=Y7g+9MD*~u3&ZX3D}MH zS-4-NE*2)|2i}tYB~aV~%$yTMJA4|?q#_D{R6=GQ@-TvJZ{rFUcQG;bEyc|eovFUl zqOKd)$4S>1zxH2ofAiQEZ)CzQK#~n#tnYNzFT z0^g98pj@B9zCx2b1-Nwg7=Q*20BVeV3biHRnAdrI5sqHT;c+23$$_+;;ulH)&aKVo z%<`}8EPL7E$faRG2YmR0cE~IoPMd5-w6mOTIvVA~K`etWp86L-0!3gqK&Xw=%zkx0 zvKj(VJ4&q=-QiHPI>~EE1@}U$FuokPoy?m{{smb6H#eC}3@m;w9Eee45n>cgrNJIZ zV4a*6i|(1srLgiRpUK}-aA9y*>B7>KmLWME>Az67zXuJsQ7iso;bqONpdrHo3OSFX zVQ?J7gBG!#Mmj{&&vCf_{JAIw$dY~AGvU2K zy!R!v+O*cemJ*v~wiyUKnRH1n85T`{5ezqRvnxa~nu%aqzotG|7uuqE^ZxZ?Mtmy> z>?ub?@64}Fl@xU@z9;lSRbOS~lVQirUh50O4dV`@jxNQ^;gR!g4GBbAESiS4zBJQ^ zP%3N-E-Gl(Up8U}Qw$fLMk#I)Q8J_Y!z z^{J>0Sk8BqFA;K;zd~)IW$V?Sy=RFg`bIb^c!3EQ7#D+ z`AfF2R*MlXp%zR+Edym^kpq#n6uhqSPKFoRxM9XpsTizY`Xk9qvh>JAPsooID?f$W z+@3uX{oUh{zPTon0{Gj`FT`uAeDHi=pXl7v2;mYDE>HiJ`>rR05LU-OyN%09N@)hd z%xtMk9%|N`k<&CL7zE{d$(ys|aC&j+3XKV|3ar!BT9>4!pjbZeUj-jC|-ys&cx@EP;O0m57)1`+B z2I}#2VauisdQ|8U&EE`r-`LdKT*i)mp|%m82+Uro@3%=$K$;?n<`RYK1>Rkgr6H{s zH!=I=U%K6l$q0zD^0k?XI!$Akp|TB=zmZQ%adZorm0ZAVpAh_(et{9)8a4C9S*!PP zHxzHBy6XXiG&m-PMwW{-a9g=pat@dA0!t;NRRCC|BM@e|7}lQY86 z37|c-c1V`4l(bmvnRK5=x$8E~$*JWk@COx3hFHs<@|{?Fv9?1)$j7%#kdC+P9HjFrX<9N?BJ+&XM~J)W;eRbl7ve3?yCr7@3#eM0tj?knaU z7)^T-n-8xeVfB~=*47@Psdb}G`Y~ARWwLx_?&o)}XbD%)b{26e${sMd#?)1TR(ao= zoyR^d&Uu(3Qb1&PdHA|MmP0w--F5Jdu0XRN7s)Rmp%lEBf)YF)qVz}hXHY)Cd z55T!+ok${m44MN}sE#rWwp_A7`qAKxcoJbYCC7mz9N$<)OW_KoE8KLsXxWB>KV9^X z{r~-~doscNufVT9(EQ?8eCp$rXE2p4Qhjoyc^lEfDZrSyy;LlF@~xM_^j%7cR5d9^ zX&cA&s}VVZO44}FT;STF%@Sy~81pqUPM$(yW}ktI;c*Z(Dv{>_iP=n`XnLYqIaT~{ z&A{_Coq|U^e4&co9`d0Vx3=P@#b7P#7)3iQRo}b*`E?K`j|T3CBVdH$FG|Z@5FZ&P zc^8RPMxS;etS~%1Ds@NU$}{V^gR;TDb6_vO{68BhIK}DY6lB_# z*;K=%=_;9cNU{U^wBVnfHx9v9ZRfK3-WF@l4zm_lKF* zPrUFvrLj29wsHKBpN&F;47>A^JA<|^bqZl& z;XxsZ92H}qXI*hv%Ez1>%dJUScdaPK;J#nDFU=?-H~mDrOi_-j&`*}K039UxJuad* zmte7($5t(c(4yI>{KE%Y!rwLA*zqX+zo5p5K@aH~=Er_>JWW`;%>)9i` zE!CL+Z!;JNOOp^+AdJfbA=uINThj1hMou^=ZdAIPgNo4c<&f||Jxq<(V6T{AsT2#D z+Nn8;BCM_gsB8*MJ-^@99Dx1M8-zbig|6+npJfFAO$f#W8Q*9u^4oJawr7^`nv@cr zhZ-SYL4||N+}WRVW_liIl_SRiyxH@@1h1MPVV((*d9cg4Wo$cTQl@$U!+=GDoH@fxgTQr_)TM}VfS?QM0AJTy*+ zz)o^}9PPpl|Exk#yS+A1NT^pXM5VrR?15!#ELH;x5D zyn^5F)el0f7E8P57P!Xv?5-Bj!_pK5!Q zQC1yB|7YIp1C%~ay@OYi1G4%!()p$Ggpa9Xd6yg%Op&*D>`rFh-bBcdlXy4gSBgr+ zdIgl41%228B#a8HgK~D2zT*$6eGiL>5~eyR9OD{Sn>FB(BWl;SbUT_&caf!JrH1>o*jKaw&%md(Iq8+!3$R5~<;Y)y^X z?b-|OG=B4Fu4AK>3_{#`>&Z|1d1(^7=)3d@&{D!Qyld#MqZZ7|x7<`<4tzq)^ySLe ztWDH2p`GI*ug#QbLrXq~z#?CeBz&cGi0jSF_{hgnD%;+&oBv4T>i~`n=gRklh`zSh zMIdfeOAF5ZWiS0vNf-JF!=IT*G!OF_lU-O?m|-`z$HqcPtOWf}m{)}O6GdvE`$$64 zMAbOoF(nqE7xPapk-9D+WB`I+NE1ft1a>aULmvo7sgbS>KcN$R{d9wP>|RELvN}Y_ zOGDz1gmXGy{}rP((nqkf(--y*yA7lyJjuDcV9=H!GuqpVn_$YKlMH*3Nb)`vD4RsR#3QD8Yu^UDV z$tW~Cz9Qj$Iren%|3g0AS_5W(a?j4(%rS~*%M+{^p;^iiG<^-pb8 zWft9!3y)U~!?5lzBlvLkKq0$Dykf9S(EMlp7(%syZ?sTjL@xpSf5VNLw~zBaBYB>` zw`sXLZl5jrWBHcX-PUPQVlM&C-y?oPp4KJ7k|{9;>uy5rIrhLTXTa&logM0VUU_RX zPkx+iBL}p;`Y%F_6F2|RWoR(8G7uSP3i)~UMiVVTDj2n3ZtpQCko1u(KD5kHt`~wf zzwnwG8`LBe6W$l5|8I5zTJZz!$Ac}m?@;MTK5g}O#vaUDI6Zi4rWm<7=V#`Ha=~O3 zN3RG#21506kLBe;cg@!M805$ii45nGyu{?pnw-fqaqA$5F$n|Y3`NGii-C>!MA<_S z9}W-)lN>Vjmn@=#Ac7!boLPGLK2kOP1d^y1n39gULl zFqHP2^YWOL>Il4o-Bki=idHIB5BoIqrCF*6q*DT3D;5FjT=L@rjrBf{*E?a2i{7{3cI4MH0^h6h|>FS9F?h17XwJGU{~R%(C1) zzdDWf@Eu~WR)he|P1QU4V@|M$9XGB*SR;a*Ne`;jUz|SwqF-VPs)@BC`>lDJX|t&g zTmG%ehC4weGr4hu15(PhvqLU^e%8m8#pcM^`^xb(|KG5n+?;T1+yVnek1+3R^eWx~ zLgbC;k4Y~%c@zc)?YbH7^Ez9cx)cw@qy}(EaO5>mvx|S$_Gqk~kCy|=4KJoe0S_HT z#hIX?ibMLHW5NR-gGC90=J|9j_Z?xbI%DofK@p<>2S#B)f`|LZ#=kT|32zMUd9e(! z@X*!pt>#%V$un+wU5(|e#r;3!z-{KH$*bS;;{S=-(+sgmBbDzUFu6WQLk=`~Mw-_E z6;U9y*T1^zY(1NF#G7ep5X-bo!pQ4vm0t|lXsmtY7m1(|P`kYMYUS%f|C<>rABiVd z1VWtAf_>3AuMsiyey6{Gx(3_Ex#t2$@iPS#g;?eI_(S){MZd6%F9Wx%lt{S5AAWD1 zEF0a$7jYTs;TU7q&)*vBKrIDl!KmHDmLcTc8e-5d3=sE4WHx^ePkDWmD>Eb@HdPiV z18Zud!bG*9QV^2X}~26VX*9P&b)k_ol8AW2s2986eaF zIOVzZnok5A-m+_)KQ_UiRUC47gjk?e3l3pYIro-pZg%BhZ_Vs^M9cKtZ||RB#0Emn z;l+r%?dA?nnmc>^=;IAsC9yzR{^EWP;^8lAwcN(3$Cp4E? z{;`Q&Y_D9MYr0FpX0vHw%$&E1kx}1|-(QT+M!-#>K@?~t7W4g5;GMzxwu*5+d+o5c zFWY$zD#&xHjFGmeDkgaKkFj8@%UK28ev(`su)PzX5n?q`IWzVf{Al!dROhduL0^Q~!78Ib*0BCt~3&r-<*U#>C+^>9P!gG~PeL!KW zs*XC>=u5%(KVa^+8t6wRyoutkUqjeI8E@9jZGmR=j*B=n$pxY7#p9nU@u+IYQETdq z-c0^%5{v%sFSqyS7$Z3&&Tq^OUf|m>+aT_fa8KbQo)|mp@Z#`Q{KeV!C+3#b?B~eU zve7RMiKJ9|F-OhD4#AsZ9kISt^qMfqoZvDWCuL(n;UpRdH6!-J@FjSV2O{p~G z|2EStmTebaDj`BMi%Ui^;f3cDK!zpbnDj|Ngq@ihwWJ=o2FO~s!x!E(!Tx_J^lh~a z4QY25pO-3VJ{*hVJ#QD*(Ea7<{rykKBHNmE`XGr@)i}tJi)q~NhmH2l)K67-@5o7p zJ#rW&)EbzXoNX3|a+_I_WTbiD1Tl+xx0_t3nBU-ZFTs|xV_p%&}RD#18 z!!@=f>*CNGKaN6ka;WqWKc9;T>}cSORfE5UK4E=(^3r(eeZ?Vq+Y^=?8W}2@oGR-z zoA0M|YVF3K$#S6IJ(C&ZgbLAdwIs{X&dB4621_%>5%(;xpQ&p+h}VAmCJ3_;^1`M! z)!V8Out742Vs$kb8Aqz0QQ7-xkoB2tqdFc=6e{1#mYHJK6E!XjFsoJ*Hx^X9qD?q* zf+z_)9K3|HfBTdLr|@z+DR7p3kIF-Wf~+H(-i)=4^F^aC^V_*m!W_240CMr)on>j} z$tuVDF}^(xt~<+$VP>Q9B=<}pZOw_4Ev#OW6 zm6$%dOW$W;i>1-Edo6;Cj#9DG&)h|ohYzK8CHh9yy$Hv+x(8V`eQ_C^BgfTJf@BwY z2)^HZ!|OY+V5J{kh$adt5v?c72f#e31t?yqU?4z9cH#$5s9TC8#FUpLJ?Q2>Kt1mK zGUq*1?Z8vts{9rL$1D@(GiArZbLxG&ah-HHT8fRKc>j4=eA8%`DH115{x~bd9?x_` zxdTP2cU}mYPTfpn;%66uQo;MOSYgFsU-HR}mDa8NNQp1O({k(i@vd?saOeI>A2wxF zgzx*;Jby??t?OF=?nwM`i6izP{P@ZeB^a&=3 zy?!-N#S;l6(K??n0-W;h3mNo=8UAvKFUnCZ88z4Cd-`vZmtFW4*X( zo9V4X4TVm6eKftP-t6iNvCS@hB{8p5I2DKv|d++5^1xUVaY;Qie z?k@vpP$E~*PJCfCJ|^Ia%wS+m)HO$CplS7kA#Uc+B(^=NILG8xTawF@y?*S><`HD50l*Su{yw?^+_ojd1OxdsqqR)uj z1eI*}F6((P;9-zPcP-87J6&=cAh&^QpKc5XzB7){D$G0v7#BhNX=CL|2}Wshs7FavOEsOo{p@k|*PTXfUeqy<-{NdD4mU>`>g zCo&FCmDhr6U;w4R_Ql(nSKPBcS(s=M5x<_h39h0~@f|C2ppi`bN;rw~K07ux7I0u> zeAT*VA{wN?k0u*~c)yMbsNVhRANaq*&*?g@4zT}M}ZBR3r;S&2%z|fw>3P07*0@)=h zH3~hqRa~tt84Z_*MW6Vkcdi!>I8jBc3rAQD8lq4nzP;4ctwW6iwR$MeZ2>d2% zEXN*%`gNmG|Fg=fB#fN?9*Umcl5FFoJIB7r_$2Fn+QMR%=;PQGU)zM9>L9&ugo7#1 z@_;F<0>n!_!3nr7^86$TwA`ovH=ehCUyRRbXl7hp@AgSq3PgU+itqWw0s%QB!9IkL zcdhF+mh1JgbH?^3%tR@|q(J+YrTv_`))~zz%+pS|FfT>0lm7O4y$I<9v zz~U6V2K$^f({Ulsoz@_>qBP&OpBC>P`cSX2SyC8vjSe7POfF(Ry=lomQU9H|)Z(tj z{O`*mbz(5@;q_j22^g^+6@lJ)f;z3KHt%G@hQsYGLXP%)+DJ7_uQPw0F*ih-*kCeCR92*D6n)YpX^>+ltR;7fn8kK*s3yt^%~*Hn+i z)W1`X=}teLzrQ;Btb~iv!CW3DA_zNk$U(PzD|j-?mBbJ{BW0y2y|RdHq0DhQGrFPh zqaj(PA^zZYZ{csZOyrj7SkBP(AC{Oug#Ad`UE(2-&%)R4=gECChJwUpSjr*dmw!3P zVM#J(@*bb-g{%IFH{Am$3(aCJ-siQ29ZW$DlICIb`=fRwRXQeeAwcj|1Kv_!g#qjaJH8td0ppy&NnJ~ zfjkx;A!MqxPP5~4-Xyv@|C!oN9hENg2;!5WPUL9T?lkcCW8WtR-sML=fMdSLw_Cks ztj3v6Un7}p?@+b!VM-)aR&-c@w|*+@oPPIjwP};}O_+Y;dS*hO?)rvcQz6MDc5hzC zKPfnkL7pK4+v-&?v~eFxqs`TkN(DpGf6OZ4X5hKxNz^u{!q??V85~;?Lr_&FvSq;% z1Gk{=#Y^s0jrJWDAtP17RyU>+E6RlW(pOGw-!J>=sxGC_zS*(h8DnOPOsz#H)Xl^` zi)T_uOEEuL{P(jWuYrvlr5y|zd-h?c&t9a?xV=$!2M)jE^cvDE{Sa(axq5wZmg|M3dmu9@Z-S%vr{&!&fe^`vKwz~a zaag5SR5rj^P3olarwk?j054rm%%2i|*HP$)>|Za^bAG2W&RjKJcXO8V3igvKz$L-R z^BewBccha1Fy-l{# ze#MoK*eUS^6}#dDYl&NhTj0qNL9E@bPYg7JQ(xVSmXcESSN@2uP&h~0?0Wl8%EUf5 z`xxE2j1{Tv;o0H*61(L&(F&1@tH*#fH@H&ujJ9x4u0Vru%-*QRL|@%D5w%{L4|pdy1FX;{={FbYU#lCnG*z5+p+P zf*UaBbqb{u&kt}f*cIK%4$k?8r)_vVQ>=K?om@WTyIu}8Z zvqX?0E%-tEX#^4ni-yJB`V|1RAl1ivB^Kp~9V9i8DO2*hABQ?V+fGYhDi@aD5RulD z?Jyg#Da%ps!DScf!6l9$dbHWX|Xs{fTVRB{NMOp~r?v8y}E znZBM(EcdG+x@$G(#RK36_)I3Mz8e~Xfw{MO)8-bGcKKNxYv z8`H*nLEtXRK#nK0F^2TU+Cblg%S9Y6C$3^Oo)u!YF>YSZqfivo-MyH2r)v6Gm=SgC zb;K@2^_u5c4Ps^-DBVJp&}C z*uU0!&1KKryO-!?;-*_nY5KOh%QP6H48o217Fvnp zJP#UurZz1Z^!;hr@siXGTI_h<$m)^rq&ofbia7uy{MU__{batcV??N2xXNe~IhctQ zslaoAy%bV9($m|VzoN(Cc|kj;i_0aY+ZB4WryOrjSnH#sHEsf4(ChY#)Qiv5_E)Ja zTDKDK(F|;7i#8BqWi(VdJ)2ptYWd1;nMj$=l*X*t<|1`@);@0P_{_54Ffk=a)$5<& zy6E(o?+)EzX_*+vN+(*4E{&aCQLA)B>ZbNnUhjZ>MGoNas~TE=E+QRjMC_xS0-M(iJ}Nogm!@Rq;J`FMQ}7EZXD7^Ps}kscw{ zgi)=sJR*)n3x9USJd@KQWb85NmZZAW+eU{!f~BqF(3cHq+iH<0%iOiu`i*`3H@hcF zwEo>*zZyjqAf$NW?RQjVe+}jmDNi-fxj5XS8%m4p%r5r*#y05DVY1jjwqjqA*MCDF zA8MR0ZUu=3%#RcSyM2lSiR_kP5GT%a-GnSY3kw5ta&aK)`j9$+7R|C5T~QncGe5} z-rkw$eqXNxwvcbXDQNlf7BzOqrT#U>P6}eZ0nfb|seE?>Q_PaAR{EAPjFKaANJ`{S z`nE^P9rb5!w*A8u@=SmF?Q>R~?VGQ!xQR3dGQ%h{F$i2LHfD!%9wnCzUt8!Xlbg)> zh{v!FO~|Ab%@f~q(yT^p7)GOrS)YOdscV-$#u;D;irs`IWJhBp0*A)(^dk{{^=SlP*V zguLbrT4n7UOFJft5`XHdhDwA;Ul|?XMxfkxNv^-EwLpmkJ_*lkQ7boV4hQvwh*SWL zTRY7cqIuPi=ywQu^X`W)YDr$8(1^R@plkXO4up9KnEwjIo^=>0N&p1%?bz_k7HaQ+oxSwfx zMd#hF$nNYY*YlXO>cR9|eDu}mD`$DRKORBE_2O?)821m=&`^-I7@E|wFa(~X>KJ)k z+qY`Nkk|fM+kDH@<|HPJJ@U9DkC;ADNQs?{;9uk2^w}0rOq43{4+f{cS~M~`?iXXt z+I}1$h8DoUCN2qqLyn@tIipc2+XD|!aYPMEikr{JjvwIG9n)ke*pRMT&^?rAG@y5t z6vqvN-29n1{atcsV24i6bg~V2&O}*;TsrewYiMTzlz`EkvcVuZpXD(0@!N-xMhZCj z%Kj)4z2ClCNm=f$cPfRpJp#i1Hr=c&{rmewnC;qhybbCb)Ys`HM`t#6mUN01#i5k1 zyj~Id`fwuvzQ&bZGCuvvbcwYj!XY!`$^BV&s=4W1wEP{iqfiWML@UA0$OsIVm^i`|l zQSGtSadbGbgv6gd3OX8Q`34clrFx&whY`^dp0nPl$}mxs)Us3274=d^Ch5eK!F5*b z!;fwA4J-F*x;7%f{Fh|2^P#&njX$i0i60=weLugWro%Fn_I|VhG;ePUyX9M9d6r#O zHZXebUtn*-Fec7DIv4+dt&s+@9((3PWeD-d zjTn9U)-?N}rt%RbwS##NdkSAJ96HTVANL0v6|cfuw+TPGnwYnEu`Y^}fGGh1`b6Il z)RVHKbZTMtXUjCpW`U@vJ>ugI?TH4hz!TW|vFPQU-n$Ii9a46?Bn>PTO-J%n)*N>yBb_WCQu1;Wi1@) zIO+8l9H$0xJJjC9bHO9X%&(NEnRU^mwEJ~@y`v=RL4J_+g2&pWx)Oph^5;wd zr51^ue_hb6sGj#AWh2hT*SttL+0))50$zU-BZ;#ssTqO#(ps_#A=q;txkZ!u-}cN~ zhBl9fiZ}8hmMD}k=zq9IUNVd{=&ssV_|uvbWp%-Sdwa8X*G!Ua;Nlf;Fo=FH9a2-G zW5~Sn2YzHE6>Vw>9rW?{_LkPLz*0Xt449Rl9}=>7h(Rs z{k%e4I29ftVLp}1`{EOeb=1(y7^Ydr6#yFgE5lymeKWePz~MgJ51@q%}lB7$@A0PLhb@14MVAtVyc-Pd!#_ZCZoVUJ^?9 zG_KCXLVsl|ZN2a9%q7$4h;eMJJ~GD1No?`Q>|I1hsvglQ$>1wU{{p;y`RNTKRyy#* z^EL@7Ta}jV@R?=y0MQ!X{sb3677#gh;qO4s%o|I(HXztiQgM2{V7?ZwNRd*poPb*} z2Pe$-jWoBwXWe*3$^joesyLs*j5ka#n@R>zcjHGEJ!=jBb;ODCR9WM4>8*~x;@Ri) z{D~3#75z?ZVUk>1k|TP4|8@JEn)946p72-ilx5%SfDrVEPi|ZGa|X|boWU~S9rykJ z+M({K_Mv+~>iBd|aQeuf;qms2H2XxHXiKan0*8$nx@LlBZm4_e0j1Gtte@CD7YBw* zFvjEpBoTxz9;VmH`{B10wH!_I59T&Rx^v+Xw-r{24v{loZL%T6)sTZ@s3>Qis!WBZkAA$C_JKg&9Reo>4TF_P$9xRX)vG26Z?(V-kyuWHmDpNlLiW zGgns6jzbjOGc5bpuTdp6hmP^0ZazCSF3WrcLh7DaAmi%vJJDy{v@!J+)8|3) zl`DiyzBWD}3aK?xRuJbISNRdqV~7lz@POLU3wEU#Rw35=*7EMcpruh!aw*#vM=UJ5 z+>xm*-F1Igzd(7}g}OlUP}bnhE&Z>y5QiZ9yzt6Xw9Dw)7PhWXzN^I{Tabdi6=b%u z?)4g$i6AhI%9=_Dp#smjE`L3*qFDPpjfxX2r>97sETK^bVs1tC1;LM4EVZELz?(_W zjm@m<#GVu^%wjbLstz)>h=Zx`GW8<~9{N=H^_+TFuUYug)pdw~nZDQ#w3b9UUyY-| zN9rwUPNsG$>FR5NJJyYZbzBCUmDC>&M8ZuThd2o6b>_ueuCpNu*DO^Z{M}|fh{@81 z_KP*Va(mUJK-*%#x_4*N@}zW9N04$>*k}cZ+12l_zII?BcDBG;8SQ*H^$_`OauFx_ zA4r>dN~7JvL~^gVn!*6hAAR5IUsXiFx>K)UFA{NyD>($f^$iUt8r4F2u}8w=(k?@P z^55M{10Px`5k#tKk6(6FsaUE0hyMf4Krz41{0$M-W>^zx9O08po`G1{csn5IK`l5A zQQ95K${bT^2eshXz-0@#7=+vc2oakP9ShHvnr9h)qp55GTiqU|9e;bWhtiRcZ@H!K z7&7>p=;oUI#jAno#Qv)n@>)}CXoSPr%*K}rFRFvYQA%~z8eccjOJf@#}(5p2;aY@`u3;fFaPRT<78W$ zC!^vOIhJY-8JK)n zFTg$w9xSE^-knG3z!oAfalU0I7DxV3esv{{7A=sgVQH`Zxh^!hgY37NpB_Q-(Za*i z9ItFKT(WX)+0jv-fAv(5G789O^InOU*Ch{*A&nu^Gx1VA*1&eTY&VIlP#lv#L#Efj zpd?m%sndfBrK{{{3fI1G1Psm;YtIy8rz5|Nd|P z>3{zHzy7}i-2e3-|I`07e!B5f{k#A6AOHTJ|HJ?I`~Up6@oSX1??H08i ze6jPUuHjeO4GAsg@N#SLvuCd4*xos0euNNL2!S4B9;fguxq)dnlP`h781j)h}& z!Bz+CqW}-_5_i9-<%5#wKoK`ktd>#q4VLlTFdT33CSz-u01md?eH+MP8{$|xI%FUY zG|>t?)q=wjzQw|K2HzFST)~I6;Bdrn$s0IUE3d@L3*MWW90j(?jE@TFf;7`rSeQ-; zjG#gUAFysm_?8*I1>k6J$wQu?aKvxv8z@$rK+}i&p>OT(a5Q&V*b|Ka2D*-=90t!q ztiJdW!}39;aNN!Mp0jhG7qa$o#2Xf@31T?uW*skHzxq6zvH$buJC@w(XAp4((O$1s zpBCMY4dFwi_3O0zHVncgJE#N4>AoQ{!q<-|)-Nii(_!0j&#T)~vVkM-YXeP(e3HqT z3dukrp&a1huE&#Z4~v6jMUTxK=HUm;$K~PPxGh%NxUt)HvKMvqIWGcrjfLL zpOx}0nZl`%1{88zK4hl29Vn#Vll4pxhuo7987OSfa2ti(lf6w82dc%J!(I6p1#?$I zzN-3q^XA`9(6<&02@oZZ8~b-;`pbk{pC`okaggQhq8=PR{x)v_StH2fm7{+=p!m5^ zXmL<7AbS)YzuNa&vA*oK%x5ty=-gdWhgN)~k5N9>eX@@PUg)fzZ4S=*(27F@CNn;9 zpFok9>nkg+Bm+JxpDIgU&$%q&VptAc;eMT;Gj`58==P!L8MR1yxmvVRkzpxssZQQr zn_S-)AcoMUip|lP*NKQr9|XqhEx3P6Z)UeHzXgaP)E=`rvk_lLa}+K;#3BuFkDA;a5!nM|%g3KbXn7UdKUZX@o$Yb-KPwA&&A%t%JG>z>&_hlC3x# z6uim?j=16gZCI*~Xs8ZLSL>hd?a)ZtVi?&G$Fs%pqCgvOxZ&~? zgd>LM2tj}gO=){Fc`i=r(IR&M&9k@tTukc5my{%U2fsdYKRPXYkLv)LG+h5 ztDY!gr!Mw=m8SDf*RutBI$SBh$e-P#`4`vYl|nh5T6M0HKIl&L-@ICnZBkU(f|^#EUY>L5nryctiTe`-=GC`0O|H*-f{=qn|N8)g|O6kTe8lWI_tsM$C8j< z)NyjzTR2+P$gt>%F0@DdW2J_w9@Rv$j1>vCOy>8fO@kw$o* z$M?Q)**O5wj&5}JalltV1k_L?Q_))CJr!@odu3Y$hP+=F<;4fYE71a!P$P?}b#G28 zzf93xSv-MJZfFUqt|nbf7VId7^S$x;L4hL4*~=@oww6 zO#$PW6H^5!qnsTKDUKLkDg{Bz+tHa-909z{s}uWgYbAc5@+giFUOEMGzU**x@S9AS z4UF43&@(~F4ik5D_L>aC@pu*NyIfV{pVbf`WV+ZwHTE;2+$wecg4)mzC~ zm)m&^A0oru+T7_r2tXxnA3S}%h@HCFFUO0Xce<4u#}KidCg5gK(RkZ>eCmWiIiFg2 z8sw~SvZ>~M9LERQ9HrAQ{Tak+=h}`Y>y9dRh}hdl%Rm$Te1o5l<531Ar_(73cUFD! z?5zM4a#yZOe+IG|M=m!l$fto+0HofOcAGwTpRg(=+_m>VzP$+%e=0voCIh(^-O9PjkLz(`uSYeckgC>>B)EuuVLJU2p|uFL!u!y>0= zLY!QX5kUfaGYZ_J>Y530)`?anGAxH)Zqv&(mQ`5N0Uy**?@!sjIwkq#w99fXhNa(@ zrZbMtmU?YtdAyG8k9zrJ*=RK*!;%j7mpLnx>jMJ}Q78G=1D*V3e{y-5khl~=aOATJ z@$g)i=K@4mC-)F?h4&DA4-1!>6A*7;fZxpjUeOTHLY>S-KS;OY+pFCx)!K(qLwtY# zzP$Kwcx71)fJj6abWF-i&s`}zfuTnSLVR}7Z6G8A5c!55RBsGKjCXCRwv3%Yk^82H zT_Kio!wB9B1kr9=Ms;CO(tYWZ9wC%`(`>zG1f&I2cGTo}t#TB$b?&rQ07KD(?lz9) zmQHoBSyeW0#1#j4&vhxoQ9RYT&pIT4g3O`U>VV;3;A^HZBItIno;`)tVdT~NtADyB z_YDPTcCU`Z@6{2_Yux~`+BfTjbyAmtm+^;#har`yg5R6o1@O)o04?IQ>`!@LA=!s z80$Bc!*NF?+~W?B5&JYm03;p<61l^*(>eMxkoCjLXFYD@U)2y9-d0JPp7Y_F$ydNm zT_o^P9rw77>(xU<&EX2b(eGM{PmO>yw;;Ex+{hiI?hvu2{Qx)xbfDhltAb}U+*OP- zB;|0%9)mcL$jsN3)E=cC@LBO?p6AjCz){2D%*4Si43TOfqyQN4o`lt<4+2DQS(#t< zQ2~y8PwH*@UV@|Dviz9#0XW3kZ^+g8{_}d9C&Q^|g;I(=_ z&no&z-q;}$v~2W)G0_5|g5@l&_ctIpt-{Bfd_Y#+6;7OtT0MLI>fqAih__E63U=gF0*f*;7W8 zm#MicekxTO49k$+Qi*?X_eaLxB z?~btE1p`UvfjG*kZjIKt?tfSU>htdDbm)$#-ZMo3UUB=bD!y5Vqnhg0XPpB0rrMe4 zvEp!KCcQ!&8qVNYZNm}H`@ATX0FHD%csQbY?;AK)>(G50mk@AQmN@z^O=f&l5h$aa zPOT(3y7xn*INIsJAt5<%SSVM3BZo7);#M5uz#$MvX{Vi4<`Hm+jPR%AyDI%Oj_9xt zlbLiJfl`nAUB`V}ojz9+h#!@$dH-Npd#Qv#IqrQUkAy>Hd{&x3U0ds23-n7R07?tz z4c;*YW-~{lkkSN-sVCcD-{pgOEj2_&h0bv3=>$G$Y*jCeVP548X-v9 z@hpX#yI4QNzyWxy*6+$=O^pC1iyXN9WT`%F1W*oLZpz4A-nZ_5Tkyv12P=|kB@G~{ zcV!nZrR+nA;kF#g%z`^W67R~C&Jt_;3AD#>Paef`UW~0FthX>JPtz?g z1u-2Lfzr<>Tt4P^hDCrR9(otaFVl2pCK328xQcZD^U5#NzvhAwlycX&XfaVG0x0Mf z0&rii`!91|3`@Uj+ktMw`X_{EWtVR!!ogF~(4v2FKg_EY3V^iZ`f!B8&>@Wc4kLfQeB4n1#)P_ zZ7~nW7Il*uDLlb(zA-*JUO}T!9OqlLq9dBeE1K`Ww#}o$XWM=yI-+^Z7|2^p{kf$( z0(zWtRR!SCE6BM7R38miU9FdW689U?Z87fkY`e%$XyN8)ZW=5-ZJ9;P18c;445+e<41%5mqL z98b_{j#pIxj(pb|{ZfhS8+>oX;G4t!I`ZCR#gwW77@fc<9ENhgHAHgw8OHKqNjSbU zMEQ3$MAX7a1~}wQJr!T3f2KwVl5##lahQ6x z@ASb4jNUXZT2Ry+0g`;kb;aG8m(ePSWay{ zTd?TYWRh%G@^hJ=8{AHHwfgum6hf12ueS_iq4%ZW@S+5I?zuA z^jsj0Lk*|t^{Ofhgi`Lx4CTm>w0P6xJ!b?&^YJeEl4@wT2 zE=3CCO+M?Hu_sTLjdhoU8Fnr2NZ_A;R*pA@Boqd6Sh;%C;V|?x&vhh#gIRfXsKXHq zQ-(0=@iQ>~o{q&KtTo;<-eM<4}|4V(FfyS(yj8B1lZyp(11j;t1#>7)UuC z3B?i6#R585P_C`9M6r4--4W6yGaxy<#r6IG#DQa$>Lmgo^*9jaF=U90`U3%p=Wp#f zw#=pZj!+W75pP=APK6L4$9->f&?a*v)cR1004VvUWqPJS+Hq^o{OiiIoU-D3A4os% ze;ol)txQKiV8g5k?W=`67T61^>( zG85q%02H|?18h1$K+f#A=+^0((uoGkE+j06i?8V0b0m-)J@W&~eY zj%U8G*SX;7i3t+DX>hd2s1*f=1|%qFV~J%IBEs7S7Ecf`z2R@IhnLfl3~fm z4|RFjNTVX{b$uVpZTnQL3}#SHkHt94uIu{()K?*UhRheS?tdrAa_IxWsHf**eEi+z zx&ZH0!CZ``wj0{WFF&AMhE7oE(aRBDiu;O*fbgoB7)ROrre3e(ujG;7s7I_LzxY;q zC0u~+s$?`KDIMZ-vX56?0${XoPxGkt+Jd-^(@#)>Ty?lyaVW132l90aMV&_UFHpZPY+vY-}OB?-WH@&5MTqE zv`r8T`QtcUXENbetpEhDYzImc-H$beW-O=(h&j+QB8cOG&*uE+{vFzlC;OdCr zDi8#)Y!!!5cpB)eqr7JTf?Op4E43CFjtoTe28?fJ(cTg9e&}a(L~ganUG{f0))3By z3w6Y8trP??@8&UYN95Ldd1U|Hwgx?(MLAmgP3C7D-?RaOcXq@*N5`_sj0~g!5bcPc zT46ZCca9q{)^Cb6#=86zhcQaMU)mx-QIDhGzP60g;ztzgCnaZHZRS2|hzvJt zO*LLD4Uqu>!FaM_^*u?t z05Ed6WfeYcqXHQ5mJHi;xCDmYveuZk0jdqM!SjPu;nW7GHu8O0k(uXq0HxoQ_mrP; ztY22SDK%o5ZU>}7k$W<@0%4SwQeFshY&uLeEnSHnvLV)z63h^;om)qJOlc=3=L4EJ8Kzi{B z;j(f-Xg%)JO`s-uGu3;=!U|L&ge2V?gR;vfFP6DinniE`CP+FwRpEOgyizPc1F;^T zfDfQJNx3U~2dv!VCZB($W%N1^RqSh{-|vg+?Pm;&CR)h%EIxWdx@e)^HaYCdpgh^% z`7ey%y+9P{3<30d3DpH6xh-kZBSg~gnXLEBaP)F|mtS_&wAosx8-dZ@azE?Yt)}eY zu(B{5J-p|f*)vW> z4g^R(4y18^HAF_u!GN51ypDiAoo)`m)V1HVoSg~*K=N_l>&URm^t&0{RP9;rT9{9b z>`#C6OdbsOYr)0Rxyu?N&0LlO802-<<$1X}hDgmn!&two5>BV?jyh_HjI=!i{;ijI zSHfp%gdox5*@yzR?(NL^ z`t=lulXMV!w*@BB@}XQSzRdR)3Z)%_5?b6r0|S=}({Rdhu~A0K37P>z5QLX8?TF~=7goQ0xQi44jivN6A0U|DsQ zBcQiBn!qjF!;&e#oOfB$1+c^rLcA+iXGERdeg;^WFaBWBXcZ&GqVJ&W-d>?xA6O

*&DWWr02W>y*@>eu$Yg#5@y);!qe(rVl%tTU^8!U6${_Zw zjvZ`{UBe~=VUTs=)zjQm9d%T-#_Nb+kX^%7c(z*|`ADrBFuoZF+$dfgE3BnD;&`<< z-bpqh<#60^1o7H23Si_dIE=hGf_R%j98e5V!||l5IpTPW8$iD4LqQyGjtJ;jjBYZ) zR^|W{`nt1vZsU%b1e5t0$G6X_q~qSIac4C|Mg+`>_}wDsk#I|Iv*h>@$+vH-ob|h% zCnZB<_}rW#K~Zm6%T8@X@Lkp8j@Lm`50UXd%88Waa53x$%krrcQkYldeS^dMavYSB{RqAu{vZ7au$b^~ycIJ1%136y%KFqD_6Uh}{RN<@bcJ{cBAP|Oku6m$vUlfKIw*N<4f8GV#n zazRD}Wl2OSXt!$JzO7SUE)=awgjmjdFlUiv6;>7@SkPdu#Rxtk;>^AB43P*-zbjE^ zEL|2bR*@2O$e*kmN7V?iq<0W@Z!c4>4=fWP@;ZI`mp1sUbsvh5GyH>BMFaE`?s>dS4^x#6J+D~!<_5M^$=&>d!<|ii4b}y!ebA< zC&Vk=Y6Ju#vlG4_;^gYCWFGJ->2Xugzsxqo#zT-Y^8LOjX+MMbrU;GqtVAS1ZK&Kf zNff16${oYF6bhr=wxAM$Sn_R&6p0i{zGvDlnE??rvEy2q=h%*EGT~PZ1jnf*hD)*D z9Mo3J7|EH#F3ZrQ*Z;`NhP|LCd%LGmbU5i;|~Z4>#v%Wi*+AA`%#+L)MX_ zG)G)-eFMd}k4h0$+LYtyj#{eE#%rPsP@DJNTUv2N;RxwHQWW4lw?~I%bVnuCt?Rmz z2$;j6$gy}_$1z5ep-5QYb#tt`mhOn=ecrDq1c@FG9**MBWPS$n%|!5?uh2SQY7VZ4f2OYzTNX-IpTS@cwR_)RnqyBBHaJkSuacU*?#xbth=y=HM{%sWwoTWDq!1+Wu4L8*lK2gY-m_?*R#FL&d{16(df!UEt#;FjWLilh zD(Sc67^g-6kD~FuJj%?0JHaA1WlT4KeEYcKO_>zSfO8-~>OINd@-vQaUsgJF@m^mh zAk1+IF_IKdXIxGK*rFmsa^~jC>onag6w&8(=;lj)nF5|Z7(qcj93PB~78Y}k1PVHv z@JaV&&g(}k-yAXNX7mI`Cpl!yP|koIQnq!q@AlQi_;ST)^&-Tg$G71+D=n+Dau$LG zjqY}FOj|jVFH5~3mU>&>&PcnQm4IOm`GeJ?m5vOHhIf#6Z!c7?FO0B78eeBqpWPU7 z5)+q35D+=45g+Asc`w3wDPf8#y)oi@Zn#Vxp?Jd;g}=o&Q^HqRBqWiNZR9=d!ASaY z^?PMq2uXkcL5TR`%i@)C5sD}yuiNktiIcLs5_$wA-O)a>&5@A0H_Hvbs@#4?@vS1s z{hk#`PEZ{s-Zxv!O2OzI<9RL=MmbYi#n&sVEELOa8I>F%lq&bk-*aZpE9d=2`S~&o zH8N#r7gw;(Y;puG=LBBkJVr9#k}-~maVWx3@%kMN$$`VVv&oIXoS%5DSAeV^mN%19LrZ?9ma}W5hu89YCI2 zdvt{MI72%*v6pK(oohu$Xph2yw8M?&8Xb{6>I4GVpxn-PY-)4__n3E}d@Dyf*dRaS zG;V6<-a4a9l>4$PGbbjS z#ERs*^1`N<3WjEikZL|EKJnpYB`yz!kf3_Lb0kh;ct%J9L=#boI8@>z@1~vPPLK#e z5*$c;%&*g+4NSF48cz~^fBLMdm*~fx*xPr32 zyj(;(=$DM&55nTv4- zua=QECd;t2w~S=IynK=k-a zeRQz*v11_R(ChZ1lH@4n)121|kw9suUxbsR*h&!tdDeUTt_Dd@kz#$_WK~RU>5Si6 z%EshiRg+*Kdfaa%N4b@(ubV95t?ked-3r9M){nq{gV|T>% zR56f4ZQZM}J7Rm9Gh2lK(c{@xa>Vx3F_7ckUgC)Caz%CoI6YK?|>c2mYVa;O$d;D*SdY`1k9qeMB46>WBAOm;n~i88IRhO03ls>v2h@dgS|s! z)On>l6!01g2l*?Kgfs$`ZK3-ZuP;N`D%%r#zDE+QX>MXbjlzdxy#nR#) z2o$+1Eo@rpVDzD7QqGHGV8BUBTn-E&AqD;R*HvHUg=d5$Knj_fPrG9^uakFXCbbhF zWNbba4-M%fhRqFE;=A6mmh41uw7{4<;fo5n{}6*vIs89ce`*15*#NlIi8z%L=dD2?K|+*5gW0us*jWA^{YhwO-<2?ImLv z3Sbn6G92Z*SSz=7f`Zt$XHSthxFM++1~KsFn93AKc_r4y9pnB-6+<8v-uVJjaWJUT zISgRp8n|t!qqI`%;g(KN01LMs7i=4zMHm_}3}E7#_&4QQ9-$V(Qz9sUg{$yH#6twB zP!ti^x2i)I9$IcrWHo|ae|tKGi6CtWo)f`GJJ7Uk1ID#6ij zNxUh=QPMrjkIO_zAywp_B;r&F0&-8PWTw1?@_E=K`!A+LuS$v_srMvIEbEPd;E1;* zcBeuZ5K^V@yRH5*-Eg@r1cg-T+Yzz9%bo}FNOsz)%_@0XH1>lwgp(2L;hUdXhkE0 z@`i_!`1T^@`n)p1k>5a|{`04mUM3_ig&-h^Ld9LnPO9tjU4`HvdE`TL|7VTJi!Th9 ztpgk}gm+NdZ)Sq8s8|UMGEDs_?RtDH!&&-XNf*K)ufK*qxs~C2M!XWPMqnVfTk({I zldik+c?6_<$UG7;5BsG0a4KmZNBz)umB@Exs$e*xe6A=-s3@@{9%9L7QpWhFlrf={ z(Q+&Z=JmGmt+1X@ShrBfaHR0L@+zV7%E}Rl<&(rpLd1$O5fDs${V8iFkxwX*x7-)u zNP(S}c(_zZACA0~e;B>)Vi_W7RDCJyFWpCyPb29GBN-wxEFU7N$8{39PU6r>rbr%B zD(x>oBs2^p2L5%KOzIs%iEtHS;aD1n(tgRPH6RkQR>Y%}uQ!KnAVWk6Qxkzv>WM($#ds5M5Y_A2uVAQBv*`Nh)g$(ki2VI`;&m8JfP_1h8Yra8ApV> zuFk#i5Rrg^=<$!M^N*_!B$Xl|7yP7f-^D$b`K?A_9Jlsf_@`9{k`9r`acln~wfDnf znDM>DPLRaYNE%NchltD)7$HFm&}!lVo`;elV#y-}k`FuJ%*{Qw>3|`S`j%Y}kAVm` z5((4)LLlT$@4W0vt^FT1BH#}6JUD7dWE+V_f+Tj1L^zV)OGF?NdCOMw$4C;-frrS< z<}3NQRF4Bu2NM0A1S2RYPYI5yH#mIokeTHogVGMCT%FgwJ^xO+2#_2OJK@5=t|4;e zTnI=yY$snls(>5z*VX4rTvtAA@n1{BgxvL-D}xvkcC+*GJeEFwX5@Av7e7=|B%fD3 z4khwTIL67UKq&0AMC}|(<$k#S&V><_65o&uKSk1b$=J%33^OG1hJf-EN#aOSnGppd zL2oA-JeCq19?YiXW=1^F?7Of+ij*glf4b2qA)rxWKFvWW{XH8T^udNQked@ zB*J$;TWkIvEZpwqs1Dkwrr)VC!h#BxN8b49_mz{Q_DUDQ%CMk{ zWuIj#}gF0R$^x`KQDZ+X=jb)NM)RPUF*>S+Ipm$+cl`q1#cAYzLB!ENrCN|3g#PMX5 z)CHshAQ^vHjv9Z+a2ze}uU^W#IKE~CbK-Lyc>=Kltn5z^G_Z?TbaV1_0V0{NVlf#V zmAwJk9SFb3!I_8Ak)gQTC&tr zg2SPY5d>vo*w+S_&CDfkDr0e0g|~K^jD1vTKa%$ZVn>gAs%XmtBj4O*GTF9w30M); zr2ut=Jsf?}MsR2&Ol=6zhU|Y-j~SrHFbdbk5Xlxf1T2Q?U?*~pyV?5EhaUNezsbx% zZp*6ofq+#Qk~UXJETKH}-6TUqi%uN-3aRi+vSW=qM-qOC#sMS~Ao7-5;(x(Wm+FJ> zSs5ZSjRZkKuL`n#tbRel6UAzWCrl}YASuU@@bY|!$g~rLq#Z}X?PQ2ZF`ZO`q@PB@ zKdv-i6Bv#b@A+-ncU7bjB>F+um4NG-ZmW`o9=+8&eqHuu6(uEA|D2Twz+qbk^L{^l zdU8gg@ z@?Py%841Y#7xrv3$-6U1-OnJ+cNJ|wC-IaUPA|IQ>4J;y^NcB^{Zl7t^D!YV3+_1Y zYmW$))8~CBoPz8>ekMs6g=2ZR$%s)939pCf@H2uer}D15!> z5XqL(Gbousam4t@->Zg*v2`UU0;RAItT~clzB_z~WJ~KAly=h(Y<^s^WPnBEhx}I} z{>yw<$qJ&0>PWicP!5J%X#`cMo5($=k$b-fF2Nx#5g-!QWN&=r4=pfilBy0OaA_+ztE(cZwsHEQ1 z5s#=+h$C+MZ&{D(-}v~W>YVTD@nRrRSZo!1Q<i3 zvF?JRB4{(!(5Xt)kq7HcgagF^PGdd{B9GOPd6hLpWRA6@wa8_h-LrfBt_E1{BX$U@gblre3ZmwhS#e5 zV`M3k9_Gw@2^z0=he$S4uS&F0-tlEUXSEY&wNt!4D@1F@$ZD(pN^DmW+pS8hWk30S za`<37CjRC4%%4J{f{9JxRtdVNS3DT&R0V9D}gT+yp}|X zZx4r3-VhE)5?@I;R8WlMLQBKOpBRRSHQJ0Xs{`Mw2eOm(!N(ENt`IivaO76?dIDh}^nPE|{F)-6cOM^#`xm;Y%SFXXOe2N+eN*;5 z#Y#RZdEGMplH}I@2OI)$Obj*b54NWCqzlt+9e)fPO2USj2kIVA(%$ZHmqr;@}OaeWNFF7j#&T2ZU8bGrCTi)KU|Xk<<&Ks0Qw>hVs-zdYM6_Trcr z88TK()ldnTavqF2Dnnzia;IS0c`yzJ-ejbhW*Pz0Kk%73Jb>-UuN{J^@wT6tePT6q z0!Hua&din77zmnr+waW2u^PdQQfePH8bM$NkeV9E0XoY89v{SdGO(~j8YPj&tOkuN zJlp;K5}37*&cV@}jD2UQN9gIo?3cc?)deU|{x63%{?h$T#z{gXs@eBvf6O(N4UKKzDAyZNyZ$Xs;X>ZbJGxn z!N#s0@fJ^_i#le-O~$C=ngYQBCzCtJ5*)Pmkg+iah=q-i#lW#R8lg-kTM?5Y!NR(N zAKr_7_Ki8-hK7taLqROgu|9th3ItEBh#;gS`ACjEj;gSD|>$Nq#S{mGLF@nqAB zRSDor%cS|a(nhHzt5lLznkz%CQc^zUkp+0<>5b9ji_`-HzRSHu#}uZ?7-bo)@pRuE zSMXtNwzMojI^X!%!`xj7VLUs6nf9A=o)!11;^@zj*`HH|q%93RP=?I`fdxqB`vr%H zZ6AU#NMC)xFx0US%4BAKFC=AYEdA2p`M4a#iftPUfr2SF{J7?a6Sk@H0jYh*qO+^Tri3G8%8tNOi4?SPUxkMEuQN=6qW*gq}nrp0{{ZMrR0nAn=ZCQ1X*~+Ur9L!d2 z6GbK{NXF7}b6IszTeVLVg`fcZT-&6!78K3FZM85_RDuH7c#C))ZF6v2Elw1Tpy>B2 z53Mw`Y0vG7B&T%4!paH~NtM8O($=eQTGG)SV1|s^pc~oZnxBmxzYUCIv(1pPW=aO; zaXZ#)SXO?{aZqB&sEvk_^_%(e!IgJm$^1^#5V4j@h(rJp(fXeE$}g+LK-lUK00eBH zZVf)LivxzqTvn0^jB*f03=ZaZ$XuTlfuUr2vPZh}(Q#IEh+K9~f+A?knmdSgj6;{N zN*rI6{0<}thrVAO`l2=r!H*{Xt&$?$Ol^O}WodkGiML?Rdn-DF;dTpVCOu6b?cx7T zHg-_plIu#Zszr!eW_|*(fRUXho{@y+=(wH-WUj~#KC%3{=?Wp!6&Kgo15r!)oLYpa zWhPq?OFP}_+ZqLwXJ6J2vqjcrnmLa0X6wdHD} zbF8f}83RJ7M$);pnFX&TU30|7HmOD-R3mBKYWz%UbGY9&sYW4GBWT^4&)RGciaN$7 zO~z0Vs<8qa@0@Dv4yv(Fs!<5lSo005L#qsJ8{2+4LRPtauB@5`Ndnyu861U^;E90Z z*c@UqHW^hL;Y}NAYn(rq15I|I8Fjm@(f;u8rZw`{}%}t9sxO5u*cYo$YsWa6!a`Z>i2QOpeN5DT~p*|!rFS+O|SpgubS z8%XC%jAuTv1xiZI(Gb|?s*Rx*K%*4WS@Th~%sk~sEZ;SQ+JSYOOOa*wMt9J3ebRI} z5-5d0DciO$O9xta@LPTITUiK{hM)vbV{>;fTzxWJ88BRh9KP&rvjkp0E(gWcC&fj! z(-g9cs`G9-$B9Cd33HnWK(U{-%(mw(Wh^aRfrojM33HVQfKdPp%yH!q9VjNpl}S(p zYnwip($7>_zzkn`ytwI)JwhHjUL3cdO~#&MYEJ}=oCo8XS+W^2yXe8dG}cyE9i)om zazvloQEC?gr5}ePyc2DRSWiBKLRy9-#m$kp_@YV-gWY`sIE3Ixe6-JTz0YLKPKqET zjUW-)#O1>A+eQ$K{c>?0m7ypcr1p@xd@#Y0uk`&fnSWBpAKDN&1jPAx*zG82_Z);yKME{>{$ikKsi7|mo=D&e|HMXZWAx>0ke z4k(jVse~XZXTjpqT z?V#hP^l%(V<1K?j#JbHPlzoQ&5sqh+ih~<68T+;h8BZ>#&qFrHEtew8F>N_Ntn$;W z`0BbU=<=AG3O0?sFR{c?U&a4jUx6-<3f7D~y5}Ar$XCx#>w1qtg>-&Ar)4%SyCpRZalau5m2OnKUim=Fo_3dsv z;nKgTc%GpdL0XTd7BrYtSZHwGnkIRRxgpBzik2F|$^PYba_eV?9t# zMUtOPxyYyzjkm1_EAaD9;LB9YAS!x+yRCO~o5iCA>hnJ!#of@u-O?L+{+`ztE{X|M z@2^Hi;Q4imK4LlkX&STOw}h>{P!VfhVt!2vQe#$=eEDqxUhZ5AIq*r24Rd4v`DG>l zYu~vAgP1n4Mo|O&U40#-$rnM25gWZe2%Gs0aL=RrUJz(8n9=wFhcmxIUF-Mr`qFPt z&ZIvF^wwm&z1@2$Pr%vN4mYB?Qq~7Z^6U!{F|i2VnT{BmS|Zug^TJGGE{A)UnR13 z{e#~^QW=fH!`=0;C=22E4E`n5dn$;B#7n%gB0^>*7E<{+4UyVU^6(OCT^bvx27knDGEc!w?F%n>QVV#`8 zflt6Rzoj0k+-E}5vaM9bL-|SUxSJ^Eypk{a-u2i7nH=O{)AH)~?yO1NN%Yn=P#JAu z@7b9yhjTxh7(pm4w#3PiCqvn&|gLEw*aYllo^<&}LPuXcnCmG-iZ8NNMicg&8saTQpf6ue;?Lan& z!RPLjBEDxw^PwPW6~fCFSo3P2EFMjVwh#B)I%}cQid?}9Foup=s8^PO5Q99U0I@7< z2-cE$>QvebSi#m|Tt`QxY&*BxFOJj1L@vjVbz47R&KPYAq&k~nuO)fPJ1AYT-=Y$rm8Mu#9&qrqNx< zvf%eO@x8`Ll|K+kVG`qEUw;U?eEZs8SIhhw_eLDgt9GjCr<+%iyO((E_Tpz{eJYWO zm)k}TUud@db1E_@uY`YM;#+sT_Hx(jBM}`+0Hw+&VcvrRa=t?t6f=_xV1tvPpU8gy zn4HHp1SJ=Y3~DQH@9pnsJ&QB3B@JrZZPN{pQ5l`q?t4;j@FaC=+pW|68Z+j3(Q6mk zeq&6bxXmiy0kyR!5E3Yoca5Y_TxS(!RQsA0nL7h9w#+;r2O)y9~+vr^?=xzbAN?O=i$DAH94K;an8H1*bZITPiKN%NEg zh_E>+x1S=;#d;u%T9e8=Y2c#sDzPx1uQFepO81h{&t zmcO|KC|}V9s=mUo;x#_#RDnUIo0|KpD=QwvgEG`Ir^T>w7Pp)gkIwO8#QHnc>^{6f zMhF57zEeu76!j~%sw+5^8lu+ttpB1-+)%wY+Wx*q!slO}4knQ+PK7sht zbpW9kX`aWQDV#YK*8rmTc35lp%1er}CI=DzML<|I29QN8DClmRy`DBO7If$u$B|FLV`JtBmSd6WZ%o3-dRrore7e6t9?n>?P zZ7f*~gb*z|;S;AU-Jq$n*y>Ja_JFB+uq_pR9#jxoOnc5-1F1a8O!!?O1b%pC@42ja zphk3j_&p}#l%Yn0Fea_mu9Z6J2p|}~ARm3_j|@Znttlf4kzZ>ck(qa=!CEVI9xGoS z9C-c{IhI#;R5@>W&(r4~tAAgpo*foRNb~U?!ThRzDshR1eV;V1*Mhe^xx zq?fhK*4Zz!ne)l&t+?L~n5_Z-qEf)i`UDx#M-Jr}G?UzSHt7zAgkD+oXg`=6s)9$n z7kIu6jW1>-*meq2Vz?cNBn`VjH66|21!(Oib=>O8P}k!ItUt$e6^Xvb?-1}v^?yqo z#|@!nY_S*iMD9D=O8T%dMib#`Ot)&*jtAM6RTuJ{nv8@t-d?hswsiEVqeA~tjoM1K zv83Paclq_6V93HjYg3ylT~Q>Sm)f7DiacS-n$}l)SX5+tOpvitwpVUN>a^~U5-ywAO*g*4#l8x~y6+^4&QjxRVD%2$f`>}Nq@}_i|GuMt zKZvfd^kvAr8e)v$*zWR;ig*zdRgAI0JRqH8tczq@uAMeO6&;tP`E=jJJROxl`(y;eo~_eolQKZ)2A0NYIA*xS{7fO zU;l-I?g|ity)uBR$1d*_`Bm*Bg1$7mqj^>f=TYnS=iFS4d4wcZnV$oC*NfMVUd!R> zAsHXM0*vksh$_K<*c;obEvSQ?xiC6)T>R2H=YBM(@K@Gq0*VxJwTjV$au2r-sbZ~} z_Vu4;bhW^mGB@}$ADAKNr3I5ut9)nrdhq6}jE&D z@?ttV1ev+%rNr#)qZ5{7=NqJE`6jUW9+yBCFl)+i#QR>0i@feyPE*~`@v@8r;}46t zGT{LiK^S!*%1J*ZnF~n5eIMJW%qG=LUd4mp*>Vcyf%d5(GSLDpVx5I!4@7DTkzujt z(8(XqoJ`RlrnC|R?GwK#%L|R}jQhEjGULx$@ZxqV{WcwM_7hOdjz?_YWqt~a)teCzERQ3e%4xN#na9HzZjJzfJ4DR=!Y`^V7y6A4rsiPioYFb#7FN2swWv z@07@FcIZ$HV*+qCiy~WwN@geg28J7=@7vDb%rC5gj259aLJt)zVHkJY0FWVQ_(r`y zsaS>+Bl5Xb-Hdyf8Yaglr%=ItDBGz=cE>mX`@Xes0G*7fsa9l?w&0F)53rR}aGrYc zgE^HoCZS@e20Wmm21kw;3J}>G>LoE=5K#)jTHzmzwD#A^<#>K;n-Nkjd!f~Q`TjWF zGT)UvfKT~LaaN2i4dd;z1f;Vt2lQRp^A#g{IAFwBBFlXO$PEAEtq^DXkzZHkD#RT` z#+M0V1HNIiBOtWjUD$Ny_YJZw)SHW#vQ>nV49wEN5hT_!Y<3h_Y&AWdsOg5z04@pZx9j z8ojTTniAp9Lf@oPxb_)#5_-H>OA)syXP=oR?i(2oRrO8fLBQ<*GrUBKS;&LFXWG}* z#|DKV=`w~H9$mvnmuiznl|7)v@UL5qS<_sN-G)C?@X*VSZL)6Hrc)RK8gqasDnckbuJe>oc|txO+QLGxhvadBniJ(UP$Hr0L& z3Fkf}?P!q2vu)J`nD*qXZ`_c_iA6CxiRQ>Z=R9l8qIKcG+UNP}$0N59aSHA?AFo44 z&j1U#eyWP2O@WXp4LSEO{Q{Xrm0+#Sl0n*}1KQ&joqNJ!kHG~#pI=uf&=;tyF-?wzi{vqchjy~l-G2~6S$YDNb!94Zh=g)M) z35rL@E8F+)L~eEVGS$X_h}X1dxy{_}Wb9UvLrSOA>j^rz(k$8j)B5wXG_%%?c8vsd zYpB*Lbj@o)e~n%Gzgz#VL@ZRhXl6<$Piujm$e0CQ83M_m@{*9{v&Z&WF_(a>gwg#Q zJ?s<@syJ)Cahu&O+;CZ#(zUd^4X2p>rz14RNVkKMJP7Tnx}8@fJu3huc5sBIjnwc0V1erqz< zop{r5Qv2N9+VVGC6vY!4h2%eLPfuFNFN7^~mSR?IBV; zHbOi$VQTH*{&Q2tyNGdPPVj3#!{`xELW-=QPK-inBzVA>14^6&zSaiizO~GsDH@(%=;n$%pmuCvB#~ZV-e)s&-;$DY z!qsuqob#G{!1D`Y1c!{N$RBO`(z3DQ5Kn1afnWXz|N1j;J4Ydn*5JWU5GVpMvgpf{ z>Mxi2u$vZ(q3lurJ0oG~tQEG@Hjpld@MJ6_#Pk^)LHHu!XkvY=jq+9`Z9y#1zKB6@ zYd?GrDdtQ+ra@bhQz$8e;zgmw#=g|#e68i|Kng^iDE$lP>mTF5Ox9Xcr`M}>$SN}(80;*BkmNSD9EoP?n zu|2~kPA)^grN=*(u@u=q({Ra?!D8^e?!fBsQI`VQ(B|64W-HUwW7W~2<09|>= zfedK#y|Mu1C`b_t;+3sCcMDJivwb4`(kqYo#1vJa1hc;$0`U|<23L#f7r{-vUIVRF zh)0)A9b`_6fyCV~ws28bH5uAJS~%k@Y8R-!>rG_9EIp)5$B?A%Xm!g?g*j#Dw6+`G zv71?I%|C2&D8bWV+<)F%TC|_34(fk-BD8s8`BewV_oZ{=pXpQ^U^gN+o1XJ6*1z%9U(W!YL{;YdHvlC-dwCUctM@) z1Bij-=OgysTGP`#d_KGEc*6~Ot%4lhRb_~c&&P5fk!x;ZY#R5KiVL4PiKL3LwwttZ zA`DumFLv*Y(X^rwHBHlz$XXu2%D9AoU4f%T6@o;oJ)(S<~hnB18u38D+A5`qr) zH2E?YNk`m50^B{f`o0rkvDxr@*1V^mBv#`Tbt~OcOGS+ABHIOq&*wDUnQ}QGo9Z-1 zjjXU6BLR>i0qCM1Zh5=n_Mp)E-P?g@J_(+`0+}wkmQFX14%JTA6M+7dWuEr=~(C?Lgi?5W5r4Ue1tHz6TU)sXBqcaTEa|Ur4m3C89uwHn;OZF&pw}o z_(62KN7-KO_2Lk(@$8Y61vBMfQlO5d0bP_5(NzgDy`fa9vi?Vt@0k@9w0Xo zryweO$kcpoL{mq(LeS4J_mIY`77_HEv^=e2!oVwY^{vi4^k~#T3($T!Dd`^LzYj0B zUbyb-R7s%6UAahm7jXQp38Xw^VR+YaOx1)Ln%{_1})p@RVNnKfNy`OiVd;;+yF@r4OZB~$yw5=JHvsUG)yK*u(e`11lLhJ_q;c@eu75@Pk; zc}>ePJ~=>r^RPi9N(~sYo$i9Byxv#moJ&)#8g}tXhTugR2%9d%*b~KpkS-AoWw>J#E+k{mSC@$+>8LZA2BIXrSgDZ~J5eRn|3axt`uX4L zn9D%gGNj-%|Bx|*^ZAcySf`uKLI{95`3pMsTZQM=pSL27bw(Z_9UDt4MdEbsssFr5ypZc;|xXIvx zy|m4J{2N<8h{#drxEOzV^N(g&Bk;G5B=>2ZWt4$=f$Uvj+8#PGoabomV@?*6jz(Ox< zGKBZa^L{Cx;8|>bKA|8D%Nr2+_v5EOCgv0{3pyN3z@}urgJymx_`8y1pcmfV5wq>n zUJE0lGx={)2z$pg`?)+*c!B6y5bQ&R45qH2)KUe7!K( z327XQY$j{sw~+Lf41COn`tMhTZ+E0gO1z;)OX^v-@|WQSA>I|BL9KT?=s)@z()3kw z>UF5-Qk}4UXX1wTKk!L7%4{p+<>PGPU^kIyWE#&+iO;}y^WbRPzP1;b+q3Cc7s)~C zZ5yKHuY!MBJ53(0h4Q}_%54)1g!D%CofXc0?!Y8p*KEzWd4tbsWi@F&KTzy!S`9-- zQ?7=F%ng*xGRSj<7vT8FBfdSIJN(4f9v*|?#IKZ)(|=er!nKUGIQrFI%*~a08B1+s zUe}|C3fEL!dlk+(M3Mi9ve_4UG9xvQ)S~cO^%uX1!oAh{iz3jUtBqJmF*&?-A*RLvxTN^x zz;;YT!D=Cq<`ti4r+|w4`wu3?QMSkV5E*`yHBYGZt;KXaxadvIG(?&L{X|6Nw#C zXo6z+_g!}0VcydabZtrGPl47V%v)#P{#TfVMkQHDygkJE9)Y%FQFTFQlWDAUQJ zPf^~xt6YILm_xBi2Dgd3lU)EY#7G3BAwxS}KaUi#AE`>KGC|tGU*F39GTYlPn~1~? z3=0`v13bO!FzmY2rVAWJM`2V~!QVq=-I5^bS%D}MrO0Y2!M^r}c)!7CWO&Gm)xp7? z_{D!_da~IEW#W9=VgHpFj^6&Q)(Kqq9`$cz50rl8oikCAJgT{te%hPGEnl`rK9Ji( z7ELcHvEKS2NU&lLf2Xa$&K-(PPhTlv84ElK0jm@8(1t<-jE~Q9`&#npliRC&tI@ls zt~iaBZG+#oZm5+1$vI_R_o%c9zAJJ3$LhxaN5e{GZ z*8-BHFe`H!WivVR9s!pQ47_ z;WkPmR)#fB=Iny_F-n#!*f8$;qi%}gZEG!X?3YBBgFVXksxZAO@eIzo!#-lnTcJFW zSnO~6hG=q$RxjnM;%nj*x+F*!T-OQ|s62!(mPoIeGVtOpkF3lEjFfujG2?<17>Bn+V226->?>N5afJHX`eM?kNyY)EfVi& zU4M3Ue;;+HyPSoC>i0vCKVD(&!LEWu$Yim^-F8i+SJdMI_42*dRJu(dt0c4B=j~^) z#vbfYl&_rEUjq(W1foo4+F!Nbu6q$)k-2_jY|JC!BX!Z!ku!SDyeQ{~OhLu(FN8q*oBT!T@)o{4YH>c@FIrz*Pw z1m|~440Ss_ApE#}M=!DqQ_McK8Y30{0?QXV=5=MkozRS0TH1?$#JM1|D;I^do_GO} z*$P^;V1ncNHHUEEi|UiajjJhz7j%KHxQp43Ic-K9R7F%8JlCOe9y9Np3nh$-`!Wmg zfbCm{pKk(nfkPYkdG_W4Ohfq@LvoptejZ^y=%`tN=(h8)H(Us}yqWnK;!;B@_ebND zodS>tA3i1*5!sVl%HAM|ev$~?>;y{SP42K_RBvf{uadVX-8T)4{jNRaF`ABF$&c`c zsWo7LZm$iLhb_e94z#Jt6p^Krml#KJ-WCR^mHsN2EScTmV83b(8&;jSpC?VNZS0%K zJ?n^66=VI#0##$T>wnv%IRZB{x%sEOqqOo@o2W#a(Mu$nIj2zxFv0@W31m|lWL4g$ zVx{lA1K|rq+-K1gp_YYc1Pv6Cm@_`v{>aXo5KmOVf1+KvQ@DBaFRe=5A4iojlP*di zUR((r=1k9Z)*3YR=uzidnypz-B_Ay6vDwuSf#>%aaL)Nk8+Z%d2_=cNcwufHsZ+>~ znafbOsE9Qg9M9OibQ^jAru?$COYM)TLxHo7{cYXkZmw3TcY>MU%NtN8$>7s%5dP!Z zA&T~Q;HW&xZ#@w*x1y@x+)`B$w4RSQf`nI3tE|LrEFJ|_{>G!K_u6q$K9C?5cMF3- zX_lvDc~h`!lf$v2a0YD+dOrC?DlfCKilF|wsWK5U{p67Q=un+}M0i3vi-@nPywjlD z^4!cOZ~U`7&l_Jgqh2cq;%x7vb!3a-EtNcXjTO!=NWsqsZ*7ms0~Rh z`A!P_1Vt5@uSLJWVJtoVHs*C0uqRG@F)L@@&b9c4_g2jvBA|$eEG%46$*^5-wo+2I zbnCbc(z$u3wJl3)94FP69%>FvFM7|u^S^4v!fDPeE&PzLuLLOAc=%aS_B2Ty7J}9W zvnGiX!Cyac^dk1yBEXbT)>Zg>D3HEU%0I@Q8CRHG*P3Q?M~EfI|JJ;&AY{CHJE9V- zI%!50+(~A}HakBfb`pCnVV}R9fSUe2>0)^E#CI#Ry*Mq*!EA+mKtS+_fMD6(3H3b& zO0$N7quw5q6yGxqBsQ+^Io^b*N#WVak%Z)ryT7X~W6u?vnm=Lz1`;I!L1o|Q1a~MC zSp?w`CZ|}60JielyC+@h%iex3*o*DWCtsL-$u^TO3w3w8^Jvgsl{BxJhT}gW)$e_D z85fWaJv!iLRNLh_a8LLfa{+CoIL9+rEj75k!ftG`I$+|636nRJ0`h2Upx|k+Qo$~6 zRfCDnD9<}wHgaS!<=NC%W5_^AH6ZURY8WvE#v(9D^)0g}^cFpEPPkAO{k{pBKnEILnZl3{HjYt@ct4UII5Okl4$AtK`x`lpkWy!Z zEq+WX$hPDoYXXFBT-eZroQ4~UlXT=Js(r)D_Lg+kG@KB!!X`JvKDsI?yG@OQ)6}*? z>X#)Bn6c15?Zk|~P7J)N#9Zw?4WwTm0~rA7b7@W6Or3&-EH^@*W8z7Tjt|cn=^=Y=52qT3tX%>DMLX$ND36X2U2t1f^Z0(T!mZ&c zOq)^rP&0`SC{6QP9jp|oX=dtel!wuKPW(IeZXbw>(m#GE>j03Q1!aEkYXtYin}7ej zh39h~&nc&%S=Vo+kR=mlRkPP=(#Z%6Zc9YU+Y?_BgyhTLpNW1$Q=jSLHtww+z@P7X z(N_`q-V}OfkAGnbae38MR}b+a4ya=1ha7j~)A#`TKE$NCPVIJ8V;zDa1|wF%JkMlK zRm%RG``S`z=ioP7Nn9QESj;T#!0=;E*YB|zm}R^ASu(QBUtI*NKPY=AIh@yjRZoNB z;OVG01dNB#qwhH$>|tagMCj;d>#gp@M0$qJ59fh6({!^dDo9pU;lxTH$bL{2d_Crr z7vi<4uR*l#N^+PM|v1#_BfWJi^cY}kdN?p!uN6-P?Pt?Fykn9CROBACH#}s(RjD0fl8YO zXY>;dXbT9n8caNNTpDB^#m2y4E`ROEC20LpsK!~{6J?sN3;F-WvM$U7_jZAKxsIW4 zDjRE+yU`0Ylc?WrjC2@cy3LKYw%p*I!DEXC7Lc+XUDIBC&CjGnx_WAwfKD$xS zt4uR+VPR2rpd{?k(ryJV*ir0M{ybUGOYP?~OdI=B6T;q9r^WJ@6KwrbQgiNUMW@r+ z5a0p-$TJFdNS%;>O6X-w;~}ctDU2i_r0;=GSrUOH2IlV@i)#2?eShVi#S`P^!;5)p zOjLj1H*YOx`C728OGshpr6Tix7~>YnF+QtwFHgJKsF(RV@!sJ6Nxk@Vu^hcgaLGkG zX+THjS7cM7`O>Jxgqq6hR_O9unCyd3wAK&t@JO5;-s>HzT&tRDWf{!;;*5|;Un;*u zCZE@jLEm}SaisDRC{&xel^?faWW(+kR%v~Vl$bGaTL>RkOm>tL`h~QD=CcD7P}=%G z-**SJJsBSo<2UCa+1%1e5doOIjJt31&m-xn&TB7jj&i{DGt-_f{7;|-&kR#)(Z)H9 z$}%qXg_V_De1?>GHAKfg92eTL${-mnCCp4p#ti(#zaz^S<%no6PBd^;=s_pFmdTJx z6wp%8eJi9v9~UduXJTRJsmqSTf~P%VIrNN|;v|hQNYTLjC5mEGq*O%~us*(`cMSB@M5`js+9E=+6d&}}e* zl!9Rn3!a4ncNC0c(w5Ifuv?{QM*i&NQ7)NtL#C3UQi8#57!?(M8FIxEbd2fi-;_1y zSm>fY8T3|jA&o5bFr7l~$Fo*fzxZVQmt9IuSpZb=`=#$|_~EhBi7HbT{Z_8k1nvD{ znAQ87hKkJSpo?xXmp8MpNtV``zTU8|-tM3<`b_^Vk$uvea7o(u5(j4G;Rt4P3mcEN zWc8E;Vaz*Vg@vSp6wt7nHs$SEO0EQnn&4f=d)}I+R~Ccboc_Dk32`+WYGj4L+)7@7 z=G75qyyYy^5l%}YIKi>#LzeGul`MKea9Kh-mH5be$1sj}mqAhVEW?~X;=UVO@pFtx z%kUYIKgsRTCz$+aT%ge;S{|UR3t~pqctW`%GxO>G^+H^;o4UPR4(lljnxJZVxvdB! zyZqXy1{M7Z+S3kMG7P9LgC0=41hq<$+Ge&wLmoJ#mdqkg8`q9l6nZ;yLQTNS z){{Td-8OAz_syx&oGFB|CE_LeWqr3IA0u+JVTmkKxAUpu}C*L^J_A!o?Q zceJYu=nKokF+pM?UXFXQ#;+7jIs5n+?^G&r;FvX!w3ROl(>GoIGtnL3;MIP!!@l>n zaEyJX{qn0G%eqNx1BZna7fb6aYmAroqM^7?CY+Oo!U3Nfh13N(b8oks#?N$bH@Qyw zVg$4@{FRSeV-d5=!j0&CR+LvjgE{KxqJbEC$rHyLE&Qvkaih+!kxO+E*UjD4EGG|$ z$bfiH24m%YjW4mX9*UloCC*2OeTHJrHm`9OGf-zd76dmM9dPkt^K6kW`Kv1#WRH~? zlbK3eOUm-0D&z-cnj zXJtHf@J%2;VY$iouJ(hi71{hP+#Q&@$A8QRQ$X?H`CY$&iB2%OQypsFS_SKx8gy6X zWzD<9*24ndw+Q0agttDrQ$a2=yR)cSU@w+YuuR^9du(C*-`fsm>KDZQ&mT zuilDVE6}%9>;=71I8b7&y8lL_IrEv+*djmgPR@K9%w{;}%r@3hlG=xX)Q>agWEA7n zi*VH%uhkK;cyPS{#AGy7WtNA?~vSd z^g$zf=zHZ@9F}-T_4(&C(zXPm1hn>!Z4-D2TPQ6bY~uO888YFI%ES&#Oef(KIcqRi z;#Nx{M*#1^H$oLsdXL=0C4nTLSJ~_OMuA8R;UNIvuIBd*PbDA&14Y*!5wC*#@e>{W zDPbeTq^(C3P;9jPjO+L>1eDdyuPncZ?Of*6-}c&2OsE02%?V#GM>xvz7bJcnCWm5p z)Xof8Te2x#M1_I>NzfuOW!lSSS0t~SYUXr)iGSSqkoANwCpnM@9kC&XGI>+k=YKon zZ{avnTeYwck4$*O%4c$7CTo%f7M6qe-aJhZt=_1D!?dNMczCT}Ht_y~blTK%>^bLt zxgXzBBb!S22EL8D8LZ3^sY_x&kfgYEVf3p~SntVBk&@j&@mtT*<;fVCDXdwQjwD3? z+!a9s*<4$g|5F$^q-y>>LW?i;g|!B;^I+G%^AzI!)wgP952@Mz`ppgptyD$GS3;l5 zfeQG}O7~e$*l0O_Rqd>`T>COvS;52KepVy;G6*W_cq!nqf3sb_U-EDCO^DW1IavOs zIO8@W%)WUnJzes|XNcl92vnzL3c!z0mue%hwSp>86m1_;vnfkBo5CZme0X*U_z`$9 z8&OraQG3c&ZMtQ&g$$WK*j5noTe)ZQTP=K6n7=f$Jh-w35X&l%tSjMc6fVDzMjT7_ zILj~o6Uo!Y{k_1TE4oCbZ40wOJgC#($K4ZU0H!5FGxB?Mnp0EPj3zqB&xJ=I3PX1_ zg|ro|SU(&V3*AISbVe)lXbQ=8wCmt6Yqu;2pqGsaB(6mA^TlwK5w29)jTdmioz)2e zj&Dom{qV)4bkg$0d%iUwZ)E?8ih@`l!V6De`U?gANk$K=W)^SE!^b~gKdAH*bv7}V z*ST~!%mT}96JiQsO#c2f%Tz7|1e7!iZEc^Jg6ZU$W5W`d78<6uw8Erg)bRbS-cSM= z(BEv=y9XvKEv>!FEyFPB30~ZG7X6ga zE*rq3!gYIS8dO>5rsSo*-e1Sv7}ipHcEY<)oe8xZ@s0Ea<_ZB3*W zpOD-OL(A=y|As~XAqza1TOF$lOEK#6^+kM-QpQ@&BF7?LB%iYT^Zw?Z17`DHCimWG z*cx!tTWZ60E;zhStQqmDE5y|q=N#ikNO|H|#mXvH#^_CJHxP!`AjFmQBB5z8qBmd7 z{9T_F(&x41$v~eae&sxzPR#kmjuP~Q09DVZsv*^WO*5O#iT!AfxPVwCxms4b&OLnzlV<;3J+EMPE;!UlOy6GE&vB$$*;v)ggyD=g z6?dbROHSVN*34Xh=sIVw9Z<1HHCgzUBZ`^6M+g_gL5XANIg06v0wr)WR@31e_W^cz z>{tt#I4h*Js}^r=yCv~YwP+eXbi7%JZ*>fx<1zx>uv@VLR^~<+agiz3R=M{A1l;MtpHsiwjINYS!(!_B=^}{Kp_J-84BtXfJo_hRz_C zT8y4JQ*2ZcW}vz%VYqZz?=M5lXl#hf&-Jn8`FX|rkE@-SDy--j3DC2op!Tpl;a^pY zDf|(im11<*{}EGX@!eRZZ1Z6^Tk<)@y|lI9&6R~2wQh;kWX*%=vjJUA{^o91wu3yd z4J`#dwScX7`80dBgE8VDN@HFZ$0a2cOHLfNBDZuaIZEJ2QLo2p`?kje6^QjJ?ptHy z-pSGY;Y+y-V^`x^EVFg4U!l7Yqs(vZVL-pM81W?5nDCG0zdqaO$a^fPSYTVu6)&ku zx|*Ufk)}cw_@i0PB~9>R>8pONm5w><-U&08!9SL05V{QLhD?;V>a#ZgC&RKA zZpJ~;I^4WfHH(|LwEe516uo_w^Dmg$<#)Wt{3ldnQj8?Y6AthmOJ(SMSK_PZv}1sfy{W zF(m)F45TD;cR{FB>WRGb)Do0jTCzyuO;A0#4J4miU8PL!6W9r}_ zHv>~?1xeYS2D`5iZ+OA@Q>hLgHX9zfEomPC zi*yD|VoEW}TFnUby+X)6jqu02eaHJ$oSpYaecCRvnZRUV`t6^@!y=6zyR+IE8shs- z=6fZ>)R>ovaar1h#~8`gC|Z*nr*3=^w@5buAPvMDI@o>qPa}>L{qQ(vqR8mTTm{|4?Ft865)1 zPAoF}e>$@!ISso9XOb%3r}pv=$u8Y81~ReAvlE2bpeZ5uS-QlE3~$(cRDXcs3=CV} zDS-0^C9v^q1N&rYFD8Z(ol*__Oh-fTt43Q1RV8(UaFuOvXkXu1u!69k-E)Y*bQB0mLagMU8A|QWR&|} zWNk&Jt?)8Yn-)KbN&(&EM0a7;ex@dxdI|lO0a3(>VE0LRq2olh%J_5dBO)`E8Nk&Ev!r$YJ2!02hP`i{|7O49>p0TLDu-4>zjWt2eF_W>9OWwOEQrBU zaTuCVog*QRvI#$DI+^DrNhU7ZQwcYKS~Zz1&ea3>uyx~VheZFQB1Rrv9@uv0&KD^` zln}pUjv-w$py5RqaX_T2W&L=}`kd+@#9#;1^|F^Tf6zIxK1@c-m6K`cK$o0c(~ueK zf=y>k^LqeOYG1o}O;spr5vtf`Y)NjF#h&8IeEpQ><+m6~oF-aA!ry{E>x2^G2z&`QU&1YtPT-!4H?_!O#2A!FL_UuUsF7UCIB3 zCm5lv1z|5&9W>6nd-rf)|6H?{lS|E`~Kb9ydCki2gkW)7J#i J=$#R~_#Y= 224) + if high and low: + main, coarse = high[0] + helper, fine = low[0] + wide[rank] += 1 + split.update(SPLIT[rank]) + sites.append({'event': index, 'source_event': event, 'owner': r, + 'rank': rank, 'main_input': main, + 'main_coefficient': str(coarse), 'helper_input': helper, + 'helper_coefficient': str(fine), + 'entropy_constant_loss': loss(fine, coarse)}) + if event[0] != 'scalar': + need(event[0] in ('climb', 'center', 'warp', 'phase', 'adapter'), + 'An unhandled source event is present') + continue + gate = event[1] + r = owner(gate[1]) + if gate[0] == 'clear': + rows[r] = {} + elif gate[0] == 'copy': + rows[r] = dict(rows[owner(gate[2])]) + elif gate[0] == 'scale': + rows[r] = {i: x * F(gate[2], gate[3]) for i, x in rows[r].items()} + elif gate[0] == 'add': + s = owner(gate[2]) + need(s != r, 'A scalar ADD has the same source and target') + for i, x in rows[s].items(): + value = rows[r].get(i, F()) + x * F(gate[3], gate[4]) + if value: + rows[r][i] = value + else: + rows[r].pop(i, None) + else: + raise ValueError('Unknown scalar operation') + need(dict(profile) == PROFILE, 'The complete source profile differs') + for i in range(112): + need(rows[i] == ({i: F(1)} if direction == 'forward' else {}), + 'The restricted main X endpoint differs') + need(rows[112 + i] == {i: F(1)}, 'The restricted main Y endpoint differs') + for i in range(224, 632): + need(rows[i] == ({i: F(1)} if include_helpers else {}), + 'An independent helper return differs') + need(not rows[632], 'The owned center does not return to zero') + return {'direction': direction, 'paid_sites': sum(profile.values()), + 'wide_profile': dict(sorted(wide.items())), + 'wide_split_profile': dict(sorted(split.items())), 'sites': sites} + + +def direct_cut(program, site, direction, a, b, k): + values = [F() for _ in range(633)] + main, helper = site['main_input'], site['helper_input'] + values[main] = F(b) + if direction == 'backward': + values[112 + main] = F(b) + values[helper] = F(a, 1 << k) + for index, event in enumerate(program): + if index == site['event']: + return values[event[2] if event[0] == 'climb' else 632] + if event[0] != 'scalar': + continue + gate = event[1] + r = owner(gate[1]) + if gate[0] == 'clear': + values[r] = F() + elif gate[0] == 'copy': + values[r] = values[owner(gate[2])] + elif gate[0] == 'scale': + values[r] *= F(gate[2], gate[3]) + else: + need(gate[0] == 'add', 'Unknown direct scalar operation') + values[r] += values[owner(gate[2])] * F(gate[3], gate[4]) + raise ValueError('The requested paid cut is absent') + + +def finite_injectivity(fine, coarse, k, constant): + need(k > constant >= 0, 'Invalid finite band sizes') + low_count = 1 << (k - constant) + values = {fine * F(a, 1 << k) + coarse * b + for a in range(low_count) for b in range(1 << k)} + need(len(values) == low_count * (1 << k), 'The declared two-band map is not injective') + return len(values) + + +def rejected(name, operation): + try: + operation() + except ValueError as error: + return {'name': name, 'result': 'REJECT', 'reason': str(error)} + raise ValueError('A negative control passed: ' + name) + + +def same_receipt(actual, retained): + need(canonical(actual) == canonical(retained), 'The retained exact receipt differs') + + +def run(): + word, frames = load_source() + calls, direct_checks = [], [] + no_helpers = [] + for direction in ('forward', 'backward'): + program = word['programs'][direction] + call = execute(program, direction) + empty = execute(program, direction, include_helpers=False) + need(not empty['sites'], 'A two-band witness survived removal of all helper inputs') + no_helpers.append({'direction': direction, 'wide_sites': 0}) + for site in [call['sites'][0], call['sites'][len(call['sites']) // 2], call['sites'][-1]]: + fine, coarse = F(site['helper_coefficient']), F(site['main_coefficient']) + k = 5 + for a, b in ((0, 1), (1, 0), (3, 5), (7, 31)): + need(direct_cut(program, site, direction, a, b, k) + == fine * F(a, 1 << k) + coarse * b, + 'The separate scalar cut evaluation differs') + direct_checks.append({'direction': direction, 'event': site['event'], 'samples': 4}) + calls.append(call) + pairs = sorted({(s['helper_coefficient'], s['main_coefficient']) for c in calls for s in c['sites']}) + finite = [] + for fine_text, coarse_text in pairs: + fine, coarse = F(fine_text), F(coarse_text) + c = loss(fine, coarse) + need(all(x.denominator & (x.denominator - 1) == 0 for x in (fine, coarse)), + 'A band coefficient is not dyadic') + numerator_bits = {} + for k in (32, 64): + a, b = valuation(fine), valuation(coarse) + u, v = fine / (F(2) ** a), coarse / (F(2) ** b) + shift = 2 * k - 1 + b - a + need(u.denominator == v.denominator == 1 and shift >= 1 and k > a, + 'The canonical numerator fixture is outside its stated range') + value = fine / (1 << k) + coarse * (1 << (k - 1)) + numerator = int(u) + int(v) * (1 << shift) + need(value.numerator == numerator and numerator & 1, + 'The exact reduced numerator identity differs') + numerator_bits[str(k)] = abs(numerator).bit_length() + finite.append({'fine': fine_text, 'coarse': coarse_text, 'constant_loss': c, + 'k': 5, 'distinct_values': finite_injectivity(fine, coarse, 5, c), + 'reduced_numerator_bits': numerator_bits}) + original, split, baseline, targets = Counter(), Counter(), Counter(), Counter() + for call in calls: + original.update(call['wide_profile']) + split.update(call['wide_split_profile']) + for rank, count in PROFILE.items(): + for child in SPLIT[rank]: + baseline[child] += 2 * count + c = word['canonical'] + for i in range(224, 632): + rank = len(c['frames'][c['final'][i]]) - len(c['frames'][c['start'][i]]) + targets[rank] += 2 + targets[17] += 224 + need(dict(baseline) == {1: 4656, 2: 920, 3: 1386}, 'The baseline split invoice differs') + need(dict(targets) == {4: 56, 7: 14, 8: 94, 9: 652, 17: 224}, 'The complete target invoice differs') + need(dict(original) == {1: 3163, 2: 406, 3: 742, 4: 165, 5: 40, 8: 8}, 'The wide-cut census differs') + charged = baseline.copy() + charged[1] += original[1] + mass = lambda profile: sum(r * n for r, n in profile.items()) + need(mass(targets) == 10750 and mass(baseline) == 10654 and mass(charged) == 13817, + 'The rank masses differ') + need(max(charged) == 3 and min(targets) == 4, 'The rank-separation proof does not apply') + need(mass(targets) < mass(charged), 'The uniform linear-width tariff is not rejected') + damaged = deepcopy(word['programs']['forward']) + last_clear = max(i for i, e in enumerate(damaged) if e[0] == 'scalar' and e[1][0] == 'clear') + damaged.pop(last_clear) + controls = [ + rejected('understated_valuation_loss', lambda: finite_injectivity(F(4), F(1), 5, 0)), + rejected('zero_band_coefficient', lambda: loss(F(0), F(1))), + rejected('removed_final_owned_clear', lambda: execute(damaged, 'forward')), + rejected('integer_to_float_receipt', lambda: same_receipt({'wide_H1': 3163}, {'wide_H1': 3163.0})), + ] + witnesses = {'schema': 'two-full-exact-width-witnesses/v1', 'calls': calls} + result = { + 'schema': 'two-full-exact-width-gate/v1', + 'status': 'PASS_TWO_FULL_EXACT_WIDTH_GATE', 'new_kappa': False, + 'source_payload_sha256': PAYLOAD_SHA, + 'witness_payload_sha256': sha256(canonical(witnesses)).hexdigest(), + 'frame_audit': {'status': frames['status'], 'events': sum(x['events'] for x in frames['orientations'].values()), + 'warp_matrices': len(frames['warp_checks']), + 'all_contacts_and_transports_checked': True}, + 'restricted_independent_columns_per_call': 520, + 'original_paid_sites': 6596, 'wide_sites': sum(original.values()), + 'original_wide_profile': dict(sorted(original.items())), + 'split_wide_profile_information_only': dict(sorted(split.items())), + 'entropy_constant_max': max(x['constant_loss'] for x in finite), + 'complete_targets': dict(sorted(targets.items())), + 'baseline_paid': dict(sorted(baseline.items())), 'charged_paid': dict(sorted(charged.items())), + 'rank_masses': {'target': mass(targets), 'baseline': mass(baseline), 'charged': mass(charged)}, + 'all_power_moments_ratio_upper': str(F(mass(targets), mass(charged))), + 'policy': {'site_width': 'Uniform over all permitted inputs at each paid occurrence', + 'representation': 'Literal exact per-register numerator; one shared exponent is allowed', + 'baseline_width': 'k+o(k)', 'width_tariff': 'Linear in the leading width', + 'limit': 'k tends to infinity at fixed native rank and fixed fiber/column multiplicity'}, + 'finite_injectivity': finite, 'direct_cut_checks': direct_checks, + 'no_helper_controls': no_helpers, 'negative_controls': controls, + 'omitted': ['Adaptive-width sum bound', 'Joint symbolic-state lower bound', + 'A limit with growing fiber/column multiplicity', + 'Full physical Gaussian execution', 'Recursive child compatibility', + 'Compiler and outer multiplication replay'], + } + return witnesses, result + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument('--write', action='store_true', help='Write the rebuilt package certificate and receipt') + parser.add_argument('--output', type=Path, help='Write the checked exact receipt to this path') + args = parser.parse_args() + witnesses, result = run() + certificate = PACKAGE / 'WITNESSES.json.gz' + receipt = PACKAGE / 'RESULT.json' + if args.write: + certificate.write_bytes(gzip.compress(canonical(witnesses), mtime=0)) + receipt.write_text(json.dumps(result, indent=2, sort_keys=True) + '\n') + else: + same_receipt(witnesses, json.loads(gzip.decompress(certificate.read_bytes()))) + same_receipt(result, json.loads(receipt.read_text())) + if args.output: + args.output.write_text(json.dumps(result, indent=2, sort_keys=True) + '\n') + print('PASS_TWO_FULL_EXACT_WIDTH_GATE wide_sites=4524 extra_H1=3163 ratio_upper=10750/13817 new_kappa=false') + + +if __name__ == '__main__': + main() From e654d2fcb953698d9d842b3ac78c93b2cc46d23e Mon Sep 17 00:00:00 2001 From: Ali Romman <226877337+aliromman@users.noreply.github.com> Date: Sun, 25 Oct 2026 01:53:58 -0500 Subject: [PATCH 2/2] Keep isolated mutation copies writable for read-only exports --- research/two-full-exact-width-gate/test_mutations.py | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/research/two-full-exact-width-gate/test_mutations.py b/research/two-full-exact-width-gate/test_mutations.py index 1623e9e8eb..b75c96099b 100644 --- a/research/two-full-exact-width-gate/test_mutations.py +++ b/research/two-full-exact-width-gate/test_mutations.py @@ -24,7 +24,8 @@ def main(): with tempfile.TemporaryDirectory(prefix='two-band-width-mutations-') as temp: root = Path(temp) package = root / 'research' / PACKAGE.name - shutil.copytree(PACKAGE, package, ignore=shutil.ignore_patterns('__pycache__')) + shutil.copytree(PACKAGE, package, copy_function=shutil.copyfile, + ignore=shutil.ignore_patterns('__pycache__')) for name in inputs: target = root / name target.parent.mkdir(parents=True, exist_ok=True)