From e713a7b1b2a2b6378d660444a411d539fb8cacb5 Mon Sep 17 00:00:00 2001 From: armin Date: Fri, 6 Nov 2026 23:07:08 -0500 Subject: [PATCH 1/5] =?UTF-8?q?Prove=20an=20overlap=20floor=20for=20refine?= =?UTF-8?q?d=20recovery=20at=20depth=20t>=3D27=20(no=20=CE=BA)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Answers the first step of #6660 open question 1: every overlap pattern has |fiber(0)| >= F^t (1+(2^d-1) mu_d^(t/(2^d-1))), giving >= 15.78976 F^27 (696 tag bits vs 692) at t=27, with near-attainment by an abstract pattern. Co-Authored-By: Claude Opus 5.5 --- .../refined-recovery-overlap-floor/PROOF.md | 136 ++++++++++ .../refined-recovery-overlap-floor/README.md | 82 ++++++ .../RESULT.json | 140 ++++++++++ .../SOURCES.json | 38 +++ .../refined-recovery-overlap-floor/TASK.json | 89 ++++++ .../VERIFY.json | 36 +++ .../refined-recovery-overlap-floor/verify.py | 253 ++++++++++++++++++ 7 files changed, 774 insertions(+) create mode 100644 research/refined-recovery-overlap-floor/PROOF.md create mode 100644 research/refined-recovery-overlap-floor/README.md create mode 100644 research/refined-recovery-overlap-floor/RESULT.json create mode 100644 research/refined-recovery-overlap-floor/SOURCES.json create mode 100644 research/refined-recovery-overlap-floor/TASK.json create mode 100644 research/refined-recovery-overlap-floor/VERIFY.json create mode 100644 research/refined-recovery-overlap-floor/verify.py diff --git a/research/refined-recovery-overlap-floor/PROOF.md b/research/refined-recovery-overlap-floor/PROOF.md new file mode 100644 index 0000000000..c174964866 --- /dev/null +++ b/research/refined-recovery-overlap-floor/PROOF.md @@ -0,0 +1,136 @@ +# An overlap floor for refined recovery chains at depth t ≥ 27 + +Prepared for apoursh with substantial Anthropic Claude assistance. Apache-2.0. + +## Setting + +All objects are those of Nick Petalas's +[PR6660](https://github.com/CrocSwap/integer-mult-bounds/pull/6660) +(`research/refined-recovery-longer-chains`, head +`b6de532eff668a7daf8f2f98668f97af5af41338`). That package builds on CubeJerry's +PR6327 and uses the 112×8 matrix M of #5444 from +`research/precision-state-frontier/FIXTURE.json`. The chain is z_1 = K(2x), +z_(j+1) = K(U_j z_j), with fixed frames U_j ∈ G = {U ∈ GL_112(ℤ) : MᵀU = Mᵀ}. +The code C = ker_F2(M mod 2) is the self-dual [8,4,4] code, and +F = W_C(13,1)/16 = 51,008,161. + +PR6660 proves that the optimal worst-case fiber is exactly F^t for t ≤ 26 and +strictly larger for t ≥ 27. Its open question 1 asks for the exact optimum at +t ≥ 27, and its suggested first step is to minimize the zero-fiber kernel +formula over overlap patterns. This note bounds that minimum from below for +**every** overlap pattern and every t ≥ 27, and pins it at t = 27. + +We use two results from PR6660 and do not re-prove them: + +* **(Z) Zero fiber, its §5.** With N_j = im_F2(W_j M mod 2), + + |fiber(0)| = Σ_{u ∈ ker} Π_j 7^(8−wt u_j) 6^(wt u_j), + ker = {(u_1,…,u_t) ∈ (F2^8)^t : Σ_j W_j M u_j ≡ 0 (mod 2)}. + +* **(c) Dimension cap, its §6.** Every N_j lies in one fixed binary space of + dimension at most 104. + +## 1. Coset form of the zero fiber + +Since W_j M kills C modulo 2, membership in ker depends only on the cosets +a_j = u_j + C ∈ Q := F2^8/C ≅ F2^4. Grouping (Z) by cosets gives + + |fiber(0)| = Σ_{a ∈ D} Π_j S(a_j), S(a) = Σ_{u ∈ a} 7^(8−wt u) 6^(wt u), + +where D = {(a_j) ∈ Q^t : Σ_j φ_j(a_j) = 0} and φ_j : Q → N_j is the induced +isomorphism. By (c), dim D = 4t − dim(N_1+⋯+N_t) ≥ 4t − 104. + +verify.py computes the 16 coset sums exactly from C, which it derives from M: + +* S(C) = F; +* S(a) = 50,983,170 on the 8 odd-weight cosets; +* S(a) = 50,979,600 on the 7 nonzero even-weight cosets. + +The even-weight cosets together with C form a plane E ⊂ Q of dimension 3. Write +ρ(a) = S(a)/F, so ρ(0) = 1, ρ = ρ₁ = 50983170/F off E, and ρ = ρ₂ = 50979600/F +on E∖0. Then 0 < ρ₂ < ρ₁ < 1, and + + |fiber(0)| = F^t · Σ_{a ∈ D} Π_j ρ(a_j). (1) + +## 2. Theorem + +Let μ_d be the minimum of Π_{x ∈ F2^d∖0} ρ(ℓx) over all linear maps +ℓ : F2^d → Q. For t ≥ 27, every frame sequence, and every 1 ≤ d ≤ 4t − 104, + + |fiber(0)| ≥ F^t · (1 + (2^d − 1) · μ_d^(t/(2^d − 1))). (2) + +For d ≥ 3, μ_d = ρ₂^(2^d − 2^(d−3)), attained exactly by the rank-3 maps onto E. +Also μ_1 = ρ₂ and μ_2 = ρ₂³. Hence the optimal maximum fiber +min_U max_y |fiber(y)| is at least the right side of (2). It is at most +A_t = (13^(8t) + 14·13^(4t) + 1)/16, the identity-frame value of PR6327 (U_j = I is +a valid frame). + +*Proof.* Choose a d-dimensional subspace D′ ⊆ D, possible since dim D ≥ d. +Parametrize it by an injective linear map x ↦ (ℓ_1x,…,ℓ_tx) from F2^d. Every +term of (1) is positive, so + + Σ_{a∈D} Π_j ρ(a_j) ≥ Σ_{x ∈ F2^d} P(x), P(x) = Π_j ρ(ℓ_j x). + +The term x = 0 equals 1. By AM–GM over the 2^d − 1 nonzero x, + + Σ_{x≠0} P(x) ≥ (2^d − 1) (Π_{x≠0} P(x))^(1/(2^d−1)) + = (2^d − 1) (Π_j Π_{x≠0} ρ(ℓ_j x))^(1/(2^d−1)) + ≥ (2^d − 1) μ_d^(t/(2^d−1)). + +*Value of μ_d.* Let ℓ have rank k and image I. Then ℓ hits each point of I +exactly 2^(d−k) times on F2^d, so Π_{x≠0} ρ(ℓx) = (Π_{a∈I∖0} ρ(a))^(2^(d−k)). +verify.py evaluates this exactly for all 67 subspaces I of Q and every d ≤ 8. +In each case the minimum is I = E with k = 3. The general form follows from two +facts verify.py checks exactly: ρ₂ < ρ₁ < 1 and ρ₂⁷ < ρ₁⁸. + +* If k ≤ 3, the product has 2^d − 2^(d−k) ≤ 2^d − 2^(d−3) factors, each at + least ρ₂ and at most 1. So it is at least ρ₂^(2^d − 2^(d−3)), with equality + exactly for I = E. +* If k = 4, so I = Q, the product is (ρ₁⁸ρ₂⁷)^(2^(d−4)), which exceeds + ρ₂^(14·2^(d−4)) = ρ₂^(2^d − 2^(d−3)) because ρ₂⁷ < ρ₁⁸. ∎ + +The perhaps surprising fact ρ₂⁷ < ρ₁⁸, with a ratio 1 − 1.18·10⁻⁷, means a stage +map that collapses a line onto E beats an injective one. A naive analysis that +uses only injective maps gets the constant wrong in the seventh significant digit. + +## 3. Depth 27 + +At t = 27 we have d ≤ 4, and d = 4 is best. Then μ_4 = ρ₂^14 and (2) reads + + |fiber(0)| ≥ F^27 · (1 + 15 ρ₂^(126/5)) ≥ (49343/3125) F^27 = 15.78976 F^27. + +verify.py certifies the rational floor by checking ((L−1)/15)^15 ≤ μ_4^27 +exactly. A control confirms that L + 15·10⁻⁶ fails. So every mode-preserving +frame sequence at depth 27 needs a tag of **at least 696 bits**, compared with +⌈27 log₂ F⌉ = 692 for a hypothetical direct sum, as at t ≤ 26. The identity +frame needs ⌈log₂ A_27⌉ = 796 bits. + +**Near-attainment by an abstract pattern.** Take ℓ_1,…,ℓ_27 : F2^4 → Q of rank 3 +onto E. Their kernels cover 12 nonzero points twice and 3 points once, so they +meet trivially and the map is injective. This pattern gives +Σ_x P(x) = 1 + 12ρ₂^25 + 3ρ₂^26 = 15.789775 (exact rational in verify.py). It +exceeds the floor by less than 10⁻⁴. So among four-dimensional dependency +spaces, the bound is essentially the true minimum of (1). Whether frames in G +can realize this pattern is **not** established. For example, if the first 26 +stages form a direct sum, the 27th coordinate map is forced to be injective. + +## 4. Larger depth + +RESULT.json lists t = 27,…,40 with the best d ≤ 8. For 28 ≤ t ≤ 40, taking d = 8 +already gives |fiber(0)| > 251·F^t. That is about 8 more tag bits than +⌈t log₂ F⌉; RESULT.json records the certified bit count for each t. +Larger d, up to 4t − 104, gives larger bounds, which the table does not +evaluate. Asymptotically, d = 4t − 104 gives roughly 16^(t−26) ρ₂^(7t/8) F^t. + +## Scope + +This is a lower bound for the zero fiber, and hence for the optimal maximum +fiber, of PR6660's exact interface: fixed known frames in G, one precision bit, +unbounded integers and full output access. It is not the exact optimum. +Realizability of the near-optimal pattern and the true maximum fiber at +t ≥ 27 remain open. It supplies no codec, physical tag, caller or restoration +cost. κ, the selected frontier and its five assumptions are unchanged. +PR6660's theorems (Z) and (c) are cited premises at its pinned head, not +replayed; that PR is open at the time of writing. The written proof is +author-checked with exact finite corroboration, and no independent human or +proof-kernel review is claimed. diff --git a/research/refined-recovery-overlap-floor/README.md b/research/refined-recovery-overlap-floor/README.md new file mode 100644 index 0000000000..7d8522cede --- /dev/null +++ b/research/refined-recovery-overlap-floor/README.md @@ -0,0 +1,82 @@ +# An overlap floor for refined recovery at depth t ≥ 27 + +Prepared for apoursh with substantial Anthropic Claude assistance. Apache-2.0. + +**Scoped proof with exact finite corroboration; no κ.** This addresses open +question 1 of Nick Petalas's +[PR6660](https://github.com/CrocSwap/integer-mult-bounds/pull/6660) +(`research/refined-recovery-longer-chains`, head `b6de532e`). PR6660 proves that the +optimal worst-case fiber of refined chains over mode-preserving frames is exactly +F^t for t ≤ 26 and *strictly* larger for t ≥ 27. It suggests minimizing its +zero-fiber kernel formula over overlap patterns at t = 27. This package gives a +floor for **every** overlap pattern and every t ≥ 27: + + |fiber(0)| ≥ F^t · (1 + (2^d − 1) · μ_d^(t/(2^d−1))), 1 ≤ d ≤ 4t − 104, + μ_d = ρ₂^(2^d − 2^(d−3)) (d ≥ 3), ρ₂ = 50979600/51008161. + +| depth t | floor / F^t | tag bits ≥ | ⌈t log₂F⌉ (direct sum) | identity frame ⌈log₂A_t⌉ | +|---:|---:|---:|---:|---:| +| 27 | 15.78976 | **696** | 692 | 796 | +| 28 | 252.51 | 725 | 717 | 825 | +| 30 | 252.26 | 777 | 769 | 885 | +| 40 | 251.03 | 1033 | 1025 | 1181 | + +So the strict inequality of PR6660 is in fact a gap of about four bits at t = 27 +and eight bits from t = 28 on. The optimum lies between this floor and the +identity-frame value A_t. + +**Argument.** +1. PR6660's zero-fiber formula, grouped by cosets of C, becomes a sum over a + binary dependency space D of dimension at least 4t − 104. The summand is a + product of coset ratios ρ ∈ {1, ρ₁, ρ₂}. +2. Restrict to any d-dimensional subspace of D and apply AM–GM over its nonzero + points. +3. The per-stage minimum μ_d is attained by rank-3 stage maps onto the + even-coset plane E, not by injective ones, because ρ₂⁷ < ρ₁⁸ (ratio + 1 − 1.2·10⁻⁷). + +At t = 27 an abstract pattern of 27 such maps reaches 1 + 12ρ₂^25 + 3ρ₂^26, which is +within 10⁻⁴ of the floor. The bound is therefore essentially sharp for +four-dimensional dependency spaces. Whether actual frames realize that pattern is +open. See [PROOF.md](PROOF.md). + +## Reproduce + +From the repository root, CPython 3.12, standard library only: + +```sh +python3.12 -I -W error -B research/refined-recovery-overlap-floor/verify.py +python3.12 -I -O -W error -B research/refined-recovery-overlap-floor/verify.py +python3.12 -B scripts/research_package.py --package research/refined-recovery-overlap-floor +``` + +Each run prints `PASS_REFINED_RECOVERY_OVERLAP_FLOOR` in under a second. It +derives C from the pinned matrix and checks every number stated above in exact +rational arithmetic, including all 67 subspaces of F2^8/C for μ_d (d ≤ 8). It +recomputes RESULT.json and runs two failure controls. + +## Limitations + +PR6660's zero-fiber formula and 104-dimensional cap are cited premises at its +pinned head, which is open and unmerged. This package does not replay them. The +result is a lower bound; the exact maximum fiber at t ≥ 27 remains open. It +supplies no codec, physical tag, caller or restoration cost. κ, the selected +frontier and its five assumptions are unchanged. No independent human or proof-kernel +review is claimed. + +## Open next questions + +1. **Realizable minimum and max fiber at t = 27.** Can frames in G realize a + dependency space whose stage maps are rank-3 maps onto E? If the first 26 + stages form a direct sum, the 27th map is forced to be injective. Is the + maximum fiber equal to the zero fiber there? +2. **Upper side.** Beat the identity-frame bound A_t with one four-dimensional + overlap, by extending PR6660's stage-by-stage box lemma to one coupled pair + of stages. The present window is about 100 bits. + +## Credit + +Nick Petalas's PR6660 supplies the depth law, the zero-fiber formula, the +dimension cap and the open question. CubeJerry's PR6327 supplies the chain model, +F and A_t. zxv's #5444 supplies M. AM–GM and the coset structure of the extended +Hamming code are classical. diff --git a/research/refined-recovery-overlap-floor/RESULT.json b/research/refined-recovery-overlap-floor/RESULT.json new file mode 100644 index 0000000000..e5af8c22c3 --- /dev/null +++ b/research/refined-recovery-overlap-floor/RESULT.json @@ -0,0 +1,140 @@ +{ + "rho1": "50983170/51008161", + "rho2": "50979600/51008161", + "mu_d": { + "1": "50979600/51008161", + "2": "132491882463990336000000/132714690473637451277281", + "3": "894900941243498747987651419558649280921600000000000000/898416383679163135162438552548107225177152888861914721", + "4": "800847694638499998472233863757595868617486486841136281833584754575020753745346560000000000000000000000000000/807151998463145264180418887843724631692904231387501185235528301824111562114506101860040358812625482276507841" + }, + "t27_floor_over_F27": "49343/3125", + "t27_abstract_attained_over_F27": 15.789774623144325, + "table": [ + { + "t": 27, + "d": 4, + "floor_over_F_t": "49343/3125", + "floor_over_F_t_float": 15.78976, + "min_tag_bits_at_least": 696, + "direct_sum_bits_t_log2F": 692, + "identity_frame_bits_log2_A_t": 796 + }, + { + "t": 28, + "d": 8, + "floor_over_F_t": "25251109/100000", + "floor_over_F_t_float": 252.51109, + "min_tag_bits_at_least": 725, + "direct_sum_bits_t_log2F": 717, + "identity_frame_bits_log2_A_t": 825 + }, + { + "t": 29, + "d": 8, + "floor_over_F_t": "50477483/200000", + "floor_over_F_t_float": 252.387415, + "min_tag_bits_at_least": 751, + "direct_sum_bits_t_log2F": 743, + "identity_frame_bits_log2_A_t": 855 + }, + { + "t": 30, + "d": 8, + "floor_over_F_t": "12613187/50000", + "floor_over_F_t_float": 252.26374, + "min_tag_bits_at_least": 777, + "direct_sum_bits_t_log2F": 769, + "identity_frame_bits_log2_A_t": 885 + }, + { + "t": 31, + "d": 8, + "floor_over_F_t": "50428013/200000", + "floor_over_F_t_float": 252.140065, + "min_tag_bits_at_least": 802, + "direct_sum_bits_t_log2F": 794, + "identity_frame_bits_log2_A_t": 914 + }, + { + "t": 32, + "d": 8, + "floor_over_F_t": "50403329/200000", + "floor_over_F_t_float": 252.016645, + "min_tag_bits_at_least": 828, + "direct_sum_bits_t_log2F": 820, + "identity_frame_bits_log2_A_t": 944 + }, + { + "t": 33, + "d": 8, + "floor_over_F_t": "10075729/40000", + "floor_over_F_t_float": 251.893225, + "min_tag_bits_at_least": 853, + "direct_sum_bits_t_log2F": 845, + "identity_frame_bits_log2_A_t": 973 + }, + { + "t": 34, + "d": 8, + "floor_over_F_t": "50353961/200000", + "floor_over_F_t_float": 251.769805, + "min_tag_bits_at_least": 879, + "direct_sum_bits_t_log2F": 871, + "identity_frame_bits_log2_A_t": 1003 + }, + { + "t": 35, + "d": 8, + "floor_over_F_t": "50329277/200000", + "floor_over_F_t_float": 251.646385, + "min_tag_bits_at_least": 905, + "direct_sum_bits_t_log2F": 897, + "identity_frame_bits_log2_A_t": 1033 + }, + { + "t": 36, + "d": 8, + "floor_over_F_t": "12576161/50000", + "floor_over_F_t_float": 251.52322, + "min_tag_bits_at_least": 930, + "direct_sum_bits_t_log2F": 922, + "identity_frame_bits_log2_A_t": 1062 + }, + { + "t": 37, + "d": 8, + "floor_over_F_t": "1256999/5000", + "floor_over_F_t_float": 251.3998, + "min_tag_bits_at_least": 956, + "direct_sum_bits_t_log2F": 948, + "identity_frame_bits_log2_A_t": 1092 + }, + { + "t": 38, + "d": 8, + "floor_over_F_t": "50255327/200000", + "floor_over_F_t_float": 251.276635, + "min_tag_bits_at_least": 981, + "direct_sum_bits_t_log2F": 973, + "identity_frame_bits_log2_A_t": 1121 + }, + { + "t": 39, + "d": 8, + "floor_over_F_t": "10046149/40000", + "floor_over_F_t_float": 251.153725, + "min_tag_bits_at_least": 1007, + "direct_sum_bits_t_log2F": 999, + "identity_frame_bits_log2_A_t": 1151 + }, + { + "t": 40, + "d": 8, + "floor_over_F_t": "1568941/6250", + "floor_over_F_t_float": 251.03056, + "min_tag_bits_at_least": 1033, + "direct_sum_bits_t_log2F": 1025, + "identity_frame_bits_log2_A_t": 1181 + } + ] +} diff --git a/research/refined-recovery-overlap-floor/SOURCES.json b/research/refined-recovery-overlap-floor/SOURCES.json new file mode 100644 index 0000000000..1f9c9e6cc6 --- /dev/null +++ b/research/refined-recovery-overlap-floor/SOURCES.json @@ -0,0 +1,38 @@ +{ + "schema_version": 1, + "base_commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "d59b5035e7b4cbaa9d688a1d32dd0d6eb79c466a", + "sha256": "9b8d0eea95b3bf0dfcb7938a732a6439b87a2685dec2a5ab9e525b3b34debbfa" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec", + "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81" + }, + { + "path": "research/precision-state-frontier/FIXTURE.json", + "usage": "input", + "git_blob": "0aa9f7816378c3eb11ec2e3d63ed9e85cfaa893c", + "sha256": "2ca4d7550fcae5b757ec500f87aee1d2ef9f64b59e4abe2bda93319521304af8" + }, + { + "path": "research/refined-recovery-longer-chains/PROOF.md", + "usage": "provenance", + "pin": "head:b6de532eff668a7daf8f2f98668f97af5af41338:research/refined-recovery-longer-chains/PROOF.md", + "git_blob": "34a5f56d608c17dec7acca938fb01d17a74c25c3", + "sha256": "9c67877b06dcdf24211f2d2ff23553fa07d54f476598382af0527f6b4ba2c9e9" + }, + { + "path": "research/refined-recovery-longer-chains/README.md", + "usage": "provenance", + "pin": "head:b6de532eff668a7daf8f2f98668f97af5af41338:research/refined-recovery-longer-chains/README.md", + "git_blob": "3fd64c60a00f2d07de2d2aaecfc35309f00046fd", + "sha256": "e700cf4344daec060003a192c5edb268ee7a14a3b15e1b7a42dbef6301aa5a3a" + } + ] +} diff --git a/research/refined-recovery-overlap-floor/TASK.json b/research/refined-recovery-overlap-floor/TASK.json new file mode 100644 index 0000000000..54f6ccb638 --- /dev/null +++ b/research/refined-recovery-overlap-floor/TASK.json @@ -0,0 +1,89 @@ +{ + "schema_version": 1, + "task_id": "uniform-transfer-audit", + "priority_revision": 8, + "base_commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a", + "original_card": { + "id": "uniform-transfer-audit", + "question": "Can one of the selected record's five inherited assumptions be proved at its actual caller?", + "starting_points": [ + "docs/research/current-priorities.md", + "docs/research/research-family-status.md", + "certificates/selected-result.json", + "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md" + ], + "methods": [ + "Construct and independently check one source-bound instance of the stated first experiment.", + "Seek an exact counterexample or target-specific complete-budget obstruction to that same proposed change." + ], + "acceptance_gate": "Identify the proposition and what would change downstream; do not equate a finite replay with a universal proof.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_selected_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read revision 8, the selected review and live exact-source handoffs. Then follow this card's bounded first_experiment.", + "scope": "Source-bound orientation only, not a supplier replay or theorem proof." + }, + "first_experiment": "Choose one assumption ID (native_all_columns, owned_erasure, compiler, precision_tape, analytic_recovery), one quantified implication and exact dependency closure. Check current handoffs, including #5625 row reentry and #5707 root-prefix lowering, without treating their partial scope as the whole theorem. Prove or falsify that implication with a caller-bound argument; stop at the chosen obligation. Finite tests or root digits do not discharge an all-size statement.", + "bottleneck_link": "Judge the actual current supplier contract and complete signed target/paid bill; frozen-profile ceilings require an applicability proof.", + "allowed_variations": [ + "One exact source head, helper/cut region or quantified proposition and changed hypothesis; check live handoffs first. Different seeds are not different scopes." + ], + "scope_change_triggers": [ + "Changing source head, helper/cut domain, operation alphabet or caller boundary without recording the new scope.", + "Treating an archived proposal or local numerical pass as complete supplier admission." + ], + "overlap_terms": [ + "native_all_columns", + "owned_erasure", + "compiler", + "precision_tape", + "analytic_recovery" + ], + "existing_checks": [ + { + "scope": "PR #4100: proposed unconditional construction and finite checks, without independent acceptance.", + "evidence": "research/unconditional-batched-crt/README.md", + "remaining": "Independent proof audit of one caller-bound all-size implication; all other premises remain explicit.", + "status": "author-checked", + "source_commit": "337d04939571a637aeab54a0f58f54fde811663a", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "Selected PR5599: complete helper-subspace construction and independent caller replay; five framework assumptions remain.", + "evidence": "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md", + "remaining": "The next experiment must identify uncovered source-specific work. Successor archive intake does not transfer this admission.", + "status": "reviewed", + "source_commit": "09dd0965711ca7eeb169057a420abab1c9052137", + "selected_record_sha256": "2a0220e866417774606e0f991e41b9c1d26b1f43b97857238cf478dbc7d330b5" + } + ] + }, + "scope_status": "changed", + "actual_scope": "Quantitative lower bound on the optimal worst-case recovery fiber of PR6660 refined chains at every depth t>=27, from its zero-fiber kernel formula: |fiber(0)| >= F^t (1+(2^d-1) mu_d^(t/(2^d-1))) for 1<=d<=4t-104, with mu_d exact; at t=27 this is > 15.7897 F^27, i.e. at least 696 tag bits versus 692 for a direct sum.", + "scope_change_reason": "Answers the first step of PR6660 open question 1 (minimize the zero-fiber kernel sum at t=27 over overlap patterns) with a bound for every overlap pattern. Like its predecessor this is precision-state accounting in the analytic_recovery interface, not a caller-bound discharge of a selected assumption.", + "bottleneck_link": "Side result for exact history accounting in the inherited rounded interface; it changes no supplier invoice.", + "budget_minutes": 60, + "stop_rule": "Stop at the all-pattern zero-fiber floor with an exact t=27 constant and its near-attainment by an abstract pattern; leave the exact max-fiber optimum and realizability by frames open.", + "outcome": "completed", + "evidence": "PROOF.md; verify.py (exact rational arithmetic, normal and optimized Python) writes and rechecks RESULT.json.", + "author": "apoursh", + "ai_assistance": "Anthropic Claude (Claude Code) found the argument, wrote the verifier and ran the checks under apoursh direction. Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Is the t=27 optimum (max fiber) equal to its zero-fiber value, and what is the minimum of the zero fiber over frame sequences that are actually realizable?", + "why_it_matters": "Together with this floor it would give the exact depth-27 tag size.", + "first_step": "Decide whether frames in G can realize a dependency space whose 27 coordinate maps are rank-3 maps onto the even-coset plane E, the near-optimal abstract pattern here.", + "blocked_by": "With a direct-sum prefix of 26 stages the 27th coordinate map is forced to be injective; other realizable overlap patterns are not classified." + }, + { + "question": "Can the identity-frame upper bound A_t be improved at t>=27 by a frame sequence with a single 4-dimensional overlap?", + "why_it_matters": "The present window between floor and A_t is about 100 bits.", + "first_step": "Extend PR6660 stage-by-stage box counting to one coupled pair of stages.", + "blocked_by": "Coupled stage cosets break the per-stage box lemma." + } + ] +} diff --git a/research/refined-recovery-overlap-floor/VERIFY.json b/research/refined-recovery-overlap-floor/VERIFY.json new file mode 100644 index 0000000000..391d78fd94 --- /dev/null +++ b/research/refined-recovery-overlap-floor/VERIFY.json @@ -0,0 +1,36 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/precision-state-frontier/FIXTURE.json" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 60, + "checks": "Fixture hash; C=[8,4,4] self-dual from M; exact coset sums and the even-coset plane E; rho2^7=3; certified t=27 floor 49343/3125; abstract near-attaining pattern; t=27..40 table against A_t; RESULT.json recomputation; controls." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 60, + "checks": "The same explicit checks under optimized Python." + } + ] +} diff --git a/research/refined-recovery-overlap-floor/verify.py b/research/refined-recovery-overlap-floor/verify.py new file mode 100644 index 0000000000..4717abc96f --- /dev/null +++ b/research/refined-recovery-overlap-floor/verify.py @@ -0,0 +1,253 @@ +"""Exact checks for the overlap floor on refined recovery chains (stdlib only). + +Prints PASS_REFINED_RECOVERY_OVERLAP_FLOOR on success. +""" +import hashlib +import json +import math +import pathlib +from fractions import Fraction + +HERE = pathlib.Path(__file__).resolve().parent +FIXTURE = HERE.parent / "precision-state-frontier" / "FIXTURE.json" +FIXTURE_SHA = "2ca4d7550fcae5b757ec500f87aee1d2ef9f64b59e4abe2bda93319521304af8" +RESULT = HERE / "RESULT.json" +N, MODES = 112, 8 +F = (13**8 + 14 * 13**4 + 1) // 16 +DIM_CAP = 104 # #6660 Theorem (c): every N_j lies in one space of dimension <= 104 + + +def fail(msg): + raise SystemExit("FAIL: " + msg) + + +def check(cond, msg): + if not cond: + fail(msg) + + +def wt(u): + return bin(u).count("1") + + +def load_rows(): + raw = FIXTURE.read_bytes() + check(hashlib.sha256(raw).hexdigest() == FIXTURE_SHA, "fixture hash") + cols = json.loads(raw)["mode_columns"] + check(len(cols) == MODES and all(len(c) == N for c in cols), "fixture shape") + return [tuple(cols[j][i] for j in range(MODES)) for i in range(N)] + + +def code_from_rows(rows): + """C = {q in F2^8 : M q = 0 mod 2}, as 8-bit masks.""" + code = [q for q in range(256) + if all(sum(r[k] for k in range(MODES) if q >> k & 1) % 2 == 0 for r in rows)] + check(len(code) == 16, "|C| = 16") + check(all(wt(a & b) % 2 == 0 for a in code for b in code), "C self-orthogonal (so self-dual)") + check(sorted(wt(c) for c in code) == [0] + [4] * 14 + [8], "C is the [8,4,4] code") + return code + + +def coset_ratios(code): + """rho(a) = S(a)/F on the 16 cosets, S(a) = sum_{u in a} 7^(8-wt) 6^wt.""" + w = lambda u: 7 ** (8 - wt(u)) * 6 ** wt(u) + reps = sorted({min(u ^ c for c in code) for u in range(256)}) + check(len(reps) == 16, "16 cosets") + S = {a: sum(w(a ^ c) for c in code) for a in reps} + check(S[0] == F, "S(C) = W_C(7,6) = F") + rho = {a: Fraction(S[a], F) for a in reps} + odd = {S[a] for a in reps if wt(a) % 2} + even = {S[a] for a in reps if a and wt(a) % 2 == 0} + check(odd == {50983170} and even == {50979600}, "two nonzero coset sums") + return reps, rho, Fraction(50983170, F), Fraction(50979600, F) + + +def quotient_subspaces(code, reps): + """All subspaces of F2^8/C, as frozensets of coset representatives.""" + rep = lambda u: min(u ^ c for c in code) + subs = {frozenset([0])} + frontier = list(subs) + while frontier: + nxt = [] + for s in frontier: + for a in reps: + if a in s: + continue + t = frozenset(s | {rep(x ^ a) for x in s}) + if t not in subs: + subs.add(t) + nxt.append(t) + frontier = nxt + check(sorted(len(s) for s in subs).count(8) == 15 and len(subs) == 67, "67 subspaces of F2^4") + return subs + + +def mu(d, subs, rho): + """min over linear l: F2^d -> F2^8/C of prod_{x != 0} rho(l x). + + A rank-k map with image I hits each point of I exactly 2^(d-k) times on + F2^d, so the product is (prod_{a in I, a != 0} rho(a))^(2^(d-k)). + """ + best = None + for s in subs: + k = len(s).bit_length() - 1 + if k > d: + continue + p = Fraction(1) + for a in s: + if a: + p *= rho[a] + val = p ** (2 ** (d - k)) + if best is None or val < best[0]: + best = (val, k, s) + return best + + +def certified_floor(t, d, m, places=6): + """Largest L = 1 + (2^d - 1) * y with y = floor(10^places * m^(t/(2^d-1)))/10^places. + + Returned exactly: ((L - 1)/(2^d - 1))^(2^d - 1) <= m^t is checked. + """ + n = 2 ** d - 1 + target = m ** t + lo, hi = 0, 10 ** places + while lo < hi: + mid = (lo + hi + 1) // 2 + if Fraction(mid, 10 ** places) ** n <= target: + lo = mid + else: + hi = mid - 1 + y = Fraction(lo, 10 ** places) + check(y ** n <= target, "certified root") + return 1 + n * y + + +def zero_fiber_ratio(maps, rho, d): + """sum_{x in F2^d} prod_j rho(l_j x) for maps given as images of the basis.""" + total = Fraction(0) + for x in range(2 ** d): + p = Fraction(1) + for basis_imgs, rep in maps: + a = 0 + for i in range(d): + if x >> i & 1: + a ^= basis_imgs[i] + p *= rho[rep(a)] + total += p + return total + + +def main(): + rows = load_rows() + code = code_from_rows(rows) + reps, rho, r1, r2 = coset_ratios(code) + rep = lambda u: min(u ^ c for c in code) + even = frozenset(a for a in reps if wt(a) % 2 == 0) + check(len(even) == 8, "even cosets form E (3-dimensional)") + subs = quotient_subspaces(code, reps) + check(even in subs, "E is a subspace") + check(r2 < r1 < 1, "0 < rho2 < rho1 < 1") + check(r2 ** 7 < r1 ** 8, "rho2^7 < rho1^8: a map onto E beats an injective map") + + # mu_d: the minimizer is the rank-3 map onto E for every d >= 3 + mus = {} + for d in range(1, 9): + val, k, s = mu(d, subs, rho) + mus[d] = val + if d >= 3: + check(k == 3 and s == even and val == r2 ** (2 ** d - 2 ** (d - 3)), "mu_%d closed form" % d) + check(mus[1] == r2 and mus[2] == r2 ** 3, "mu_1, mu_2") + + # Theorem at t = 27, d = 4 + L27 = certified_floor(27, 4, mus[4]) + check(L27 == Fraction(157898, 10000) or L27 > Fraction(15789, 1000), "t=27 floor > 15.789") + check(L27 > 15, "t=27 floor exceeds 15") + + # Near-attainment of the d = 4 bound by an abstract configuration (not frames): + # 27 rank-3 maps onto E with kernels distributed 2,2,...,2,1,1,1 over the 15 lines. + # Coordinates: F2^8/C basis b0..b3 with E spanned by three even cosets. + ev = [a for a in sorted(even) if a] + e_basis = [] + for a in ev: + span = {0} + for b in e_basis: + span |= {s ^ b for s in span} + span = {rep(s) for s in span} + if a not in span: + e_basis.append(a) + check(len(e_basis) == 3, "basis of E") + maps = [] + lines = list(range(1, 16)) + kernels = lines * 2 + kernels = kernels[:27] + for kvec in kernels: + # choose l: F2^4 -> E with kernel spanned by kvec: send a basis of a complement to e_basis + # build basis {kvec, c1, c2, c3} of F2^4 and images {0, e1, e2, e3} + basis = [kvec] + for v in (1, 2, 4, 8): + span = {0} + for b in basis: + span |= {s ^ b for s in span} + if v not in span and len(basis) < 4: + basis.append(v) + imgs_on_basis = [0] + e_basis + # express standard basis vectors in terms of `basis` + std_imgs = [] + for v in (1, 2, 4, 8): + for coeffs in range(16): + s = 0 + img = 0 + for i in range(4): + if coeffs >> i & 1: + s ^= basis[i] + img ^= imgs_on_basis[i] + if s == v: + std_imgs.append(rep(img)) + break + maps.append((std_imgs, rep)) + attained = zero_fiber_ratio(maps, rho, 4) + check(attained == 1 + 12 * r2 ** 25 + 3 * r2 ** 26, "abstract configuration value") + check(attained > L27 and attained - L27 < Fraction(1, 10 ** 4), "d=4 AM-GM bound nearly attained") + + # Table for t = 27..40: best certified d, floor, bits; identity-frame upper bound A_t + table = [] + for t in range(27, 41): + best = None + for d in range(1, min(4 * t - DIM_CAP, 8) + 1): + L = certified_floor(t, d, mus[d] if d in mus else r2 ** (2 ** d - 2 ** (d - 3))) + if best is None or L > best[1]: + best = (d, L) + d, L = best + lower = F ** t * L + A_t = (13 ** (8 * t) + 14 * 13 ** (4 * t) + 1) // 16 + check(lower < A_t, "floor below identity-frame fiber A_%d" % t) + bits_lo = math.ceil(math.log2(lower.numerator) - math.log2(lower.denominator) - 1e-9) + check(Fraction(2) ** (bits_lo - 1) < lower, "certified bit floor t=%d" % t) + table.append({ + "t": t, "d": d, "floor_over_F_t": str(L), "floor_over_F_t_float": float(L), + "min_tag_bits_at_least": bits_lo, + "direct_sum_bits_t_log2F": math.ceil(t * math.log2(F)), + "identity_frame_bits_log2_A_t": math.ceil(math.log2(A_t)), + }) + check(table[0]["d"] == 4, "t=27 uses d=4") + + result = { + "rho1": str(r1), "rho2": str(r2), + "mu_d": {str(d): str(mus[d]) for d in (1, 2, 3, 4)}, + "t27_floor_over_F27": str(L27), + "t27_abstract_attained_over_F27": float(attained), + "table": table, + } + if RESULT.exists(): + check(json.loads(RESULT.read_text()) == result, "RESULT.json matches recomputation") + else: + RESULT.write_text(json.dumps(result, indent=1) + "\n") + + # controls: a wrong ratio or a too-large floor must fail + check(not (r1 ** 8 < r2 ** 7), "control: ordering is strict the other way") + check(not (((L27 + Fraction(15, 10 ** 6) - 1) / 15) ** 15 <= mus[4] ** 27), "control: floor is the certified maximum at 6 places") + print("PASS_REFINED_RECOVERY_OVERLAP_FLOOR") + + +if __name__ == "__main__": + main() From e877fa476d915c32c8f511b5739ce8198a2aecf9 Mon Sep 17 00:00:00 2001 From: armin Date: Fri, 6 Nov 2026 23:17:55 -0500 Subject: [PATCH 2/5] Drop unreachable fork-head provenance pins; cite #6660 head in README Co-Authored-By: Claude Opus 5.5 --- research/refined-recovery-overlap-floor/README.md | 6 ++++-- .../refined-recovery-overlap-floor/SOURCES.json | 14 -------------- 2 files changed, 4 insertions(+), 16 deletions(-) diff --git a/research/refined-recovery-overlap-floor/README.md b/research/refined-recovery-overlap-floor/README.md index 7d8522cede..b51ebf4950 100644 --- a/research/refined-recovery-overlap-floor/README.md +++ b/research/refined-recovery-overlap-floor/README.md @@ -57,8 +57,10 @@ recomputes RESULT.json and runs two failure controls. ## Limitations -PR6660's zero-fiber formula and 104-dimensional cap are cited premises at its -pinned head, which is open and unmerged. This package does not replay them. The +PR6660's zero-fiber formula and 104-dimensional cap are cited premises at head +`b6de532eff668a7daf8f2f98668f97af5af41338`, which is open and unmerged. Its +fork commit is not reachable from this repository, so SOURCES.json does not pin +it. This package does not replay those premises. The result is a lower bound; the exact maximum fiber at t ≥ 27 remains open. It supplies no codec, physical tag, caller or restoration cost. κ, the selected frontier and its five assumptions are unchanged. No independent human or proof-kernel diff --git a/research/refined-recovery-overlap-floor/SOURCES.json b/research/refined-recovery-overlap-floor/SOURCES.json index 1f9c9e6cc6..ae5689199c 100644 --- a/research/refined-recovery-overlap-floor/SOURCES.json +++ b/research/refined-recovery-overlap-floor/SOURCES.json @@ -19,20 +19,6 @@ "usage": "input", "git_blob": "0aa9f7816378c3eb11ec2e3d63ed9e85cfaa893c", "sha256": "2ca4d7550fcae5b757ec500f87aee1d2ef9f64b59e4abe2bda93319521304af8" - }, - { - "path": "research/refined-recovery-longer-chains/PROOF.md", - "usage": "provenance", - "pin": "head:b6de532eff668a7daf8f2f98668f97af5af41338:research/refined-recovery-longer-chains/PROOF.md", - "git_blob": "34a5f56d608c17dec7acca938fb01d17a74c25c3", - "sha256": "9c67877b06dcdf24211f2d2ff23553fa07d54f476598382af0527f6b4ba2c9e9" - }, - { - "path": "research/refined-recovery-longer-chains/README.md", - "usage": "provenance", - "pin": "head:b6de532eff668a7daf8f2f98668f97af5af41338:research/refined-recovery-longer-chains/README.md", - "git_blob": "3fd64c60a00f2d07de2d2aaecfc35309f00046fd", - "sha256": "e700cf4344daec060003a192c5edb268ee7a14a3b15e1b7a42dbef6301aa5a3a" } ] } From b8d2f4599870a6f30ab2df661ae229df91934c33 Mon Sep 17 00:00:00 2001 From: armin Date: Fri, 6 Nov 2026 23:23:37 -0500 Subject: [PATCH 3/5] Realize the near-optimal depth-27 pattern with explicit frames FRAMES27.json gives 27 mode-preserving frames whose zero fiber is exactly (1+12rho2^25+3rho2^26) F^27, pinning min |fiber(0)| at t=27 to [15.78976, 15.789775] F^27. Co-Authored-By: Claude Opus 5.5 --- .../FRAMES27.json | 6490 +++++++++++++++++ .../refined-recovery-overlap-floor/PROOF.md | 41 +- .../refined-recovery-overlap-floor/README.md | 29 +- .../refined-recovery-overlap-floor/TASK.json | 12 +- .../VERIFY.json | 2 +- .../build_frames.py | 129 + .../refined-recovery-overlap-floor/verify.py | 67 + 7 files changed, 6747 insertions(+), 23 deletions(-) create mode 100644 research/refined-recovery-overlap-floor/FRAMES27.json create mode 100644 research/refined-recovery-overlap-floor/build_frames.py diff --git a/research/refined-recovery-overlap-floor/FRAMES27.json b/research/refined-recovery-overlap-floor/FRAMES27.json new file mode 100644 index 0000000000..0cefb920af --- /dev/null +++ b/research/refined-recovery-overlap-floor/FRAMES27.json @@ -0,0 +1,6490 @@ +{ +"V_columns_sparse": [ +[ +{}, +{}, +{}, +{} +], +[ +{ +"10": 1, +"103": 1, +"106": 1, +"108": 1, +"11": -10, +"110": 1, +"13": -9, +"15": 1, +"18": 1, +"22": 1, +"25": -15, +"27": 1, +"28": 1, +"3": 7, +"30": 1, +"34": 1, +"36": 1, +"37": 1, +"43": 1, +"44": 1, +"46": 1, +"5": -12, +"50": 1, +"51": 1, +"55": 1, +"56": 1, +"6": 9, +"60": 1, +"61": 1, +"63": 1, +"65": 1, +"66": 1, +"67": 1, +"68": 1, +"69": 1, +"7": 1, +"70": 1, +"73": 1, +"76": 1, +"77": 1, +"78": 1, +"8": -12, +"81": 1, +"85": 1, +"86": 1, +"87": 1, +"88": 1, +"89": 1, +"90": 1, +"91": 1, +"92": 1, +"94": 1, +"95": 1, +"97": 1, +"98": 1 +}, +{ +"100": 1, +"101": 1, +"102": 1, +"103": 1, +"104": 1, +"105": 1, +"106": 1, +"107": 1, +"108": 1, +"109": 1, +"11": -21, +"13": -18, +"14": 1, +"15": 1, +"16": 1, +"20": 1, +"22": 1, +"24": 1, +"25": -15, +"28": 1, +"29": 1, +"3": 24, +"31": 1, +"33": 1, +"34": 1, +"35": 1, +"36": 1, +"37": 1, +"38": 1, +"41": 1, +"44": 1, +"45": 1, +"47": 1, +"48": 1, +"49": 1, +"5": -25, +"51": 1, +"54": 1, +"55": 1, +"57": 1, +"59": 1, +"6": 10, +"62": 1, +"63": 1, +"7": 6, +"70": 1, +"71": 1, +"72": 1, +"73": 1, +"74": 1, +"77": 1, +"78": 1, +"8": -18, +"80": 1, +"81": 1, +"82": 1, +"83": 1, +"87": 1, +"89": 1, +"9": 1, +"95": 1, +"99": 1 +}, +{ +"103": 1, +"104": 1, +"105": 1, +"107": 1, +"108": 1, +"11": -17, +"110": 1, +"12": 1, +"13": -5, +"14": 1, +"15": 1, +"18": 1, +"24": 1, +"25": -12, +"26": 1, +"27": 1, +"28": 1, +"29": 1, +"3": 6, +"30": 1, +"32": 1, +"33": 1, +"38": 1, +"40": 1, +"42": 1, +"45": 1, +"5": -15, +"50": 1, +"52": 1, +"55": 1, +"56": 1, +"57": 1, +"58": 1, +"6": 3, +"60": 1, +"61": 1, +"63": 1, +"64": 1, +"66": 1, +"68": 1, +"69": 1, +"7": 2, +"71": 1, +"72": 1, +"73": 1, +"74": 1, +"76": 1, +"8": -16, +"80": 1, +"82": 1, +"84": 1, +"85": 1, +"86": 1, +"9": 1, +"90": 1, +"91": 1, +"94": 1, +"95": 1, +"97": 1, +"98": 1 +}, +{ +"10": 1, +"100": 1, +"103": 1, +"105": 1, +"107": 1, +"108": 1, +"109": 1, +"11": -14, +"111": 1, +"12": 1, +"13": -13, +"14": 1, +"15": 1, +"20": 1, +"22": 1, +"23": 1, +"24": 1, +"25": -17, +"29": 1, +"3": 14, +"30": 1, +"34": 1, +"35": 1, +"36": 1, +"38": 1, +"39": 1, +"41": 1, +"42": 1, +"46": 1, +"49": 1, +"5": -17, +"50": 1, +"52": 1, +"56": 1, +"58": 1, +"6": 13, +"61": 1, +"63": 1, +"65": 1, +"68": 1, +"7": 3, +"71": 1, +"72": 1, +"73": 1, +"76": 1, +"77": 1, +"79": 1, +"8": -19, +"83": 1, +"84": 1, +"85": 1, +"86": 1, +"87": 1, +"89": 1, +"91": 1, +"93": 1, +"95": 1, +"96": 1, +"97": 1 +} +], +[ +{ +"10": 1, +"100": 1, +"102": 1, +"103": 1, +"104": 1, +"106": 1, +"108": 1, +"109": 1, +"11": -21, +"110": 1, +"111": 1, +"12": 1, +"13": -2, +"14": 1, +"15": 1, +"16": 1, +"17": 1, +"19": 1, +"21": 1, +"24": 1, +"25": -6, +"3": 8, +"32": 1, +"33": 1, +"34": 1, +"35": 1, +"36": 1, +"38": 1, +"40": 1, +"47": 1, +"48": 1, +"49": 1, +"5": -19, +"50": 1, +"54": 1, +"56": 1, +"58": 1, +"6": -8, +"60": 1, +"62": 1, +"64": 1, +"65": 1, +"67": 1, +"69": 1, +"7": -3, +"70": 1, +"71": 1, +"73": 1, +"74": 1, +"75": 1, +"77": 1, +"78": 1, +"79": 1, +"8": -13, +"80": 1, +"84": 1, +"87": 1, +"89": 1, +"91": 1, +"94": 1, +"96": 1, +"97": 1, +"99": 1 +}, +{ +"100": 1, +"103": 1, +"105": 1, +"106": 1, +"107": 1, +"108": 1, +"109": 1, +"11": -12, +"110": 1, +"13": -20, +"14": 1, +"17": 1, +"19": 1, +"20": 1, +"22": 1, +"24": 1, +"25": -22, +"27": 1, +"3": 20, +"30": 1, +"32": 1, +"34": 1, +"36": 1, +"38": 1, +"39": 1, +"40": 1, +"41": 1, +"44": 1, +"45": 1, +"46": 1, +"47": 1, +"49": 1, +"5": -16, +"53": 1, +"54": 1, +"56": 1, +"57": 1, +"6": 19, +"61": 1, +"62": 1, +"65": 1, +"67": 1, +"68": 1, +"7": 3, +"70": 1, +"72": 1, +"73": 1, +"75": 1, +"77": 1, +"79": 1, +"8": -18, +"80": 1, +"81": 1, +"84": 1, +"89": 1, +"9": 1, +"90": 1, +"96": 1, +"98": 1, +"99": 1 +}, +{ +"10": 1, +"100": 1, +"101": 1, +"103": 1, +"105": 1, +"108": 1, +"11": -12, +"110": 1, +"111": 1, +"13": -18, +"15": 1, +"16": 1, +"19": 1, +"22": 1, +"24": 1, +"25": -17, +"26": 1, +"27": 1, +"29": 1, +"3": 18, +"30": 1, +"35": 1, +"36": 1, +"37": 1, +"38": 1, +"41": 1, +"44": 1, +"5": -21, +"50": 1, +"51": 1, +"52": 1, +"53": 1, +"54": 1, +"55": 1, +"56": 1, +"58": 1, +"59": 1, +"6": 18, +"63": 1, +"64": 1, +"7": 9, +"70": 1, +"71": 1, +"73": 1, +"8": -15, +"82": 1, +"83": 1, +"84": 1, +"85": 1, +"86": 1, +"88": 1, +"92": 1, +"93": 1, +"95": 1, +"99": 1 +}, +{ +"100": 1, +"101": 1, +"103": 1, +"104": 1, +"108": 1, +"11": -14, +"110": 1, +"13": -9, +"15": 1, +"16": 1, +"17": 1, +"18": 1, +"20": 1, +"24": 1, +"25": -15, +"26": 1, +"27": 1, +"28": 1, +"3": 12, +"31": 1, +"32": 1, +"38": 1, +"39": 1, +"40": 1, +"41": 1, +"43": 1, +"45": 1, +"46": 1, +"5": -16, +"53": 1, +"54": 1, +"58": 1, +"59": 1, +"6": 7, +"62": 1, +"63": 1, +"67": 1, +"69": 1, +"7": 1, +"72": 1, +"73": 1, +"74": 1, +"76": 1, +"77": 1, +"78": 1, +"8": -15, +"82": 1, +"87": 1, +"89": 1, +"9": 1, +"90": 1, +"91": 1, +"92": 1, +"93": 1, +"94": 1, +"96": 1, +"97": 1, +"98": 1 +} +], +[ +{ +"100": 1, +"101": 1, +"102": 1, +"104": 1, +"107": 1, +"108": 1, +"109": 1, +"11": -20, +"111": 1, +"12": 1, +"13": -12, +"14": 1, +"24": 1, +"25": -14, +"26": 1, +"27": 1, +"29": 1, +"3": 13, +"30": 1, +"31": 1, +"33": 1, +"36": 1, +"37": 1, +"40": 1, +"43": 1, +"44": 1, +"45": 1, +"46": 1, +"48": 1, +"5": -18, +"52": 1, +"54": 1, +"55": 1, +"57": 1, +"59": 1, +"6": 6, +"60": 1, +"61": 1, +"62": 1, +"64": 1, +"65": 1, +"66": 1, +"68": 1, +"69": 1, +"7": 5, +"72": 1, +"75": 1, +"76": 1, +"77": 1, +"78": 1, +"79": 1, +"8": -16, +"80": 1, +"82": 1, +"83": 1, +"85": 1, +"87": 1, +"88": 1, +"9": 1, +"91": 1, +"92": 1, +"94": 1, +"97": 1 +}, +{ +"10": 1, +"101": 1, +"104": 1, +"105": 1, +"107": 1, +"108": 1, +"109": 1, +"11": -16, +"110": 1, +"111": 1, +"13": -3, +"14": 1, +"19": 1, +"20": 1, +"23": 1, +"25": -10, +"28": 1, +"29": 1, +"3": 6, +"30": 1, +"32": 1, +"33": 1, +"34": 1, +"35": 1, +"37": 1, +"38": 1, +"40": 1, +"42": 1, +"43": 1, +"46": 1, +"49": 1, +"5": -11, +"50": 1, +"52": 1, +"54": 1, +"55": 1, +"58": 1, +"6": -2, +"61": 1, +"62": 1, +"66": 1, +"68": 1, +"71": 1, +"72": 1, +"74": 1, +"75": 1, +"76": 1, +"79": 1, +"8": -11, +"82": 1, +"86": 1, +"9": 1, +"91": 1, +"93": 1, +"96": 1, +"97": 1, +"98": 1, +"99": 1 +}, +{ +"100": 1, +"101": 1, +"104": 1, +"109": 1, +"11": -14, +"111": 1, +"13": -2, +"15": 1, +"16": 1, +"18": 1, +"20": 1, +"21": 1, +"23": 1, +"25": -5, +"26": 1, +"27": 1, +"29": 1, +"3": 9, +"32": 1, +"33": 1, +"35": 1, +"37": 1, +"40": 1, +"41": 1, +"46": 1, +"47": 1, +"5": -15, +"51": 1, +"53": 1, +"55": 1, +"56": 1, +"58": 1, +"59": 1, +"6": -3, +"61": 1, +"63": 1, +"67": 1, +"7": 1, +"74": 1, +"75": 1, +"77": 1, +"78": 1, +"8": -8, +"80": 1, +"81": 1, +"83": 1, +"86": 1, +"89": 1, +"94": 1, +"95": 1, +"99": 1 +}, +{ +"104": 1, +"107": 1, +"108": 1, +"11": -11, +"110": 1, +"111": 1, +"13": -8, +"14": 1, +"18": 1, +"19": 1, +"20": 1, +"21": 1, +"22": 1, +"24": 1, +"25": -13, +"26": 1, +"27": 1, +"28": 1, +"3": 12, +"30": 1, +"32": 1, +"34": 1, +"36": 1, +"39": 1, +"41": 1, +"43": 1, +"44": 1, +"46": 1, +"49": 1, +"5": -13, +"52": 1, +"53": 1, +"55": 1, +"56": 1, +"58": 1, +"6": 8, +"60": 1, +"61": 1, +"62": 1, +"64": 1, +"65": 1, +"7": 2, +"70": 1, +"74": 1, +"76": 1, +"78": 1, +"79": 1, +"8": -13, +"81": 1, +"86": 1, +"88": 1, +"9": 1, +"93": 1, +"94": 1, +"95": 1, +"96": 1, +"98": 1, +"99": 1 +} +], +[ +{ +"10": 1, +"100": 1, +"101": 1, +"102": 1, +"104": 1, +"105": 1, +"107": 1, +"108": 1, +"109": 1, +"11": -14, +"111": 1, +"12": 1, +"13": -11, +"14": 1, +"15": 1, +"17": 1, +"18": 1, +"19": 1, +"20": 1, +"21": 1, +"23": 1, +"25": -12, +"26": 1, +"3": 10, +"30": 1, +"31": 1, +"32": 1, +"33": 1, +"36": 1, +"37": 1, +"38": 1, +"39": 1, +"43": 1, +"44": 1, +"45": 1, +"46": 1, +"47": 1, +"49": 1, +"5": -12, +"50": 1, +"52": 1, +"53": 1, +"6": 3, +"64": 1, +"66": 1, +"67": 1, +"69": 1, +"7": 2, +"71": 1, +"72": 1, +"73": 1, +"75": 1, +"78": 1, +"8": -13, +"80": 1, +"81": 1, +"84": 1, +"91": 1, +"97": 1 +}, +{ +"100": 1, +"102": 1, +"105": 1, +"107": 1, +"109": 1, +"11": -13, +"111": 1, +"12": 1, +"15": 1, +"16": 1, +"17": 1, +"18": 1, +"20": 1, +"23": 1, +"24": 1, +"25": -7, +"26": 1, +"27": 1, +"28": 1, +"29": 1, +"3": 1, +"32": 1, +"33": 1, +"36": 1, +"37": 1, +"38": 1, +"43": 1, +"44": 1, +"46": 1, +"48": 1, +"5": -8, +"50": 1, +"51": 1, +"52": 1, +"53": 1, +"58": 1, +"59": 1, +"6": -7, +"61": 1, +"63": 1, +"65": 1, +"66": 1, +"68": 1, +"69": 1, +"7": -2, +"71": 1, +"75": 1, +"76": 1, +"77": 1, +"78": 1, +"8": -9, +"80": 1, +"87": 1, +"88": 1, +"92": 1, +"95": 1, +"97": 1 +}, +{ +"10": 1, +"108": 1, +"109": 1, +"11": -16, +"111": 1, +"13": 1, +"14": 1, +"16": 1, +"19": 1, +"20": 1, +"21": 1, +"23": 1, +"24": 1, +"27": 1, +"28": 1, +"3": 6, +"31": 1, +"33": 1, +"34": 1, +"37": 1, +"40": 1, +"42": 1, +"46": 1, +"5": -12, +"51": 1, +"53": 1, +"57": 1, +"6": -13, +"62": 1, +"67": 1, +"7": -3, +"70": 1, +"71": 1, +"72": 1, +"73": 1, +"74": 1, +"78": 1, +"79": 1, +"8": -6, +"80": 1, +"82": 1, +"83": 1, +"92": 1, +"98": 1 +}, +{ +"10": 1, +"101": 1, +"102": 1, +"106": 1, +"107": 1, +"109": 1, +"11": -14, +"12": 1, +"13": -10, +"18": 1, +"21": 1, +"22": 1, +"23": 1, +"24": 1, +"25": -13, +"27": 1, +"29": 1, +"3": 13, +"33": 1, +"34": 1, +"37": 1, +"41": 1, +"47": 1, +"5": -14, +"50": 1, +"55": 1, +"56": 1, +"58": 1, +"6": 6, +"62": 1, +"66": 1, +"67": 1, +"68": 1, +"7": 1, +"71": 1, +"72": 1, +"73": 1, +"79": 1, +"8": -13, +"81": 1, +"82": 1, +"87": 1, +"89": 1, +"90": 1, +"92": 1, +"94": 1, +"95": 1, +"99": 1 +} +], +[ +{ +"102": 1, +"104": 1, +"107": 1, +"108": 1, +"109": 1, +"11": -15, +"110": 1, +"111": 1, +"12": 1, +"13": -1, +"15": 1, +"16": 1, +"22": 1, +"23": 1, +"25": -4, +"27": 1, +"28": 1, +"29": 1, +"3": 8, +"31": 1, +"34": 1, +"42": 1, +"43": 1, +"46": 1, +"5": -12, +"53": 1, +"56": 1, +"6": -6, +"60": 1, +"62": 1, +"63": 1, +"7": 2, +"72": 1, +"73": 1, +"74": 1, +"77": 1, +"78": 1, +"8": -8, +"80": 1, +"81": 1, +"82": 1, +"83": 1, +"88": 1, +"93": 1, +"94": 1, +"95": 1, +"99": 1 +}, +{ +"10": 1, +"103": 1, +"104": 1, +"105": 1, +"107": 1, +"108": 1, +"11": -14, +"110": 1, +"111": 1, +"13": -13, +"14": 1, +"15": 1, +"16": 1, +"17": 1, +"19": 1, +"20": 1, +"21": 1, +"22": 1, +"24": 1, +"25": -14, +"26": 1, +"27": 1, +"29": 1, +"3": 17, +"30": 1, +"35": 1, +"36": 1, +"38": 1, +"39": 1, +"40": 1, +"41": 1, +"43": 1, +"45": 1, +"46": 1, +"48": 1, +"5": -18, +"51": 1, +"54": 1, +"55": 1, +"56": 1, +"58": 1, +"59": 1, +"6": 11, +"61": 1, +"62": 1, +"63": 1, +"66": 1, +"69": 1, +"7": 1, +"71": 1, +"72": 1, +"73": 1, +"74": 1, +"79": 1, +"8": -20, +"80": 1, +"83": 1, +"87": 1, +"94": 1, +"96": 1, +"97": 1, +"98": 1, +"99": 1 +}, +{ +"10": 1, +"103": 1, +"105": 1, +"106": 1, +"107": 1, +"108": 1, +"109": 1, +"11": -11, +"111": 1, +"13": -15, +"14": 1, +"19": 1, +"21": 1, +"22": 1, +"24": 1, +"25": -19, +"27": 1, +"3": 14, +"30": 1, +"32": 1, +"35": 1, +"40": 1, +"46": 1, +"47": 1, +"48": 1, +"49": 1, +"5": -16, +"52": 1, +"56": 1, +"58": 1, +"59": 1, +"6": 19, +"62": 1, +"65": 1, +"66": 1, +"67": 1, +"7": 4, +"70": 1, +"71": 1, +"72": 1, +"73": 1, +"74": 1, +"75": 1, +"77": 1, +"8": -19, +"81": 1, +"83": 1, +"84": 1, +"85": 1, +"9": 1, +"91": 1, +"93": 1, +"94": 1, +"95": 1, +"96": 1, +"98": 1 +}, +{ +"100": 1, +"101": 1, +"102": 1, +"103": 1, +"104": 1, +"105": 1, +"108": 1, +"11": -12, +"111": 1, +"13": -17, +"20": 1, +"21": 1, +"22": 1, +"25": -19, +"27": 1, +"29": 1, +"3": 16, +"32": 1, +"33": 1, +"36": 1, +"37": 1, +"40": 1, +"45": 1, +"46": 1, +"47": 1, +"48": 1, +"49": 1, +"5": -19, +"50": 1, +"54": 1, +"56": 1, +"57": 1, +"6": 15, +"64": 1, +"65": 1, +"66": 1, +"68": 1, +"7": 5, +"70": 1, +"73": 1, +"74": 1, +"75": 1, +"8": -17, +"81": 1, +"83": 1, +"84": 1, +"85": 1, +"87": 1, +"88": 1, +"89": 1, +"90": 1, +"91": 1, +"93": 1, +"94": 1, +"95": 1, +"96": 1, +"98": 1, +"99": 1 +} +], +[ +{ +"10": 1, +"102": 1, +"104": 1, +"106": 1, +"107": 1, +"108": 1, +"11": -17, +"12": 1, +"13": -14, +"15": 1, +"18": 1, +"19": 1, +"20": 1, +"21": 1, +"23": 1, +"25": -15, +"26": 1, +"27": 1, +"29": 1, +"3": 16, +"31": 1, +"32": 1, +"36": 1, +"37": 1, +"38": 1, +"39": 1, +"41": 1, +"44": 1, +"45": 1, +"46": 1, +"47": 1, +"48": 1, +"49": 1, +"5": -18, +"51": 1, +"52": 1, +"53": 1, +"54": 1, +"55": 1, +"57": 1, +"58": 1, +"6": 10, +"60": 1, +"61": 1, +"63": 1, +"64": 1, +"65": 1, +"7": 1, +"70": 1, +"71": 1, +"72": 1, +"73": 1, +"79": 1, +"8": -18, +"80": 1, +"81": 1, +"85": 1, +"86": 1, +"88": 1, +"90": 1, +"92": 1, +"93": 1, +"94": 1, +"97": 1, +"98": 1 +}, +{ +"100": 1, +"101": 1, +"102": 1, +"104": 1, +"105": 1, +"107": 1, +"11": -20, +"110": 1, +"111": 1, +"13": -2, +"16": 1, +"22": 1, +"25": -8, +"26": 1, +"27": 1, +"28": 1, +"29": 1, +"3": 8, +"30": 1, +"31": 1, +"32": 1, +"33": 1, +"37": 1, +"38": 1, +"40": 1, +"42": 1, +"43": 1, +"46": 1, +"48": 1, +"49": 1, +"5": -18, +"50": 1, +"51": 1, +"52": 1, +"53": 1, +"54": 1, +"55": 1, +"56": 1, +"57": 1, +"58": 1, +"6": -9, +"61": 1, +"62": 1, +"63": 1, +"67": 1, +"69": 1, +"70": 1, +"71": 1, +"72": 1, +"73": 1, +"74": 1, +"75": 1, +"77": 1, +"78": 1, +"8": -9, +"80": 1, +"82": 1, +"87": 1, +"90": 1, +"93": 1, +"97": 1, +"98": 1 +}, +{ +"10": 1, +"100": 1, +"102": 1, +"103": 1, +"105": 1, +"106": 1, +"107": 1, +"109": 1, +"11": -11, +"111": 1, +"12": 1, +"13": -16, +"18": 1, +"19": 1, +"20": 1, +"25": -17, +"26": 1, +"3": 16, +"30": 1, +"34": 1, +"35": 1, +"36": 1, +"37": 1, +"40": 1, +"41": 1, +"42": 1, +"45": 1, +"46": 1, +"47": 1, +"48": 1, +"5": -14, +"50": 1, +"59": 1, +"6": 14, +"62": 1, +"65": 1, +"68": 1, +"7": 2, +"70": 1, +"72": 1, +"75": 1, +"77": 1, +"79": 1, +"8": -17, +"82": 1, +"83": 1, +"87": 1, +"9": 1, +"90": 1, +"91": 1, +"92": 1, +"94": 1, +"96": 1, +"97": 1, +"99": 1 +}, +{ +"105": 1, +"11": -4, +"12": 1, +"13": -7, +"15": 1, +"18": 1, +"20": 1, +"21": 1, +"25": -9, +"27": 1, +"29": 1, +"3": 6, +"30": 1, +"31": 1, +"32": 1, +"33": 1, +"34": 1, +"35": 1, +"36": 1, +"43": 1, +"46": 1, +"47": 1, +"5": -10, +"54": 1, +"56": 1, +"58": 1, +"59": 1, +"6": 5, +"60": 1, +"63": 1, +"65": 1, +"67": 1, +"69": 1, +"70": 1, +"74": 1, +"8": -9, +"80": 1, +"83": 1, +"88": 1, +"94": 1, +"96": 1 +} +], +[ +{ +"10": 1, +"100": 1, +"102": 1, +"103": 1, +"104": 1, +"105": 1, +"107": 1, +"11": -17, +"12": 1, +"13": -9, +"14": 1, +"18": 1, +"20": 1, +"21": 1, +"23": 1, +"24": 1, +"25": -12, +"27": 1, +"3": 15, +"31": 1, +"32": 1, +"39": 1, +"40": 1, +"41": 1, +"46": 1, +"48": 1, +"5": -19, +"51": 1, +"53": 1, +"57": 1, +"58": 1, +"59": 1, +"6": 7, +"60": 1, +"61": 1, +"62": 1, +"63": 1, +"64": 1, +"66": 1, +"68": 1, +"70": 1, +"71": 1, +"73": 1, +"77": 1, +"8": -16, +"81": 1, +"82": 1, +"87": 1, +"89": 1, +"9": 1, +"90": 1, +"91": 1, +"93": 1, +"94": 1, +"99": 1 +}, +{ +"102": 1, +"106": 1, +"107": 1, +"108": 1, +"109": 1, +"11": -13, +"110": 1, +"111": 1, +"13": -6, +"15": 1, +"16": 1, +"19": 1, +"20": 1, +"21": 1, +"22": 1, +"25": -6, +"28": 1, +"3": 11, +"38": 1, +"40": 1, +"42": 1, +"47": 1, +"5": -14, +"51": 1, +"54": 1, +"57": 1, +"59": 1, +"6": 2, +"60": 1, +"61": 1, +"62": 1, +"63": 1, +"64": 1, +"66": 1, +"67": 1, +"70": 1, +"72": 1, +"74": 1, +"8": -14, +"81": 1, +"82": 1, +"84": 1, +"88": 1, +"89": 1, +"93": 1, +"94": 1, +"98": 1, +"99": 1 +}, +{ +"10": 1, +"100": 1, +"101": 1, +"103": 1, +"104": 1, +"106": 1, +"107": 1, +"108": 1, +"11": -23, +"110": 1, +"12": 1, +"13": -13, +"14": 1, +"16": 1, +"17": 1, +"20": 1, +"23": 1, +"24": 1, +"25": -15, +"26": 1, +"27": 1, +"29": 1, +"3": 17, +"30": 1, +"32": 1, +"33": 1, +"35": 1, +"37": 1, +"41": 1, +"42": 1, +"43": 1, +"44": 1, +"45": 1, +"48": 1, +"49": 1, +"5": -20, +"51": 1, +"52": 1, +"53": 1, +"55": 1, +"56": 1, +"59": 1, +"6": 10, +"62": 1, +"64": 1, +"66": 1, +"7": 9, +"70": 1, +"74": 1, +"75": 1, +"76": 1, +"77": 1, +"78": 1, +"79": 1, +"8": -18, +"81": 1, +"83": 1, +"85": 1, +"90": 1, +"91": 1, +"93": 1, +"94": 1, +"95": 1, +"97": 1 +}, +{ +"10": 1, +"100": 1, +"101": 1, +"103": 1, +"104": 1, +"106": 1, +"108": 1, +"11": -12, +"111": 1, +"12": 1, +"13": -12, +"14": 1, +"19": 1, +"21": 1, +"22": 1, +"23": 1, +"25": -16, +"26": 1, +"28": 1, +"3": 10, +"31": 1, +"36": 1, +"40": 1, +"45": 1, +"46": 1, +"48": 1, +"5": -15, +"50": 1, +"52": 1, +"59": 1, +"6": 10, +"60": 1, +"61": 1, +"62": 1, +"66": 1, +"68": 1, +"7": 2, +"70": 1, +"72": 1, +"73": 1, +"74": 1, +"75": 1, +"78": 1, +"79": 1, +"8": -14, +"80": 1, +"81": 1, +"84": 1, +"85": 1, +"86": 1, +"87": 1, +"88": 1, +"89": 1, +"90": 1, +"91": 1, +"92": 1, +"93": 1, +"95": 1 +} +], +[ +{ +"100": 1, +"101": 1, +"103": 1, +"104": 1, +"105": 1, +"107": 1, +"108": 1, +"109": 1, +"11": -11, +"111": 1, +"13": -15, +"19": 1, +"20": 1, +"22": 1, +"24": 1, +"25": -16, +"3": 13, +"30": 1, +"31": 1, +"35": 1, +"38": 1, +"39": 1, +"42": 1, +"46": 1, +"47": 1, +"49": 1, +"5": -15, +"50": 1, +"52": 1, +"53": 1, +"58": 1, +"59": 1, +"6": 18, +"62": 1, +"64": 1, +"66": 1, +"68": 1, +"7": 8, +"75": 1, +"76": 1, +"78": 1, +"8": -15, +"83": 1, +"85": 1, +"86": 1, +"90": 1, +"95": 1, +"97": 1, +"99": 1 +}, +{ +"100": 1, +"101": 1, +"102": 1, +"104": 1, +"105": 1, +"106": 1, +"11": -17, +"110": 1, +"13": -10, +"15": 1, +"16": 1, +"17": 1, +"18": 1, +"20": 1, +"22": 1, +"25": -15, +"28": 1, +"29": 1, +"3": 15, +"31": 1, +"34": 1, +"36": 1, +"39": 1, +"41": 1, +"42": 1, +"43": 1, +"44": 1, +"45": 1, +"48": 1, +"49": 1, +"5": -20, +"52": 1, +"54": 1, +"55": 1, +"57": 1, +"58": 1, +"6": 4, +"60": 1, +"61": 1, +"65": 1, +"66": 1, +"67": 1, +"68": 1, +"7": 6, +"70": 1, +"71": 1, +"73": 1, +"76": 1, +"78": 1, +"79": 1, +"8": -14, +"80": 1, +"81": 1, +"82": 1, +"85": 1, +"86": 1, +"88": 1, +"89": 1, +"90": 1, +"91": 1, +"93": 1, +"95": 1, +"96": 1, +"97": 1, +"98": 1, +"99": 1 +}, +{ +"10": 1, +"100": 1, +"101": 1, +"103": 1, +"104": 1, +"105": 1, +"106": 1, +"107": 1, +"108": 1, +"11": -22, +"110": 1, +"111": 1, +"12": 1, +"13": -9, +"14": 1, +"21": 1, +"23": 1, +"24": 1, +"25": -13, +"26": 1, +"27": 1, +"28": 1, +"3": 17, +"31": 1, +"33": 1, +"34": 1, +"36": 1, +"38": 1, +"39": 1, +"41": 1, +"42": 1, +"44": 1, +"45": 1, +"46": 1, +"5": -22, +"50": 1, +"52": 1, +"53": 1, +"54": 1, +"55": 1, +"57": 1, +"58": 1, +"6": 3, +"61": 1, +"62": 1, +"63": 1, +"67": 1, +"68": 1, +"7": 4, +"71": 1, +"73": 1, +"77": 1, +"78": 1, +"8": -13, +"80": 1, +"85": 1, +"86": 1, +"88": 1, +"89": 1, +"9": 1, +"90": 1, +"91": 1, +"93": 1, +"94": 1, +"95": 1, +"97": 1, +"99": 1 +}, +{ +"10": 1, +"101": 1, +"102": 1, +"104": 1, +"105": 1, +"106": 1, +"107": 1, +"108": 1, +"109": 1, +"11": -17, +"110": 1, +"111": 1, +"13": -1, +"15": 1, +"16": 1, +"18": 1, +"19": 1, +"21": 1, +"23": 1, +"25": -8, +"27": 1, +"28": 1, +"29": 1, +"3": 4, +"32": 1, +"33": 1, +"38": 1, +"39": 1, +"42": 1, +"43": 1, +"44": 1, +"46": 1, +"48": 1, +"5": -10, +"50": 1, +"51": 1, +"52": 1, +"53": 1, +"57": 1, +"59": 1, +"6": -5, +"60": 1, +"62": 1, +"65": 1, +"69": 1, +"7": 2, +"71": 1, +"75": 1, +"76": 1, +"8": -9, +"82": 1, +"87": 1, +"88": 1, +"90": 1, +"92": 1, +"93": 1, +"96": 1, +"97": 1, +"99": 1 +} +], +[ +{ +"103": 1, +"105": 1, +"106": 1, +"109": 1, +"11": -16, +"110": 1, +"111": 1, +"12": 1, +"13": -3, +"14": 1, +"16": 1, +"17": 1, +"18": 1, +"19": 1, +"20": 1, +"21": 1, +"23": 1, +"25": -9, +"28": 1, +"3": 4, +"30": 1, +"31": 1, +"34": 1, +"35": 1, +"36": 1, +"37": 1, +"39": 1, +"44": 1, +"48": 1, +"49": 1, +"5": -13, +"50": 1, +"51": 1, +"53": 1, +"56": 1, +"58": 1, +"6": -3, +"60": 1, +"61": 1, +"64": 1, +"65": 1, +"66": 1, +"68": 1, +"69": 1, +"7": -2, +"70": 1, +"71": 1, +"72": 1, +"75": 1, +"76": 1, +"77": 1, +"79": 1, +"8": -16, +"80": 1, +"81": 1, +"82": 1, +"83": 1, +"84": 1, +"87": 1, +"90": 1, +"92": 1, +"93": 1, +"94": 1, +"95": 1, +"96": 1, +"97": 1, +"99": 1 +}, +{ +"102": 1, +"105": 1, +"106": 1, +"107": 1, +"11": -7, +"13": -12, +"17": 1, +"18": 1, +"20": 1, +"21": 1, +"24": 1, +"25": -20, +"26": 1, +"28": 1, +"29": 1, +"3": 7, +"30": 1, +"32": 1, +"34": 1, +"36": 1, +"38": 1, +"40": 1, +"44": 1, +"47": 1, +"48": 1, +"49": 1, +"5": -13, +"52": 1, +"53": 1, +"59": 1, +"6": 15, +"60": 1, +"64": 1, +"65": 1, +"66": 1, +"7": 4, +"70": 1, +"71": 1, +"72": 1, +"73": 1, +"74": 1, +"75": 1, +"77": 1, +"78": 1, +"79": 1, +"8": -12, +"81": 1, +"82": 1, +"83": 1, +"85": 1, +"87": 1, +"88": 1, +"89": 1, +"91": 1, +"92": 1, +"93": 1, +"96": 1, +"98": 1, +"99": 1 +}, +{ +"104": 1, +"105": 1, +"106": 1, +"107": 1, +"109": 1, +"11": -15, +"13": 3, +"17": 1, +"20": 1, +"21": 1, +"22": 1, +"23": 1, +"24": 1, +"25": -10, +"26": 1, +"27": 1, +"3": 3, +"30": 1, +"31": 1, +"32": 1, +"33": 1, +"34": 1, +"37": 1, +"39": 1, +"40": 1, +"43": 1, +"44": 1, +"45": 1, +"46": 1, +"47": 1, +"48": 1, +"49": 1, +"5": -13, +"50": 1, +"51": 1, +"52": 1, +"58": 1, +"59": 1, +"6": -4, +"60": 1, +"66": 1, +"69": 1, +"72": 1, +"74": 1, +"76": 1, +"77": 1, +"78": 1, +"8": -10, +"80": 1, +"82": 1, +"85": 1, +"86": 1, +"88": 1, +"89": 1, +"9": 1, +"90": 1, +"93": 1, +"95": 1, +"97": 1, +"98": 1 +}, +{ +"104": 1, +"106": 1, +"109": 1, +"11": -13, +"111": 1, +"13": -20, +"15": 1, +"21": 1, +"22": 1, +"24": 1, +"25": -17, +"3": 21, +"33": 1, +"34": 1, +"35": 1, +"36": 1, +"37": 1, +"38": 1, +"39": 1, +"40": 1, +"41": 1, +"42": 1, +"43": 1, +"44": 1, +"45": 1, +"48": 1, +"5": -20, +"51": 1, +"52": 1, +"54": 1, +"56": 1, +"58": 1, +"6": 19, +"60": 1, +"64": 1, +"68": 1, +"7": 8, +"70": 1, +"71": 1, +"73": 1, +"76": 1, +"77": 1, +"78": 1, +"79": 1, +"8": -16, +"9": 1, +"90": 1, +"94": 1, +"96": 1, +"97": 1, +"98": 1, +"99": 1 +} +], +[ +{ +"102": 1, +"105": 1, +"106": 1, +"107": 1, +"108": 1, +"11": -14, +"110": 1, +"12": 1, +"13": -8, +"14": 1, +"16": 1, +"17": 1, +"18": 1, +"19": 1, +"20": 1, +"25": -8, +"28": 1, +"29": 1, +"3": 13, +"36": 1, +"41": 1, +"42": 1, +"45": 1, +"46": 1, +"47": 1, +"49": 1, +"5": -14, +"51": 1, +"53": 1, +"54": 1, +"55": 1, +"57": 1, +"58": 1, +"6": 2, +"60": 1, +"61": 1, +"62": 1, +"63": 1, +"65": 1, +"68": 1, +"70": 1, +"73": 1, +"76": 1, +"77": 1, +"78": 1, +"8": -14, +"81": 1, +"83": 1, +"86": 1, +"87": 1, +"9": 1, +"92": 1, +"93": 1, +"96": 1 +}, +{ +"10": 1, +"103": 1, +"106": 1, +"107": 1, +"108": 1, +"109": 1, +"11": -18, +"110": 1, +"13": 2, +"14": 1, +"15": 1, +"17": 1, +"19": 1, +"21": 1, +"23": 1, +"25": -5, +"26": 1, +"27": 1, +"28": 1, +"29": 1, +"3": 4, +"33": 1, +"35": 1, +"37": 1, +"38": 1, +"40": 1, +"44": 1, +"45": 1, +"47": 1, +"49": 1, +"5": -14, +"51": 1, +"52": 1, +"55": 1, +"57": 1, +"6": -11, +"61": 1, +"64": 1, +"65": 1, +"67": 1, +"68": 1, +"69": 1, +"7": -3, +"71": 1, +"72": 1, +"74": 1, +"75": 1, +"78": 1, +"8": -10, +"80": 1, +"82": 1, +"84": 1, +"87": 1, +"89": 1, +"90": 1, +"92": 1, +"94": 1, +"95": 1, +"98": 1, +"99": 1 +}, +{ +"100": 1, +"104": 1, +"105": 1, +"109": 1, +"11": -15, +"111": 1, +"13": -8, +"15": 1, +"16": 1, +"18": 1, +"19": 1, +"20": 1, +"23": 1, +"25": -15, +"26": 1, +"28": 1, +"29": 1, +"3": 8, +"31": 1, +"32": 1, +"33": 1, +"36": 1, +"38": 1, +"44": 1, +"45": 1, +"46": 1, +"48": 1, +"5": -12, +"50": 1, +"52": 1, +"54": 1, +"56": 1, +"57": 1, +"58": 1, +"6": 3, +"61": 1, +"62": 1, +"63": 1, +"65": 1, +"66": 1, +"68": 1, +"69": 1, +"7": 2, +"71": 1, +"72": 1, +"75": 1, +"76": 1, +"77": 1, +"78": 1, +"79": 1, +"8": -12, +"80": 1, +"81": 1, +"83": 1, +"87": 1, +"88": 1, +"89": 1, +"91": 1, +"92": 1, +"93": 1, +"95": 1, +"96": 1, +"97": 1, +"99": 1 +}, +{ +"100": 1, +"102": 1, +"106": 1, +"107": 1, +"108": 1, +"109": 1, +"11": -22, +"110": 1, +"111": 1, +"12": 1, +"13": -8, +"16": 1, +"19": 1, +"21": 1, +"24": 1, +"25": -14, +"26": 1, +"27": 1, +"28": 1, +"29": 1, +"3": 12, +"30": 1, +"31": 1, +"32": 1, +"34": 1, +"37": 1, +"39": 1, +"40": 1, +"42": 1, +"49": 1, +"5": -21, +"52": 1, +"55": 1, +"56": 1, +"57": 1, +"58": 1, +"59": 1, +"6": 8, +"61": 1, +"62": 1, +"64": 1, +"65": 1, +"69": 1, +"7": 5, +"70": 1, +"72": 1, +"73": 1, +"75": 1, +"76": 1, +"77": 1, +"78": 1, +"8": -18, +"81": 1, +"82": 1, +"84": 1, +"85": 1, +"86": 1, +"87": 1, +"89": 1, +"9": 1, +"90": 1, +"94": 1, +"95": 1, +"99": 1 +} +], +[ +{ +"10": 1, +"101": 1, +"102": 1, +"104": 1, +"105": 1, +"106": 1, +"107": 1, +"11": -12, +"110": 1, +"12": 1, +"13": -22, +"14": 1, +"16": 1, +"18": 1, +"21": 1, +"22": 1, +"24": 1, +"25": -21, +"28": 1, +"29": 1, +"3": 19, +"30": 1, +"32": 1, +"33": 1, +"34": 1, +"35": 1, +"38": 1, +"40": 1, +"43": 1, +"44": 1, +"46": 1, +"47": 1, +"49": 1, +"5": -17, +"52": 1, +"53": 1, +"56": 1, +"57": 1, +"59": 1, +"6": 22, +"60": 1, +"62": 1, +"63": 1, +"64": 1, +"67": 1, +"7": 9, +"70": 1, +"74": 1, +"76": 1, +"77": 1, +"78": 1, +"79": 1, +"8": -17, +"80": 1, +"83": 1, +"84": 1, +"93": 1, +"94": 1, +"95": 1, +"96": 1, +"97": 1 +}, +{ +"10": 1, +"100": 1, +"103": 1, +"104": 1, +"108": 1, +"11": -16, +"13": -7, +"14": 1, +"15": 1, +"19": 1, +"20": 1, +"21": 1, +"23": 1, +"25": -10, +"27": 1, +"28": 1, +"29": 1, +"3": 7, +"30": 1, +"35": 1, +"38": 1, +"40": 1, +"43": 1, +"46": 1, +"47": 1, +"48": 1, +"5": -18, +"51": 1, +"52": 1, +"53": 1, +"54": 1, +"55": 1, +"56": 1, +"57": 1, +"58": 1, +"59": 1, +"6": 4, +"60": 1, +"62": 1, +"63": 1, +"66": 1, +"68": 1, +"69": 1, +"7": 1, +"70": 1, +"72": 1, +"75": 1, +"77": 1, +"78": 1, +"8": -14, +"80": 1, +"83": 1, +"84": 1, +"85": 1, +"86": 1, +"88": 1, +"89": 1, +"91": 1, +"92": 1, +"94": 1, +"95": 1, +"96": 1 +}, +{ +"10": 1, +"102": 1, +"103": 1, +"105": 1, +"106": 1, +"109": 1, +"11": -13, +"110": 1, +"12": 1, +"13": -14, +"14": 1, +"15": 1, +"16": 1, +"17": 1, +"18": 1, +"22": 1, +"23": 1, +"24": 1, +"25": -19, +"28": 1, +"3": 15, +"30": 1, +"31": 1, +"32": 1, +"33": 1, +"34": 1, +"36": 1, +"40": 1, +"45": 1, +"46": 1, +"47": 1, +"5": -15, +"51": 1, +"52": 1, +"53": 1, +"57": 1, +"58": 1, +"6": 9, +"60": 1, +"61": 1, +"63": 1, +"66": 1, +"67": 1, +"69": 1, +"7": 2, +"70": 1, +"71": 1, +"72": 1, +"73": 1, +"74": 1, +"76": 1, +"79": 1, +"8": -12, +"81": 1, +"83": 1, +"85": 1, +"88": 1, +"9": 1, +"91": 1, +"93": 1, +"94": 1, +"95": 1, +"96": 1, +"98": 1, +"99": 1 +}, +{ +"101": 1, +"102": 1, +"104": 1, +"105": 1, +"107": 1, +"11": -10, +"110": 1, +"13": -8, +"14": 1, +"18": 1, +"19": 1, +"20": 1, +"23": 1, +"24": 1, +"25": -17, +"26": 1, +"27": 1, +"28": 1, +"29": 1, +"3": 6, +"30": 1, +"32": 1, +"34": 1, +"36": 1, +"37": 1, +"38": 1, +"40": 1, +"43": 1, +"45": 1, +"47": 1, +"5": -10, +"54": 1, +"56": 1, +"58": 1, +"6": 8, +"60": 1, +"61": 1, +"62": 1, +"65": 1, +"66": 1, +"68": 1, +"69": 1, +"7": -1, +"70": 1, +"72": 1, +"79": 1, +"8": -14, +"81": 1, +"82": 1, +"83": 1, +"84": 1, +"85": 1, +"86": 1, +"87": 1, +"88": 1, +"89": 1, +"9": 1, +"90": 1, +"92": 1, +"93": 1, +"98": 1, +"99": 1 +} +], +[ +{ +"102": 1, +"104": 1, +"106": 1, +"109": 1, +"11": -18, +"12": 1, +"14": 1, +"15": 1, +"19": 1, +"20": 1, +"21": 1, +"25": -3, +"27": 1, +"28": 1, +"29": 1, +"3": 1, +"32": 1, +"36": 1, +"39": 1, +"40": 1, +"42": 1, +"44": 1, +"49": 1, +"5": -13, +"50": 1, +"51": 1, +"52": 1, +"53": 1, +"54": 1, +"55": 1, +"58": 1, +"6": -8, +"60": 1, +"65": 1, +"66": 1, +"69": 1, +"7": 1, +"70": 1, +"72": 1, +"74": 1, +"75": 1, +"76": 1, +"8": -9, +"83": 1, +"85": 1, +"88": 1, +"9": 1, +"90": 1, +"92": 1, +"93": 1, +"94": 1, +"96": 1 +}, +{ +"100": 1, +"101": 1, +"103": 1, +"105": 1, +"106": 1, +"107": 1, +"11": -12, +"110": 1, +"111": 1, +"13": -9, +"14": 1, +"18": 1, +"19": 1, +"22": 1, +"23": 1, +"24": 1, +"25": -13, +"26": 1, +"28": 1, +"3": 8, +"32": 1, +"34": 1, +"36": 1, +"37": 1, +"38": 1, +"43": 1, +"44": 1, +"46": 1, +"48": 1, +"49": 1, +"5": -14, +"52": 1, +"53": 1, +"6": 5, +"60": 1, +"64": 1, +"66": 1, +"68": 1, +"69": 1, +"7": 2, +"70": 1, +"71": 1, +"73": 1, +"78": 1, +"8": -10, +"80": 1, +"81": 1, +"82": 1, +"83": 1, +"85": 1, +"86": 1, +"87": 1, +"88": 1, +"89": 1, +"9": 1, +"92": 1, +"94": 1, +"97": 1, +"99": 1 +}, +{ +"101": 1, +"102": 1, +"104": 1, +"107": 1, +"109": 1, +"11": -18, +"12": 1, +"13": -8, +"14": 1, +"15": 1, +"16": 1, +"22": 1, +"24": 1, +"25": -14, +"26": 1, +"28": 1, +"29": 1, +"3": 10, +"30": 1, +"31": 1, +"32": 1, +"33": 1, +"34": 1, +"35": 1, +"37": 1, +"39": 1, +"41": 1, +"42": 1, +"43": 1, +"44": 1, +"46": 1, +"49": 1, +"5": -15, +"52": 1, +"54": 1, +"56": 1, +"60": 1, +"62": 1, +"66": 1, +"67": 1, +"68": 1, +"69": 1, +"7": 6, +"73": 1, +"74": 1, +"75": 1, +"76": 1, +"77": 1, +"79": 1, +"8": -9, +"82": 1, +"84": 1, +"85": 1, +"86": 1, +"87": 1, +"9": 1, +"92": 1, +"93": 1, +"94": 1, +"95": 1, +"96": 1, +"97": 1, +"98": 1, +"99": 1 +}, +{ +"100": 1, +"102": 1, +"108": 1, +"109": 1, +"11": -19, +"111": 1, +"12": 1, +"13": -5, +"14": 1, +"15": 1, +"18": 1, +"19": 1, +"24": 1, +"25": -12, +"27": 1, +"28": 1, +"3": 6, +"30": 1, +"31": 1, +"32": 1, +"33": 1, +"34": 1, +"36": 1, +"37": 1, +"38": 1, +"39": 1, +"40": 1, +"41": 1, +"43": 1, +"47": 1, +"48": 1, +"5": -16, +"50": 1, +"53": 1, +"55": 1, +"56": 1, +"57": 1, +"58": 1, +"59": 1, +"62": 1, +"64": 1, +"65": 1, +"66": 1, +"69": 1, +"7": -1, +"74": 1, +"75": 1, +"76": 1, +"77": 1, +"78": 1, +"8": -14, +"80": 1, +"81": 1, +"82": 1, +"86": 1, +"87": 1, +"88": 1, +"89": 1, +"9": 1, +"90": 1, +"91": 1, +"92": 1, +"97": 1, +"98": 1 +} +], +[ +{ +"10": 1, +"100": 1, +"101": 1, +"103": 1, +"105": 1, +"106": 1, +"107": 1, +"109": 1, +"11": -15, +"12": 1, +"13": -9, +"14": 1, +"23": 1, +"25": -13, +"27": 1, +"28": 1, +"3": 9, +"32": 1, +"33": 1, +"38": 1, +"41": 1, +"42": 1, +"43": 1, +"47": 1, +"48": 1, +"5": -15, +"50": 1, +"52": 1, +"55": 1, +"58": 1, +"6": 4, +"61": 1, +"63": 1, +"64": 1, +"66": 1, +"67": 1, +"68": 1, +"7": 4, +"70": 1, +"74": 1, +"75": 1, +"77": 1, +"8": -12, +"80": 1, +"82": 1, +"84": 1, +"85": 1, +"88": 1, +"89": 1, +"9": 1, +"90": 1, +"91": 1, +"93": 1, +"96": 1, +"97": 1, +"99": 1 +}, +{ +"10": 1, +"100": 1, +"101": 1, +"105": 1, +"11": -20, +"12": 1, +"13": -21, +"15": 1, +"20": 1, +"22": 1, +"24": 1, +"25": -15, +"26": 1, +"28": 1, +"3": 21, +"32": 1, +"34": 1, +"37": 1, +"38": 1, +"39": 1, +"41": 1, +"42": 1, +"44": 1, +"48": 1, +"49": 1, +"5": -24, +"50": 1, +"51": 1, +"52": 1, +"53": 1, +"54": 1, +"55": 1, +"56": 1, +"57": 1, +"58": 1, +"6": 14, +"61": 1, +"62": 1, +"63": 1, +"64": 1, +"68": 1, +"7": 5, +"70": 1, +"71": 1, +"74": 1, +"78": 1, +"79": 1, +"8": -15, +"86": 1, +"87": 1, +"89": 1, +"9": 1, +"90": 1, +"92": 1, +"94": 1, +"97": 1, +"98": 1 +}, +{ +"100": 1, +"101": 1, +"102": 1, +"104": 1, +"106": 1, +"108": 1, +"109": 1, +"11": -17, +"110": 1, +"111": 1, +"12": 1, +"13": -1, +"18": 1, +"19": 1, +"20": 1, +"21": 1, +"22": 1, +"25": -8, +"26": 1, +"27": 1, +"29": 1, +"3": 7, +"30": 1, +"32": 1, +"34": 1, +"37": 1, +"38": 1, +"39": 1, +"40": 1, +"41": 1, +"43": 1, +"47": 1, +"5": -15, +"50": 1, +"51": 1, +"54": 1, +"58": 1, +"6": -2, +"60": 1, +"62": 1, +"65": 1, +"66": 1, +"70": 1, +"72": 1, +"74": 1, +"76": 1, +"8": -15, +"80": 1, +"83": 1, +"84": 1, +"85": 1, +"86": 1, +"89": 1, +"9": 1, +"97": 1, +"98": 1 +}, +{ +"10": 1, +"102": 1, +"103": 1, +"106": 1, +"107": 1, +"11": -13, +"110": 1, +"111": 1, +"13": -3, +"14": 1, +"19": 1, +"20": 1, +"22": 1, +"23": 1, +"25": -7, +"28": 1, +"29": 1, +"3": 5, +"32": 1, +"34": 1, +"37": 1, +"38": 1, +"40": 1, +"43": 1, +"44": 1, +"46": 1, +"47": 1, +"48": 1, +"49": 1, +"5": -12, +"50": 1, +"56": 1, +"57": 1, +"59": 1, +"6": -3, +"62": 1, +"67": 1, +"68": 1, +"7": -3, +"73": 1, +"78": 1, +"8": -10, +"80": 1, +"81": 1, +"82": 1, +"83": 1, +"84": 1, +"85": 1, +"87": 1, +"88": 1, +"90": 1, +"91": 1, +"94": 1, +"95": 1, +"96": 1 +} +], +[ +{ +"102": 1, +"104": 1, +"105": 1, +"106": 1, +"11": -13, +"12": 1, +"13": -8, +"22": 1, +"23": 1, +"24": 1, +"25": -12, +"28": 1, +"29": 1, +"3": 9, +"34": 1, +"36": 1, +"37": 1, +"38": 1, +"39": 1, +"40": 1, +"44": 1, +"45": 1, +"46": 1, +"5": -11, +"50": 1, +"51": 1, +"55": 1, +"56": 1, +"57": 1, +"6": 5, +"61": 1, +"64": 1, +"7": 4, +"70": 1, +"73": 1, +"75": 1, +"77": 1, +"8": -9, +"80": 1, +"82": 1, +"85": 1, +"88": 1, +"89": 1, +"92": 1, +"93": 1, +"97": 1, +"98": 1 +}, +{ +"10": 1, +"100": 1, +"106": 1, +"108": 1, +"109": 1, +"11": -21, +"110": 1, +"13": 1, +"14": 1, +"16": 1, +"17": 1, +"19": 1, +"20": 1, +"21": 1, +"22": 1, +"25": -6, +"26": 1, +"27": 1, +"28": 1, +"3": 5, +"31": 1, +"33": 1, +"34": 1, +"35": 1, +"39": 1, +"40": 1, +"5": -18, +"50": 1, +"55": 1, +"56": 1, +"58": 1, +"6": -4, +"61": 1, +"62": 1, +"64": 1, +"65": 1, +"66": 1, +"68": 1, +"7": 1, +"70": 1, +"72": 1, +"74": 1, +"75": 1, +"76": 1, +"78": 1, +"8": -14, +"80": 1, +"82": 1, +"83": 1, +"85": 1, +"86": 1, +"87": 1, +"89": 1, +"95": 1, +"98": 1 +}, +{ +"10": 1, +"100": 1, +"102": 1, +"104": 1, +"105": 1, +"11": -13, +"12": 1, +"13": -15, +"15": 1, +"17": 1, +"19": 1, +"20": 1, +"21": 1, +"22": 1, +"25": -17, +"26": 1, +"27": 1, +"28": 1, +"3": 13, +"30": 1, +"32": 1, +"34": 1, +"35": 1, +"36": 1, +"38": 1, +"39": 1, +"41": 1, +"42": 1, +"46": 1, +"47": 1, +"49": 1, +"5": -17, +"50": 1, +"51": 1, +"53": 1, +"54": 1, +"56": 1, +"58": 1, +"59": 1, +"6": 12, +"66": 1, +"68": 1, +"69": 1, +"7": 6, +"71": 1, +"73": 1, +"74": 1, +"75": 1, +"76": 1, +"77": 1, +"78": 1, +"8": -13, +"84": 1, +"9": 1, +"90": 1, +"92": 1, +"93": 1, +"94": 1, +"96": 1, +"97": 1, +"99": 1 +}, +{ +"10": 1, +"100": 1, +"104": 1, +"107": 1, +"108": 1, +"11": -18, +"110": 1, +"111": 1, +"14": 1, +"15": 1, +"20": 1, +"21": 1, +"22": 1, +"25": -1, +"3": 9, +"31": 1, +"34": 1, +"38": 1, +"39": 1, +"40": 1, +"42": 1, +"43": 1, +"46": 1, +"48": 1, +"49": 1, +"5": -20, +"51": 1, +"52": 1, +"55": 1, +"6": -10, +"60": 1, +"61": 1, +"62": 1, +"66": 1, +"67": 1, +"68": 1, +"7": -3, +"70": 1, +"71": 1, +"76": 1, +"77": 1, +"78": 1, +"8": -7, +"80": 1, +"85": 1, +"86": 1, +"88": 1, +"89": 1, +"98": 1, +"99": 1 +} +], +[ +{ +"10": 1, +"100": 1, +"103": 1, +"104": 1, +"105": 1, +"106": 1, +"11": -18, +"111": 1, +"12": 1, +"13": -10, +"14": 1, +"15": 1, +"16": 1, +"22": 1, +"24": 1, +"25": -12, +"26": 1, +"28": 1, +"29": 1, +"3": 10, +"31": 1, +"32": 1, +"33": 1, +"38": 1, +"39": 1, +"41": 1, +"42": 1, +"43": 1, +"44": 1, +"49": 1, +"5": -17, +"50": 1, +"52": 1, +"6": 5, +"60": 1, +"61": 1, +"62": 1, +"65": 1, +"66": 1, +"67": 1, +"68": 1, +"69": 1, +"7": 6, +"72": 1, +"73": 1, +"74": 1, +"8": -11, +"80": 1, +"81": 1, +"82": 1, +"83": 1, +"85": 1, +"86": 1, +"87": 1, +"89": 1, +"9": 1, +"91": 1, +"92": 1, +"94": 1, +"96": 1, +"99": 1 +}, +{ +"10": 1, +"101": 1, +"103": 1, +"104": 1, +"108": 1, +"11": -13, +"110": 1, +"111": 1, +"13": -3, +"16": 1, +"18": 1, +"21": 1, +"23": 1, +"25": -9, +"29": 1, +"3": 8, +"30": 1, +"32": 1, +"33": 1, +"34": 1, +"35": 1, +"37": 1, +"40": 1, +"41": 1, +"43": 1, +"44": 1, +"47": 1, +"48": 1, +"49": 1, +"5": -15, +"50": 1, +"51": 1, +"52": 1, +"53": 1, +"55": 1, +"57": 1, +"58": 1, +"60": 1, +"64": 1, +"66": 1, +"67": 1, +"69": 1, +"7": -1, +"71": 1, +"74": 1, +"77": 1, +"8": -9, +"81": 1, +"83": 1, +"86": 1, +"87": 1, +"88": 1, +"9": 1, +"92": 1, +"93": 1, +"97": 1, +"98": 1 +}, +{ +"100": 1, +"101": 1, +"102": 1, +"104": 1, +"107": 1, +"108": 1, +"11": -13, +"111": 1, +"13": -10, +"14": 1, +"16": 1, +"20": 1, +"21": 1, +"22": 1, +"24": 1, +"25": -10, +"28": 1, +"3": 13, +"34": 1, +"36": 1, +"37": 1, +"39": 1, +"42": 1, +"43": 1, +"45": 1, +"48": 1, +"49": 1, +"5": -15, +"50": 1, +"51": 1, +"54": 1, +"57": 1, +"58": 1, +"6": 5, +"60": 1, +"66": 1, +"67": 1, +"7": 3, +"70": 1, +"74": 1, +"75": 1, +"77": 1, +"79": 1, +"8": -14, +"83": 1, +"85": 1, +"86": 1, +"93": 1, +"94": 1, +"95": 1, +"96": 1, +"97": 1, +"99": 1 +}, +{ +"10": 1, +"102": 1, +"103": 1, +"104": 1, +"105": 1, +"106": 1, +"109": 1, +"11": -15, +"13": -1, +"17": 1, +"19": 1, +"23": 1, +"25": -10, +"26": 1, +"27": 1, +"28": 1, +"3": 4, +"30": 1, +"31": 1, +"32": 1, +"33": 1, +"35": 1, +"36": 1, +"39": 1, +"40": 1, +"41": 1, +"42": 1, +"45": 1, +"46": 1, +"49": 1, +"5": -9, +"52": 1, +"53": 1, +"59": 1, +"6": 1, +"60": 1, +"62": 1, +"63": 1, +"65": 1, +"7": 2, +"74": 1, +"76": 1, +"77": 1, +"78": 1, +"8": -11, +"80": 1, +"83": 1, +"84": 1, +"88": 1, +"9": 1, +"91": 1, +"93": 1, +"94": 1, +"95": 1, +"97": 1 +} +], +[ +{ +"100": 1, +"101": 1, +"103": 1, +"105": 1, +"107": 1, +"108": 1, +"11": -13, +"110": 1, +"13": -14, +"15": 1, +"17": 1, +"19": 1, +"20": 1, +"24": 1, +"25": -12, +"27": 1, +"3": 13, +"30": 1, +"31": 1, +"32": 1, +"36": 1, +"37": 1, +"38": 1, +"42": 1, +"43": 1, +"44": 1, +"45": 1, +"48": 1, +"49": 1, +"5": -13, +"54": 1, +"56": 1, +"57": 1, +"6": 8, +"60": 1, +"61": 1, +"65": 1, +"67": 1, +"7": 2, +"74": 1, +"75": 1, +"78": 1, +"79": 1, +"8": -15, +"80": 1, +"81": 1, +"82": 1, +"84": 1, +"85": 1, +"90": 1, +"93": 1, +"99": 1 +}, +{ +"10": 1, +"100": 1, +"101": 1, +"103": 1, +"107": 1, +"109": 1, +"11": -12, +"12": 1, +"13": -8, +"14": 1, +"17": 1, +"18": 1, +"19": 1, +"22": 1, +"23": 1, +"25": -16, +"26": 1, +"27": 1, +"28": 1, +"3": 9, +"32": 1, +"33": 1, +"34": 1, +"36": 1, +"37": 1, +"40": 1, +"41": 1, +"42": 1, +"45": 1, +"47": 1, +"49": 1, +"5": -14, +"50": 1, +"51": 1, +"53": 1, +"55": 1, +"56": 1, +"59": 1, +"6": 3, +"64": 1, +"65": 1, +"67": 1, +"7": -3, +"70": 1, +"72": 1, +"77": 1, +"79": 1, +"8": -14, +"80": 1, +"83": 1, +"84": 1, +"85": 1, +"87": 1, +"88": 1, +"89": 1, +"90": 1, +"93": 1, +"95": 1, +"97": 1, +"98": 1, +"99": 1 +}, +{ +"10": 1, +"100": 1, +"103": 1, +"104": 1, +"107": 1, +"109": 1, +"11": -11, +"13": -2, +"15": 1, +"16": 1, +"17": 1, +"19": 1, +"20": 1, +"21": 1, +"22": 1, +"24": 1, +"25": -11, +"27": 1, +"28": 1, +"3": 4, +"31": 1, +"33": 1, +"34": 1, +"36": 1, +"37": 1, +"38": 1, +"43": 1, +"47": 1, +"48": 1, +"5": -11, +"56": 1, +"58": 1, +"60": 1, +"66": 1, +"67": 1, +"68": 1, +"69": 1, +"7": -2, +"70": 1, +"71": 1, +"72": 1, +"74": 1, +"78": 1, +"79": 1, +"8": -14, +"81": 1, +"82": 1, +"83": 1, +"85": 1, +"86": 1, +"88": 1, +"89": 1, +"91": 1, +"93": 1, +"95": 1, +"96": 1, +"97": 1 +}, +{ +"10": 1, +"100": 1, +"101": 1, +"102": 1, +"103": 1, +"106": 1, +"11": -20, +"111": 1, +"13": -10, +"14": 1, +"15": 1, +"17": 1, +"20": 1, +"21": 1, +"25": -10, +"26": 1, +"28": 1, +"3": 13, +"32": 1, +"33": 1, +"35": 1, +"37": 1, +"38": 1, +"40": 1, +"43": 1, +"44": 1, +"47": 1, +"49": 1, +"5": -21, +"52": 1, +"53": 1, +"54": 1, +"55": 1, +"57": 1, +"6": 2, +"62": 1, +"63": 1, +"64": 1, +"65": 1, +"68": 1, +"69": 1, +"7": 4, +"70": 1, +"71": 1, +"72": 1, +"73": 1, +"74": 1, +"77": 1, +"78": 1, +"8": -11, +"81": 1, +"82": 1, +"83": 1, +"84": 1, +"85": 1, +"86": 1, +"88": 1, +"9": 1, +"91": 1, +"92": 1, +"95": 1 +} +], +[ +{ +"10": 1, +"101": 1, +"106": 1, +"11": -14, +"13": -24, +"15": 1, +"16": 1, +"18": 1, +"20": 1, +"21": 1, +"22": 1, +"25": -20, +"26": 1, +"27": 1, +"3": 22, +"33": 1, +"36": 1, +"37": 1, +"38": 1, +"40": 1, +"41": 1, +"44": 1, +"47": 1, +"49": 1, +"5": -23, +"51": 1, +"54": 1, +"55": 1, +"57": 1, +"6": 25, +"61": 1, +"64": 1, +"65": 1, +"7": 12, +"73": 1, +"74": 1, +"75": 1, +"79": 1, +"8": -15, +"82": 1, +"83": 1, +"85": 1, +"86": 1, +"87": 1, +"88": 1, +"89": 1, +"9": 1, +"90": 1, +"91": 1, +"92": 1, +"94": 1, +"96": 1, +"99": 1 +}, +{ +"10": 1, +"102": 1, +"106": 1, +"107": 1, +"108": 1, +"109": 1, +"11": -16, +"110": 1, +"111": 1, +"13": -4, +"14": 1, +"15": 1, +"17": 1, +"20": 1, +"21": 1, +"23": 1, +"24": 1, +"25": -10, +"26": 1, +"28": 1, +"3": 8, +"32": 1, +"35": 1, +"37": 1, +"38": 1, +"39": 1, +"42": 1, +"45": 1, +"46": 1, +"47": 1, +"48": 1, +"49": 1, +"5": -13, +"51": 1, +"53": 1, +"54": 1, +"56": 1, +"57": 1, +"59": 1, +"6": 1, +"60": 1, +"61": 1, +"63": 1, +"65": 1, +"68": 1, +"7": -1, +"71": 1, +"75": 1, +"76": 1, +"77": 1, +"8": -14, +"80": 1, +"81": 1, +"86": 1, +"87": 1, +"89": 1, +"90": 1, +"93": 1, +"95": 1, +"99": 1 +}, +{ +"10": 1, +"101": 1, +"102": 1, +"104": 1, +"105": 1, +"106": 1, +"11": -15, +"111": 1, +"13": -24, +"15": 1, +"16": 1, +"19": 1, +"22": 1, +"24": 1, +"25": -19, +"27": 1, +"3": 20, +"33": 1, +"36": 1, +"38": 1, +"40": 1, +"41": 1, +"42": 1, +"43": 1, +"46": 1, +"47": 1, +"5": -20, +"52": 1, +"53": 1, +"54": 1, +"55": 1, +"56": 1, +"57": 1, +"6": 22, +"61": 1, +"63": 1, +"64": 1, +"65": 1, +"66": 1, +"67": 1, +"69": 1, +"7": 12, +"70": 1, +"71": 1, +"75": 1, +"8": -17, +"80": 1, +"82": 1, +"83": 1, +"85": 1, +"88": 1, +"90": 1, +"91": 1, +"93": 1, +"94": 1 +}, +{ +"10": 1, +"100": 1, +"101": 1, +"105": 1, +"106": 1, +"108": 1, +"11": -14, +"13": -11, +"16": 1, +"17": 1, +"18": 1, +"20": 1, +"21": 1, +"24": 1, +"25": -14, +"26": 1, +"27": 1, +"28": 1, +"29": 1, +"3": 11, +"31": 1, +"33": 1, +"36": 1, +"37": 1, +"40": 1, +"41": 1, +"43": 1, +"45": 1, +"46": 1, +"49": 1, +"5": -14, +"50": 1, +"51": 1, +"54": 1, +"55": 1, +"59": 1, +"6": 9, +"60": 1, +"61": 1, +"62": 1, +"63": 1, +"64": 1, +"65": 1, +"67": 1, +"69": 1, +"7": 2, +"71": 1, +"72": 1, +"74": 1, +"77": 1, +"78": 1, +"8": -19, +"80": 1, +"81": 1, +"82": 1, +"83": 1, +"85": 1, +"91": 1, +"93": 1, +"94": 1, +"95": 1, +"96": 1, +"97": 1 +} +], +[ +{ +"10": 1, +"101": 1, +"106": 1, +"107": 1, +"108": 1, +"11": -11, +"111": 1, +"12": 1, +"13": -15, +"15": 1, +"16": 1, +"17": 1, +"18": 1, +"19": 1, +"23": 1, +"24": 1, +"25": -20, +"26": 1, +"27": 1, +"28": 1, +"29": 1, +"3": 15, +"30": 1, +"33": 1, +"35": 1, +"37": 1, +"39": 1, +"40": 1, +"43": 1, +"45": 1, +"47": 1, +"49": 1, +"5": -14, +"50": 1, +"52": 1, +"55": 1, +"58": 1, +"6": 17, +"61": 1, +"62": 1, +"63": 1, +"64": 1, +"67": 1, +"7": 3, +"71": 1, +"73": 1, +"75": 1, +"79": 1, +"8": -16, +"84": 1, +"87": 1, +"88": 1, +"9": 1, +"90": 1, +"92": 1, +"96": 1, +"97": 1 +}, +{ +"10": 1, +"100": 1, +"101": 1, +"103": 1, +"107": 1, +"109": 1, +"11": -15, +"110": 1, +"111": 1, +"13": -8, +"14": 1, +"15": 1, +"17": 1, +"20": 1, +"21": 1, +"23": 1, +"24": 1, +"25": -10, +"26": 1, +"3": 12, +"30": 1, +"32": 1, +"33": 1, +"34": 1, +"36": 1, +"37": 1, +"39": 1, +"40": 1, +"42": 1, +"43": 1, +"44": 1, +"49": 1, +"5": -16, +"51": 1, +"52": 1, +"53": 1, +"55": 1, +"57": 1, +"59": 1, +"6": -1, +"61": 1, +"62": 1, +"63": 1, +"67": 1, +"68": 1, +"69": 1, +"7": -2, +"75": 1, +"77": 1, +"78": 1, +"79": 1, +"8": -10, +"81": 1, +"83": 1, +"84": 1, +"85": 1, +"86": 1, +"88": 1, +"89": 1, +"92": 1, +"93": 1, +"95": 1, +"96": 1, +"97": 1, +"98": 1 +}, +{ +"102": 1, +"103": 1, +"104": 1, +"105": 1, +"107": 1, +"11": -19, +"110": 1, +"13": -3, +"15": 1, +"16": 1, +"17": 1, +"19": 1, +"20": 1, +"21": 1, +"22": 1, +"24": 1, +"25": -11, +"26": 1, +"28": 1, +"3": 10, +"30": 1, +"31": 1, +"32": 1, +"33": 1, +"34": 1, +"35": 1, +"40": 1, +"42": 1, +"45": 1, +"46": 1, +"5": -17, +"53": 1, +"56": 1, +"57": 1, +"58": 1, +"6": -2, +"62": 1, +"64": 1, +"67": 1, +"69": 1, +"7": 1, +"70": 1, +"71": 1, +"72": 1, +"74": 1, +"76": 1, +"77": 1, +"78": 1, +"79": 1, +"8": -10, +"80": 1, +"85": 1, +"86": 1, +"9": 1, +"90": 1, +"91": 1, +"92": 1, +"96": 1, +"98": 1, +"99": 1 +}, +{ +"100": 1, +"101": 1, +"102": 1, +"103": 1, +"104": 1, +"106": 1, +"107": 1, +"108": 1, +"109": 1, +"11": -22, +"110": 1, +"111": 1, +"12": 1, +"13": -1, +"16": 1, +"19": 1, +"20": 1, +"24": 1, +"25": -10, +"26": 1, +"27": 1, +"29": 1, +"3": 10, +"31": 1, +"32": 1, +"33": 1, +"34": 1, +"39": 1, +"41": 1, +"42": 1, +"43": 1, +"45": 1, +"46": 1, +"47": 1, +"48": 1, +"5": -16, +"51": 1, +"53": 1, +"56": 1, +"58": 1, +"59": 1, +"6": -5, +"62": 1, +"63": 1, +"64": 1, +"68": 1, +"69": 1, +"7": 3, +"72": 1, +"74": 1, +"76": 1, +"77": 1, +"8": -13, +"81": 1, +"83": 1, +"84": 1, +"85": 1, +"88": 1, +"89": 1, +"9": 1, +"91": 1, +"95": 1, +"96": 1, +"97": 1 +} +], +[ +{ +"103": 1, +"105": 1, +"107": 1, +"108": 1, +"11": -13, +"12": 1, +"13": -8, +"16": 1, +"17": 1, +"19": 1, +"20": 1, +"22": 1, +"24": 1, +"25": -13, +"29": 1, +"3": 9, +"30": 1, +"31": 1, +"32": 1, +"33": 1, +"34": 1, +"36": 1, +"37": 1, +"40": 1, +"44": 1, +"45": 1, +"5": -12, +"50": 1, +"57": 1, +"58": 1, +"6": 6, +"60": 1, +"62": 1, +"68": 1, +"7": -1, +"72": 1, +"73": 1, +"76": 1, +"77": 1, +"8": -14, +"80": 1, +"81": 1, +"83": 1, +"84": 1, +"85": 1, +"88": 1, +"89": 1, +"9": 1, +"91": 1, +"92": 1, +"97": 1, +"98": 1 +}, +{ +"100": 1, +"101": 1, +"104": 1, +"105": 1, +"106": 1, +"107": 1, +"11": -13, +"13": -22, +"14": 1, +"15": 1, +"18": 1, +"19": 1, +"21": 1, +"23": 1, +"25": -20, +"28": 1, +"3": 20, +"30": 1, +"31": 1, +"32": 1, +"34": 1, +"35": 1, +"36": 1, +"38": 1, +"41": 1, +"42": 1, +"43": 1, +"44": 1, +"49": 1, +"5": -19, +"52": 1, +"56": 1, +"57": 1, +"59": 1, +"6": 20, +"61": 1, +"62": 1, +"63": 1, +"64": 1, +"67": 1, +"68": 1, +"69": 1, +"7": 10, +"73": 1, +"74": 1, +"76": 1, +"8": -14, +"82": 1, +"85": 1, +"86": 1, +"87": 1, +"9": 1, +"91": 1, +"94": 1, +"95": 1, +"97": 1, +"99": 1 +}, +{ +"10": 1, +"100": 1, +"101": 1, +"102": 1, +"103": 1, +"105": 1, +"109": 1, +"11": -15, +"110": 1, +"13": -14, +"19": 1, +"20": 1, +"22": 1, +"23": 1, +"24": 1, +"25": -17, +"27": 1, +"3": 16, +"31": 1, +"36": 1, +"37": 1, +"38": 1, +"40": 1, +"41": 1, +"42": 1, +"45": 1, +"47": 1, +"48": 1, +"49": 1, +"5": -17, +"50": 1, +"58": 1, +"59": 1, +"6": 13, +"60": 1, +"62": 1, +"63": 1, +"64": 1, +"65": 1, +"66": 1, +"68": 1, +"7": 1, +"70": 1, +"72": 1, +"73": 1, +"74": 1, +"76": 1, +"77": 1, +"78": 1, +"79": 1, +"8": -21, +"84": 1, +"87": 1, +"89": 1, +"9": 1, +"90": 1, +"94": 1, +"95": 1, +"98": 1 +}, +{ +"10": 1, +"100": 1, +"101": 1, +"103": 1, +"105": 1, +"106": 1, +"107": 1, +"108": 1, +"109": 1, +"11": -13, +"110": 1, +"111": 1, +"13": -29, +"19": 1, +"20": 1, +"22": 1, +"24": 1, +"25": -26, +"3": 23, +"30": 1, +"32": 1, +"34": 1, +"35": 1, +"36": 1, +"43": 1, +"44": 1, +"45": 1, +"47": 1, +"49": 1, +"5": -21, +"52": 1, +"54": 1, +"55": 1, +"56": 1, +"59": 1, +"6": 32, +"60": 1, +"61": 1, +"64": 1, +"66": 1, +"68": 1, +"7": 12, +"70": 1, +"71": 1, +"74": 1, +"75": 1, +"78": 1, +"79": 1, +"8": -22, +"81": 1, +"82": 1, +"83": 1, +"84": 1, +"86": 1, +"88": 1, +"89": 1, +"9": 1, +"90": 1, +"97": 1, +"98": 1 +} +], +[ +{ +"10": 1, +"101": 1, +"102": 1, +"105": 1, +"107": 1, +"11": -13, +"13": 2, +"17": 1, +"18": 1, +"19": 1, +"20": 1, +"22": 1, +"25": -8, +"27": 1, +"29": 1, +"3": 2, +"33": 1, +"36": 1, +"37": 1, +"39": 1, +"40": 1, +"41": 1, +"42": 1, +"5": -10, +"50": 1, +"51": 1, +"52": 1, +"53": 1, +"55": 1, +"57": 1, +"58": 1, +"59": 1, +"6": -7, +"65": 1, +"67": 1, +"68": 1, +"69": 1, +"7": -2, +"70": 1, +"71": 1, +"72": 1, +"74": 1, +"79": 1, +"8": -9, +"83": 1, +"84": 1, +"85": 1, +"88": 1, +"9": 1, +"90": 1, +"91": 1, +"93": 1, +"95": 1, +"96": 1, +"97": 1 +}, +{ +"10": 1, +"101": 1, +"103": 1, +"106": 1, +"107": 1, +"109": 1, +"11": -13, +"12": 1, +"13": -8, +"14": 1, +"15": 1, +"17": 1, +"18": 1, +"21": 1, +"22": 1, +"23": 1, +"24": 1, +"25": -14, +"26": 1, +"28": 1, +"29": 1, +"3": 9, +"30": 1, +"33": 1, +"37": 1, +"38": 1, +"39": 1, +"45": 1, +"46": 1, +"5": -12, +"50": 1, +"52": 1, +"53": 1, +"54": 1, +"55": 1, +"57": 1, +"58": 1, +"6": 3, +"61": 1, +"62": 1, +"63": 1, +"64": 1, +"65": 1, +"66": 1, +"67": 1, +"68": 1, +"70": 1, +"72": 1, +"73": 1, +"74": 1, +"75": 1, +"77": 1, +"78": 1, +"79": 1, +"8": -12, +"84": 1, +"88": 1, +"93": 1, +"96": 1, +"98": 1, +"99": 1 +}, +{ +"10": 1, +"100": 1, +"101": 1, +"102": 1, +"104": 1, +"11": -16, +"12": 1, +"13": -15, +"14": 1, +"16": 1, +"18": 1, +"22": 1, +"23": 1, +"24": 1, +"25": -11, +"3": 15, +"31": 1, +"33": 1, +"35": 1, +"36": 1, +"41": 1, +"43": 1, +"47": 1, +"48": 1, +"5": -16, +"50": 1, +"51": 1, +"53": 1, +"59": 1, +"6": 7, +"60": 1, +"62": 1, +"63": 1, +"7": 6, +"72": 1, +"74": 1, +"78": 1, +"8": -10, +"81": 1, +"82": 1, +"83": 1, +"88": 1, +"90": 1, +"91": 1, +"92": 1, +"97": 1, +"99": 1 +}, +{ +"100": 1, +"102": 1, +"104": 1, +"106": 1, +"108": 1, +"109": 1, +"11": -26, +"110": 1, +"111": 1, +"12": 1, +"13": -4, +"14": 1, +"15": 1, +"17": 1, +"19": 1, +"20": 1, +"22": 1, +"24": 1, +"25": -10, +"27": 1, +"28": 1, +"3": 13, +"30": 1, +"31": 1, +"32": 1, +"33": 1, +"34": 1, +"35": 1, +"37": 1, +"38": 1, +"39": 1, +"40": 1, +"41": 1, +"42": 1, +"44": 1, +"48": 1, +"49": 1, +"5": -23, +"51": 1, +"52": 1, +"53": 1, +"54": 1, +"56": 1, +"58": 1, +"6": -3, +"60": 1, +"61": 1, +"62": 1, +"63": 1, +"64": 1, +"66": 1, +"7": 1, +"70": 1, +"73": 1, +"74": 1, +"76": 1, +"77": 1, +"78": 1, +"79": 1, +"8": -15, +"80": 1, +"81": 1, +"82": 1, +"84": 1, +"85": 1, +"86": 1, +"88": 1, +"9": 1, +"91": 1, +"93": 1, +"94": 1, +"95": 1, +"97": 1, +"98": 1 +} +], +[ +{ +"10": 1, +"101": 1, +"103": 1, +"104": 1, +"107": 1, +"11": -16, +"110": 1, +"111": 1, +"13": -6, +"14": 1, +"15": 1, +"16": 1, +"17": 1, +"18": 1, +"21": 1, +"23": 1, +"24": 1, +"25": -13, +"26": 1, +"28": 1, +"29": 1, +"3": 11, +"32": 1, +"33": 1, +"34": 1, +"35": 1, +"40": 1, +"41": 1, +"43": 1, +"44": 1, +"45": 1, +"5": -17, +"51": 1, +"52": 1, +"53": 1, +"55": 1, +"56": 1, +"58": 1, +"6": 2, +"60": 1, +"63": 1, +"66": 1, +"67": 1, +"69": 1, +"7": 2, +"71": 1, +"72": 1, +"74": 1, +"76": 1, +"79": 1, +"8": -14, +"80": 1, +"81": 1, +"82": 1, +"83": 1, +"84": 1, +"86": 1, +"87": 1, +"9": 1, +"90": 1, +"93": 1, +"94": 1, +"95": 1, +"96": 1, +"97": 1, +"98": 1 +}, +{ +"100": 1, +"101": 1, +"104": 1, +"108": 1, +"109": 1, +"11": -10, +"111": 1, +"12": 1, +"13": -10, +"14": 1, +"21": 1, +"22": 1, +"23": 1, +"25": -14, +"26": 1, +"28": 1, +"29": 1, +"3": 13, +"34": 1, +"35": 1, +"36": 1, +"38": 1, +"40": 1, +"45": 1, +"46": 1, +"47": 1, +"48": 1, +"49": 1, +"5": -14, +"50": 1, +"52": 1, +"57": 1, +"58": 1, +"6": 10, +"60": 1, +"62": 1, +"66": 1, +"68": 1, +"7": 3, +"73": 1, +"74": 1, +"77": 1, +"78": 1, +"8": -14, +"81": 1, +"83": 1, +"84": 1, +"89": 1, +"9": 1, +"93": 1, +"95": 1, +"96": 1, +"97": 1 +}, +{ +"100": 1, +"102": 1, +"103": 1, +"105": 1, +"106": 1, +"107": 1, +"108": 1, +"109": 1, +"11": -17, +"110": 1, +"111": 1, +"12": 1, +"13": -6, +"15": 1, +"18": 1, +"19": 1, +"20": 1, +"23": 1, +"25": -9, +"27": 1, +"29": 1, +"3": 11, +"30": 1, +"31": 1, +"37": 1, +"39": 1, +"43": 1, +"44": 1, +"45": 1, +"47": 1, +"48": 1, +"49": 1, +"5": -14, +"50": 1, +"53": 1, +"57": 1, +"6": -1, +"62": 1, +"63": 1, +"65": 1, +"67": 1, +"7": -1, +"72": 1, +"75": 1, +"78": 1, +"8": -14, +"83": 1, +"85": 1, +"87": 1, +"9": 1, +"90": 1, +"91": 1, +"93": 1, +"94": 1, +"95": 1, +"96": 1, +"99": 1 +}, +{ +"10": 1, +"100": 1, +"101": 1, +"102": 1, +"104": 1, +"107": 1, +"108": 1, +"109": 1, +"11": -16, +"110": 1, +"13": 1, +"14": 1, +"15": 1, +"17": 1, +"18": 1, +"19": 1, +"22": 1, +"25": -5, +"26": 1, +"29": 1, +"3": 8, +"34": 1, +"36": 1, +"39": 1, +"42": 1, +"44": 1, +"48": 1, +"49": 1, +"5": -15, +"51": 1, +"52": 1, +"53": 1, +"54": 1, +"58": 1, +"6": -8, +"60": 1, +"63": 1, +"65": 1, +"66": 1, +"69": 1, +"7": -1, +"70": 1, +"74": 1, +"75": 1, +"8": -8, +"80": 1, +"81": 1, +"82": 1, +"86": 1, +"88": 1, +"9": 1, +"92": 1, +"93": 1, +"94": 1, +"95": 1, +"97": 1 +} +], +[ +{ +"100": 1, +"102": 1, +"105": 1, +"106": 1, +"108": 1, +"109": 1, +"11": -15, +"110": 1, +"111": 1, +"12": 1, +"14": 1, +"16": 1, +"17": 1, +"18": 1, +"19": 1, +"22": 1, +"23": 1, +"25": -10, +"27": 1, +"28": 1, +"29": 1, +"3": 6, +"30": 1, +"32": 1, +"35": 1, +"38": 1, +"39": 1, +"40": 1, +"41": 1, +"42": 1, +"44": 1, +"45": 1, +"46": 1, +"48": 1, +"49": 1, +"5": -13, +"50": 1, +"51": 1, +"58": 1, +"6": -4, +"60": 1, +"61": 1, +"63": 1, +"66": 1, +"67": 1, +"68": 1, +"7": -3, +"71": 1, +"73": 1, +"77": 1, +"78": 1, +"8": -11, +"84": 1, +"87": 1, +"88": 1, +"89": 1, +"90": 1, +"92": 1, +"93": 1, +"99": 1 +}, +{ +"10": 1, +"101": 1, +"104": 1, +"105": 1, +"107": 1, +"11": -16, +"110": 1, +"12": 1, +"13": -24, +"15": 1, +"16": 1, +"20": 1, +"22": 1, +"24": 1, +"25": -22, +"27": 1, +"28": 1, +"3": 23, +"30": 1, +"32": 1, +"34": 1, +"35": 1, +"36": 1, +"38": 1, +"39": 1, +"40": 1, +"42": 1, +"43": 1, +"44": 1, +"45": 1, +"49": 1, +"5": -23, +"52": 1, +"55": 1, +"57": 1, +"6": 28, +"60": 1, +"62": 1, +"63": 1, +"64": 1, +"66": 1, +"7": 11, +"70": 1, +"71": 1, +"74": 1, +"75": 1, +"77": 1, +"8": -21, +"82": 1, +"83": 1, +"85": 1, +"86": 1, +"89": 1, +"9": 1, +"90": 1, +"98": 1 +}, +{ +"100": 1, +"102": 1, +"103": 1, +"105": 1, +"106": 1, +"11": -7, +"111": 1, +"12": 1, +"13": -7, +"17": 1, +"19": 1, +"24": 1, +"25": -14, +"27": 1, +"28": 1, +"29": 1, +"3": 5, +"32": 1, +"34": 1, +"36": 1, +"37": 1, +"38": 1, +"39": 1, +"40": 1, +"44": 1, +"46": 1, +"47": 1, +"5": -7, +"50": 1, +"52": 1, +"59": 1, +"6": 6, +"61": 1, +"62": 1, +"63": 1, +"66": 1, +"69": 1, +"7": -2, +"71": 1, +"73": 1, +"75": 1, +"76": 1, +"77": 1, +"78": 1, +"79": 1, +"8": -11, +"80": 1, +"83": 1, +"85": 1, +"86": 1, +"89": 1, +"93": 1, +"95": 1 +}, +{ +"101": 1, +"102": 1, +"103": 1, +"105": 1, +"108": 1, +"11": -16, +"12": 1, +"13": -16, +"15": 1, +"16": 1, +"17": 1, +"19": 1, +"24": 1, +"25": -16, +"26": 1, +"29": 1, +"3": 14, +"31": 1, +"32": 1, +"33": 1, +"34": 1, +"35": 1, +"37": 1, +"38": 1, +"39": 1, +"41": 1, +"45": 1, +"48": 1, +"49": 1, +"5": -18, +"50": 1, +"52": 1, +"58": 1, +"6": 13, +"64": 1, +"7": 1, +"70": 1, +"75": 1, +"77": 1, +"78": 1, +"79": 1, +"8": -15, +"80": 1, +"81": 1, +"84": 1, +"85": 1, +"87": 1, +"89": 1, +"9": 1, +"90": 1, +"92": 1, +"94": 1, +"97": 1, +"98": 1, +"99": 1 +} +], +[ +{ +"10": 1, +"101": 1, +"102": 1, +"103": 1, +"104": 1, +"106": 1, +"108": 1, +"109": 1, +"11": -16, +"110": 1, +"111": 1, +"13": -2, +"14": 1, +"17": 1, +"18": 1, +"19": 1, +"22": 1, +"23": 1, +"24": 1, +"25": -11, +"27": 1, +"28": 1, +"29": 1, +"3": 5, +"31": 1, +"32": 1, +"33": 1, +"39": 1, +"40": 1, +"46": 1, +"47": 1, +"5": -12, +"50": 1, +"51": 1, +"52": 1, +"53": 1, +"54": 1, +"59": 1, +"6": -3, +"61": 1, +"62": 1, +"68": 1, +"69": 1, +"7": -3, +"71": 1, +"72": 1, +"78": 1, +"8": -9, +"81": 1, +"82": 1, +"83": 1, +"84": 1, +"87": 1, +"88": 1, +"89": 1, +"9": 1, +"90": 1, +"93": 1, +"94": 1, +"97": 1, +"99": 1 +}, +{ +"10": 1, +"100": 1, +"102": 1, +"104": 1, +"105": 1, +"108": 1, +"11": -13, +"110": 1, +"13": -10, +"15": 1, +"16": 1, +"18": 1, +"19": 1, +"23": 1, +"25": -12, +"27": 1, +"3": 14, +"30": 1, +"32": 1, +"33": 1, +"34": 1, +"36": 1, +"41": 1, +"42": 1, +"43": 1, +"46": 1, +"48": 1, +"5": -15, +"52": 1, +"54": 1, +"55": 1, +"59": 1, +"6": 6, +"60": 1, +"61": 1, +"62": 1, +"65": 1, +"67": 1, +"7": 3, +"70": 1, +"75": 1, +"79": 1, +"8": -11, +"82": 1, +"85": 1, +"89": 1, +"9": 1, +"90": 1, +"93": 1, +"97": 1 +}, +{ +"10": 1, +"100": 1, +"101": 1, +"102": 1, +"103": 1, +"104": 1, +"105": 1, +"108": 1, +"11": -16, +"12": 1, +"13": -11, +"15": 1, +"17": 1, +"19": 1, +"20": 1, +"23": 1, +"25": -14, +"26": 1, +"27": 1, +"29": 1, +"3": 13, +"33": 1, +"37": 1, +"38": 1, +"40": 1, +"44": 1, +"45": 1, +"46": 1, +"47": 1, +"48": 1, +"5": -17, +"50": 1, +"52": 1, +"54": 1, +"55": 1, +"58": 1, +"59": 1, +"6": 4, +"60": 1, +"61": 1, +"62": 1, +"64": 1, +"66": 1, +"67": 1, +"68": 1, +"70": 1, +"74": 1, +"75": 1, +"76": 1, +"79": 1, +"8": -15, +"82": 1, +"83": 1, +"85": 1, +"90": 1, +"91": 1, +"92": 1, +"93": 1, +"94": 1, +"98": 1, +"99": 1 +}, +{ +"100": 1, +"108": 1, +"11": -14, +"110": 1, +"111": 1, +"12": 1, +"13": -7, +"14": 1, +"15": 1, +"16": 1, +"18": 1, +"19": 1, +"25": -10, +"26": 1, +"27": 1, +"28": 1, +"3": 6, +"38": 1, +"39": 1, +"41": 1, +"44": 1, +"46": 1, +"47": 1, +"48": 1, +"49": 1, +"5": -14, +"50": 1, +"51": 1, +"52": 1, +"53": 1, +"55": 1, +"56": 1, +"57": 1, +"59": 1, +"6": 4, +"60": 1, +"66": 1, +"68": 1, +"7": 3, +"71": 1, +"72": 1, +"75": 1, +"8": -12, +"81": 1, +"82": 1, +"83": 1, +"85": 1, +"86": 1, +"88": 1, +"89": 1, +"91": 1, +"94": 1, +"96": 1, +"97": 1 +} +], +[ +{ +"100": 1, +"101": 1, +"102": 1, +"106": 1, +"107": 1, +"108": 1, +"109": 1, +"11": -13, +"110": 1, +"13": -9, +"14": 1, +"17": 1, +"21": 1, +"22": 1, +"24": 1, +"25": -15, +"26": 1, +"27": 1, +"28": 1, +"29": 1, +"3": 11, +"30": 1, +"32": 1, +"34": 1, +"35": 1, +"38": 1, +"41": 1, +"42": 1, +"43": 1, +"46": 1, +"47": 1, +"49": 1, +"5": -17, +"51": 1, +"53": 1, +"54": 1, +"56": 1, +"58": 1, +"59": 1, +"6": 6, +"60": 1, +"63": 1, +"68": 1, +"69": 1, +"7": 3, +"71": 1, +"73": 1, +"75": 1, +"78": 1, +"79": 1, +"8": -13, +"80": 1, +"82": 1, +"83": 1, +"85": 1, +"86": 1, +"87": 1, +"89": 1, +"9": 1, +"93": 1, +"94": 1, +"95": 1, +"96": 1, +"99": 1 +}, +{ +"102": 1, +"103": 1, +"104": 1, +"105": 1, +"106": 1, +"108": 1, +"11": -18, +"111": 1, +"13": -10, +"17": 1, +"18": 1, +"19": 1, +"20": 1, +"24": 1, +"25": -11, +"29": 1, +"3": 11, +"31": 1, +"32": 1, +"34": 1, +"35": 1, +"37": 1, +"38": 1, +"41": 1, +"42": 1, +"46": 1, +"49": 1, +"5": -18, +"50": 1, +"51": 1, +"52": 1, +"54": 1, +"56": 1, +"57": 1, +"6": 5, +"60": 1, +"63": 1, +"66": 1, +"69": 1, +"7": 4, +"70": 1, +"71": 1, +"73": 1, +"76": 1, +"78": 1, +"8": -14, +"80": 1, +"82": 1, +"84": 1, +"86": 1, +"88": 1, +"89": 1, +"90": 1, +"92": 1, +"93": 1, +"94": 1, +"95": 1 +}, +{ +"102": 1, +"103": 1, +"104": 1, +"105": 1, +"108": 1, +"109": 1, +"11": -13, +"110": 1, +"13": -2, +"15": 1, +"16": 1, +"18": 1, +"19": 1, +"22": 1, +"25": -14, +"27": 1, +"28": 1, +"29": 1, +"3": 5, +"30": 1, +"34": 1, +"35": 1, +"39": 1, +"40": 1, +"42": 1, +"45": 1, +"46": 1, +"48": 1, +"5": -10, +"50": 1, +"51": 1, +"56": 1, +"57": 1, +"6": 6, +"60": 1, +"65": 1, +"66": 1, +"68": 1, +"69": 1, +"7": 2, +"76": 1, +"77": 1, +"79": 1, +"8": -13, +"81": 1, +"84": 1, +"85": 1, +"87": 1, +"88": 1, +"89": 1, +"90": 1, +"95": 1, +"96": 1, +"97": 1 +}, +{ +"10": 1, +"101": 1, +"105": 1, +"106": 1, +"108": 1, +"11": -18, +"110": 1, +"111": 1, +"13": -15, +"14": 1, +"15": 1, +"16": 1, +"17": 1, +"21": 1, +"23": 1, +"24": 1, +"25": -14, +"27": 1, +"29": 1, +"3": 16, +"32": 1, +"36": 1, +"38": 1, +"40": 1, +"41": 1, +"42": 1, +"43": 1, +"44": 1, +"45": 1, +"5": -19, +"50": 1, +"51": 1, +"53": 1, +"54": 1, +"55": 1, +"57": 1, +"58": 1, +"6": 11, +"61": 1, +"64": 1, +"65": 1, +"66": 1, +"67": 1, +"69": 1, +"7": 9, +"72": 1, +"73": 1, +"75": 1, +"78": 1, +"8": -14, +"81": 1, +"83": 1, +"86": 1, +"88": 1, +"89": 1, +"9": 1, +"91": 1, +"92": 1, +"97": 1, +"98": 1, +"99": 1 +} +], +[ +{ +"10": 1, +"102": 1, +"104": 1, +"105": 1, +"11": -14, +"110": 1, +"111": 1, +"12": 1, +"13": -6, +"15": 1, +"16": 1, +"18": 1, +"19": 1, +"20": 1, +"21": 1, +"23": 1, +"25": -8, +"27": 1, +"28": 1, +"29": 1, +"3": 10, +"32": 1, +"40": 1, +"43": 1, +"46": 1, +"47": 1, +"48": 1, +"49": 1, +"5": -18, +"51": 1, +"52": 1, +"54": 1, +"56": 1, +"58": 1, +"6": -1, +"65": 1, +"67": 1, +"68": 1, +"70": 1, +"71": 1, +"75": 1, +"76": 1, +"77": 1, +"78": 1, +"79": 1, +"8": -11, +"80": 1, +"82": 1, +"83": 1, +"85": 1, +"89": 1, +"93": 1, +"94": 1, +"97": 1, +"98": 1 +}, +{ +"10": 1, +"101": 1, +"102": 1, +"104": 1, +"107": 1, +"11": -15, +"111": 1, +"12": 1, +"13": -3, +"21": 1, +"23": 1, +"25": -9, +"26": 1, +"27": 1, +"28": 1, +"29": 1, +"3": 8, +"32": 1, +"33": 1, +"39": 1, +"40": 1, +"45": 1, +"5": -17, +"52": 1, +"54": 1, +"55": 1, +"57": 1, +"59": 1, +"60": 1, +"63": 1, +"64": 1, +"65": 1, +"66": 1, +"67": 1, +"68": 1, +"7": 2, +"71": 1, +"73": 1, +"74": 1, +"78": 1, +"8": -10, +"80": 1, +"82": 1, +"85": 1, +"86": 1, +"88": 1, +"9": 1, +"92": 1, +"93": 1, +"94": 1, +"96": 1, +"97": 1, +"98": 1, +"99": 1 +}, +{ +"101": 1, +"103": 1, +"106": 1, +"109": 1, +"11": -12, +"13": -13, +"14": 1, +"15": 1, +"16": 1, +"17": 1, +"18": 1, +"24": 1, +"25": -14, +"28": 1, +"3": 11, +"31": 1, +"34": 1, +"35": 1, +"37": 1, +"38": 1, +"40": 1, +"43": 1, +"46": 1, +"47": 1, +"48": 1, +"5": -14, +"50": 1, +"51": 1, +"53": 1, +"54": 1, +"59": 1, +"6": 9, +"62": 1, +"64": 1, +"65": 1, +"68": 1, +"69": 1, +"7": 4, +"70": 1, +"72": 1, +"73": 1, +"74": 1, +"76": 1, +"79": 1, +"8": -11, +"81": 1, +"83": 1, +"84": 1, +"85": 1, +"88": 1, +"9": 1, +"96": 1, +"99": 1 +}, +{ +"100": 1, +"101": 1, +"102": 1, +"107": 1, +"108": 1, +"11": -17, +"13": -7, +"14": 1, +"15": 1, +"17": 1, +"18": 1, +"20": 1, +"22": 1, +"25": -15, +"26": 1, +"27": 1, +"28": 1, +"3": 11, +"30": 1, +"31": 1, +"32": 1, +"33": 1, +"35": 1, +"39": 1, +"40": 1, +"41": 1, +"44": 1, +"47": 1, +"5": -20, +"51": 1, +"52": 1, +"53": 1, +"55": 1, +"57": 1, +"58": 1, +"59": 1, +"6": 5, +"60": 1, +"61": 1, +"62": 1, +"64": 1, +"67": 1, +"68": 1, +"7": 4, +"73": 1, +"74": 1, +"76": 1, +"77": 1, +"79": 1, +"8": -12, +"80": 1, +"82": 1, +"83": 1, +"84": 1, +"85": 1, +"86": 1, +"87": 1, +"89": 1, +"90": 1, +"91": 1, +"94": 1, +"97": 1 +} +], +[ +{ +"102": 1, +"103": 1, +"105": 1, +"106": 1, +"108": 1, +"11": -16, +"110": 1, +"12": 1, +"13": -10, +"15": 1, +"16": 1, +"21": 1, +"25": -11, +"27": 1, +"3": 12, +"30": 1, +"33": 1, +"35": 1, +"40": 1, +"43": 1, +"45": 1, +"47": 1, +"48": 1, +"49": 1, +"5": -19, +"50": 1, +"54": 1, +"55": 1, +"56": 1, +"57": 1, +"58": 1, +"59": 1, +"6": 6, +"60": 1, +"63": 1, +"66": 1, +"67": 1, +"68": 1, +"7": 2, +"71": 1, +"72": 1, +"73": 1, +"74": 1, +"75": 1, +"79": 1, +"8": -16, +"80": 1, +"86": 1, +"88": 1, +"89": 1, +"9": 1, +"91": 1, +"94": 1, +"95": 1, +"98": 1 +}, +{ +"10": 1, +"100": 1, +"101": 1, +"103": 1, +"104": 1, +"107": 1, +"108": 1, +"109": 1, +"11": -19, +"110": 1, +"12": 1, +"13": -7, +"14": 1, +"15": 1, +"16": 1, +"19": 1, +"20": 1, +"25": -11, +"27": 1, +"3": 11, +"30": 1, +"31": 1, +"32": 1, +"34": 1, +"35": 1, +"36": 1, +"37": 1, +"38": 1, +"42": 1, +"43": 1, +"44": 1, +"45": 1, +"46": 1, +"48": 1, +"49": 1, +"5": -16, +"53": 1, +"54": 1, +"58": 1, +"59": 1, +"6": -2, +"60": 1, +"61": 1, +"62": 1, +"65": 1, +"67": 1, +"69": 1, +"7": -2, +"70": 1, +"72": 1, +"75": 1, +"76": 1, +"77": 1, +"78": 1, +"79": 1, +"8": -19, +"81": 1, +"82": 1, +"83": 1, +"84": 1, +"87": 1, +"89": 1, +"9": 1, +"91": 1, +"93": 1, +"95": 1, +"96": 1, +"97": 1, +"98": 1 +}, +{ +"10": 1, +"100": 1, +"104": 1, +"105": 1, +"107": 1, +"108": 1, +"109": 1, +"11": -13, +"111": 1, +"13": -20, +"15": 1, +"18": 1, +"20": 1, +"22": 1, +"24": 1, +"25": -23, +"26": 1, +"27": 1, +"28": 1, +"29": 1, +"3": 17, +"30": 1, +"32": 1, +"34": 1, +"35": 1, +"37": 1, +"38": 1, +"39": 1, +"43": 1, +"45": 1, +"46": 1, +"47": 1, +"49": 1, +"5": -18, +"52": 1, +"54": 1, +"55": 1, +"56": 1, +"57": 1, +"59": 1, +"6": 21, +"60": 1, +"61": 1, +"64": 1, +"67": 1, +"68": 1, +"7": 5, +"71": 1, +"72": 1, +"74": 1, +"75": 1, +"77": 1, +"78": 1, +"79": 1, +"8": -18, +"81": 1, +"82": 1, +"84": 1, +"85": 1, +"87": 1, +"88": 1, +"92": 1, +"93": 1, +"94": 1, +"95": 1, +"98": 1, +"99": 1 +}, +{ +"10": 1, +"102": 1, +"105": 1, +"106": 1, +"108": 1, +"109": 1, +"11": -13, +"111": 1, +"12": 1, +"13": -23, +"16": 1, +"17": 1, +"18": 1, +"19": 1, +"20": 1, +"22": 1, +"25": -23, +"27": 1, +"29": 1, +"3": 18, +"32": 1, +"33": 1, +"34": 1, +"36": 1, +"38": 1, +"43": 1, +"46": 1, +"47": 1, +"49": 1, +"5": -17, +"50": 1, +"51": 1, +"52": 1, +"56": 1, +"57": 1, +"58": 1, +"59": 1, +"6": 24, +"60": 1, +"62": 1, +"63": 1, +"64": 1, +"65": 1, +"66": 1, +"68": 1, +"7": 6, +"70": 1, +"73": 1, +"75": 1, +"76": 1, +"77": 1, +"78": 1, +"79": 1, +"8": -21, +"81": 1, +"83": 1, +"84": 1, +"87": 1, +"9": 1, +"91": 1, +"92": 1, +"95": 1, +"96": 1, +"97": 1, +"98": 1 +} +] +], +"kernel_lines": [ +1, +2, +3, +4, +5, +6, +7, +8, +9, +10, +11, +12, +13, +14, +15, +1, +2, +3, +4, +5, +6, +7, +8, +9, +10, +11, +12 +], +"seed": 20, +"stage_maps_eta": [ +[ +0, +1, +7, +13 +], +[ +11, +0, +1, +12 +], +[ +6, +6, +13, +12 +], +[ +7, +13, +0, +6 +], +[ +7, +11, +7, +6 +], +[ +11, +10, +10, +7 +], +[ +6, +13, +11, +7 +], +[ +7, +1, +13, +0 +], +[ +1, +11, +13, +1 +], +[ +1, +10, +12, +10 +], +[ +13, +7, +6, +10 +], +[ +12, +10, +1, +1 +], +[ +13, +10, +12, +1 +], +[ +13, +12, +7, +11 +], +[ +1, +11, +13, +7 +], +[ +0, +11, +12, +6 +], +[ +12, +0, +13, +10 +], +[ +1, +1, +7, +11 +], +[ +12, +1, +0, +11 +], +[ +6, +12, +6, +1 +], +[ +13, +7, +7, +1 +], +[ +10, +13, +7, +1 +], +[ +12, +1, +7, +0 +], +[ +10, +13, +6, +10 +], +[ +7, +10, +6, +10 +], +[ +1, +7, +12, +6 +], +[ +7, +10, +11, +11 +] +] +} diff --git a/research/refined-recovery-overlap-floor/PROOF.md b/research/refined-recovery-overlap-floor/PROOF.md index c174964866..052b895a90 100644 --- a/research/refined-recovery-overlap-floor/PROOF.md +++ b/research/refined-recovery-overlap-floor/PROOF.md @@ -109,10 +109,37 @@ frame needs ⌈log₂ A_27⌉ = 796 bits. onto E. Their kernels cover 12 nonzero points twice and 3 points once, so they meet trivially and the map is injective. This pattern gives Σ_x P(x) = 1 + 12ρ₂^25 + 3ρ₂^26 = 15.789775 (exact rational in verify.py). It -exceeds the floor by less than 10⁻⁴. So among four-dimensional dependency -spaces, the bound is essentially the true minimum of (1). Whether frames in G -can realize this pattern is **not** established. For example, if the first 26 -stages form a direct sum, the 27th coordinate map is forced to be injective. +exceeds the floor by less than 10⁻⁴. + +**Realization by actual frames.** FRAMES27.json gives integer blocks V_1 = 0, +V_2, …, V_27 with MᵀV_j = 0 and E V_j = 0, where E is the rows 0, 1, 2, 4 as in +#6660. With W_j = I + V_j E and U_j = I + (V_j − V_(j+1))E, these are +mode-preserving frames, by the same algebra as #6660 §6. verify.py does not +trust their derivation. From the committed integers it checks: + +* MᵀV_j = 0 and E V_j = 0; +* the 27 binary images W_jM span exactly 104 dimensions; +* the dependency space D is 4-dimensional and lies in E^27; +* Σ_{a∈D} Π_j ρ(a_j) equals 1 + 12ρ₂^25 + 3ρ₂^26 exactly. + +Hence, at depth 27, + + 15.78976 F^27 ≤ min over frame sequences of |fiber(0)| ≤ 15.789775 F^27. + +**How the frames are built** (`build_frames.py`, deterministic): +1. Realizable images are graphs N = {μ(a) + ψ(a)}, where μ is M mod 2 and ψ is + any map into R′. Here R′ is the mod-2 reduction of {v ∈ ℤ^112 : Mᵀv = 0, + v_E = 0}. It has dimension 100 and complements im M; the script finds a ℤ-basis + by unimodular column reduction. +2. A relation Σ_j φ_j(a_j) = 0 therefore splits into Σ_j a_j = 0 and + Σ_j ψ_j(a_j) = 0. +3. Choose rank-3 maps ℓ_j onto E with Σ_j ℓ_j = 0 and kernels covering 12 lines + twice and 3 lines once. +4. Choose ψ_1 = 0 and ψ_2, …, ψ_22 at random. Solve Σ_j ψ_j ℓ_j = 0 for the last + five maps, adding a random homogeneous part. Seed 20 gives full rank 104. + +A direct-sum prefix of 26 stages cannot work, because it would force the 27th +coordinate map to be injective. These frames avoid such a prefix. ## 4. Larger depth @@ -126,9 +153,9 @@ evaluate. Asymptotically, d = 4t − 104 gives roughly 16^(t−26) ρ₂^(7t/8) This is a lower bound for the zero fiber, and hence for the optimal maximum fiber, of PR6660's exact interface: fixed known frames in G, one precision bit, -unbounded integers and full output access. It is not the exact optimum. -Realizability of the near-optimal pattern and the true maximum fiber at -t ≥ 27 remain open. It supplies no codec, physical tag, caller or restoration +unbounded integers and full output access. At t = 27 explicit frames pin the +minimum zero fiber to a window of relative width 10⁻⁶. The exact minimum and +the maximum fiber of those frames, and hence the exact optimum, remain open. It supplies no codec, physical tag, caller or restoration cost. κ, the selected frontier and its five assumptions are unchanged. PR6660's theorems (Z) and (c) are cited premises at its pinned head, not replayed; that PR is open at the time of writing. The written proof is diff --git a/research/refined-recovery-overlap-floor/README.md b/research/refined-recovery-overlap-floor/README.md index b51ebf4950..a386b272cd 100644 --- a/research/refined-recovery-overlap-floor/README.md +++ b/research/refined-recovery-overlap-floor/README.md @@ -35,10 +35,15 @@ identity-frame value A_t. even-coset plane E, not by injective ones, because ρ₂⁷ < ρ₁⁸ (ratio 1 − 1.2·10⁻⁷). -At t = 27 an abstract pattern of 27 such maps reaches 1 + 12ρ₂^25 + 3ρ₂^26, which is -within 10⁻⁴ of the floor. The bound is therefore essentially sharp for -four-dimensional dependency spaces. Whether actual frames realize that pattern is -open. See [PROOF.md](PROOF.md). +**Realized by actual frames.** [FRAMES27.json](FRAMES27.json) holds 27 explicit +mode-preserving frames, W_j = I + V_jE as in #6660. Their dependency space +consists of exactly those rank-3 maps onto E, so + + 15.78976 F^27 ≤ min over frames of |fiber(0)| ≤ 15.789775 F^27 (t = 27). + +This settles the first step of #6660's question to six significant figures. +[build_frames.py](build_frames.py) regenerates the frames deterministically. +See [PROOF.md](PROOF.md). ## Reproduce @@ -53,7 +58,13 @@ python3.12 -B scripts/research_package.py --package research/refined-recovery-ov Each run prints `PASS_REFINED_RECOVERY_OVERLAP_FLOOR` in under a second. It derives C from the pinned matrix and checks every number stated above in exact rational arithmetic, including all 67 subspaces of F2^8/C for μ_d (d ≤ 8). It -recomputes RESULT.json and runs two failure controls. +also checks the committed frames from their integers alone, recomputes +RESULT.json and runs two failure controls. + +```sh +python3.12 -B research/refined-recovery-overlap-floor/build_frames.py "$SCRATCH/FRAMES27.json" +cmp "$SCRATCH/FRAMES27.json" research/refined-recovery-overlap-floor/FRAMES27.json +``` ## Limitations @@ -68,10 +79,10 @@ review is claimed. ## Open next questions -1. **Realizable minimum and max fiber at t = 27.** Can frames in G realize a - dependency space whose stage maps are rank-3 maps onto E? If the first 26 - stages form a direct sum, the 27th map is forced to be injective. Is the - maximum fiber equal to the zero fiber there? +1. **Max fiber at t = 27.** For the frames in FRAMES27.json, does any output + have a larger fiber than the zero output? If not, the depth-27 optimum lies + within the window above. First step: extend #6660's stage-by-stage box count + to the coupled stages of a 4-dimensional E-valued dependency. 2. **Upper side.** Beat the identity-frame bound A_t with one four-dimensional overlap, by extending PR6660's stage-by-stage box lemma to one coupled pair of stages. The present window is about 100 bits. diff --git a/research/refined-recovery-overlap-floor/TASK.json b/research/refined-recovery-overlap-floor/TASK.json index 54f6ccb638..56456146d5 100644 --- a/research/refined-recovery-overlap-floor/TASK.json +++ b/research/refined-recovery-overlap-floor/TASK.json @@ -63,21 +63,21 @@ ] }, "scope_status": "changed", - "actual_scope": "Quantitative lower bound on the optimal worst-case recovery fiber of PR6660 refined chains at every depth t>=27, from its zero-fiber kernel formula: |fiber(0)| >= F^t (1+(2^d-1) mu_d^(t/(2^d-1))) for 1<=d<=4t-104, with mu_d exact; at t=27 this is > 15.7897 F^27, i.e. at least 696 tag bits versus 692 for a direct sum.", + "actual_scope": "Quantitative lower bound on the optimal worst-case recovery fiber of PR6660 refined chains at every depth t>=27, from its zero-fiber kernel formula: |fiber(0)| >= F^t (1+(2^d-1) mu_d^(t/(2^d-1))) for 1<=d<=4t-104, with mu_d exact; at t=27 this is > 15.7897 F^27, i.e. at least 696 tag bits versus 692 for a direct sum. Explicit 27-frame sequence attains 1+12rho2^25+3rho2^26 (15.789775 F^27), pinning the minimum depth-27 zero fiber.", "scope_change_reason": "Answers the first step of PR6660 open question 1 (minimize the zero-fiber kernel sum at t=27 over overlap patterns) with a bound for every overlap pattern. Like its predecessor this is precision-state accounting in the analytic_recovery interface, not a caller-bound discharge of a selected assumption.", "bottleneck_link": "Side result for exact history accounting in the inherited rounded interface; it changes no supplier invoice.", "budget_minutes": 60, "stop_rule": "Stop at the all-pattern zero-fiber floor with an exact t=27 constant and its near-attainment by an abstract pattern; leave the exact max-fiber optimum and realizability by frames open.", "outcome": "completed", - "evidence": "PROOF.md; verify.py (exact rational arithmetic, normal and optimized Python) writes and rechecks RESULT.json.", + "evidence": "PROOF.md; verify.py (exact rational arithmetic, normal and optimized Python) checks FRAMES27.json from its integers and writes/rechecks RESULT.json; build_frames.py regenerates FRAMES27.json.", "author": "apoursh", "ai_assistance": "Anthropic Claude (Claude Code) found the argument, wrote the verifier and ran the checks under apoursh direction. Independent human and formal proof-kernel review are unclaimed.", "open_questions": [ { - "question": "Is the t=27 optimum (max fiber) equal to its zero-fiber value, and what is the minimum of the zero fiber over frame sequences that are actually realizable?", - "why_it_matters": "Together with this floor it would give the exact depth-27 tag size.", - "first_step": "Decide whether frames in G can realize a dependency space whose 27 coordinate maps are rank-3 maps onto the even-coset plane E, the near-optimal abstract pattern here.", - "blocked_by": "With a direct-sum prefix of 26 stages the 27th coordinate map is forced to be injective; other realizable overlap patterns are not classified." + "question": "Is the maximum fiber of the FRAMES27.json sequence equal to its zero fiber, and what is the exact minimum zero fiber at t=27?", + "why_it_matters": "Either would turn the six-digit window into the exact depth-27 optimum.", + "first_step": "Extend the PR6660 stage-by-stage box count to the coupled stages of a 4-dimensional E-valued dependency.", + "blocked_by": "Coupled stage cosets break the per-stage box lemma; the abstract minimum over mixed map types is not computed exactly." }, { "question": "Can the identity-frame upper bound A_t be improved at t>=27 by a frame sequence with a single 4-dimensional overlap?", diff --git a/research/refined-recovery-overlap-floor/VERIFY.json b/research/refined-recovery-overlap-floor/VERIFY.json index 391d78fd94..0d5364ebd4 100644 --- a/research/refined-recovery-overlap-floor/VERIFY.json +++ b/research/refined-recovery-overlap-floor/VERIFY.json @@ -17,7 +17,7 @@ "{package}/verify.py" ], "timeout_seconds": 60, - "checks": "Fixture hash; C=[8,4,4] self-dual from M; exact coset sums and the even-coset plane E; rho2^7=3; certified t=27 floor 49343/3125; abstract near-attaining pattern; t=27..40 table against A_t; RESULT.json recomputation; controls." + "checks": "Fixture hash; C=[8,4,4] self-dual from M; exact coset sums and the even-coset plane E; rho2^7=3; certified t=27 floor 49343/3125; abstract near-attaining pattern; FRAMES27.json integrality, M\u1d40V=0, EV=0, 104-dimensional span, 4-dimensional E-valued dependency and exact zero-fiber value; t=27..40 table against A_t; RESULT.json recomputation; controls." }, { "argv": [ diff --git a/research/refined-recovery-overlap-floor/build_frames.py b/research/refined-recovery-overlap-floor/build_frames.py new file mode 100644 index 0000000000..c7a636f90c --- /dev/null +++ b/research/refined-recovery-overlap-floor/build_frames.py @@ -0,0 +1,129 @@ +"""Deterministically build FRAMES27.json: 27 mode-preserving frames attaining the +near-optimal depth-27 zero-fiber pattern (rank-3 stage maps onto E). + +Usage: python3 build_frames.py OUT.json (verify.py does not trust this derivation) +""" +import json, pathlib, random, sys +HERE = pathlib.Path(__file__).resolve().parent +FIXTURE = HERE.parent / "precision-state-frontier" / "FIXTURE.json" +cols=json.loads(FIXTURE.read_text())['mode_columns'] +rows=[tuple(cols[j][i] for j in range(8)) for i in range(112)] +rows=[tuple(cols[j][i] for j in range(8)) for i in range(112)] +EIDX=[0,1,2,4]; free=[i for i in range(112) if i not in EIDX] +# integer kernel basis of A (8 x 108) by unimodular column ops: A U = [H|0] +A=[[rows[i][k] for i in free] for k in range(8)] +n=len(free); U=[[int(i==j) for j in range(n)] for i in range(n)] # U columns +def colop(c1,c2,f): # col c1 -= f*col c2 + for r in A: r[c1]-=f*r[c2] + for r in U: r[c1]-=f*r[c2] +def swap(c1,c2): + for r in A: r[c1],r[c2]=r[c2],r[c1] + for r in U: r[c1],r[c2]=r[c2],r[c1] +piv=0 +for k in range(8): + while True: + nz=[c for c in range(piv,n) if A[k][c]!=0] + if len(nz)<=1: break + c0=min(nz,key=lambda c:abs(A[k][c])) + for c in nz: + if c!=c0: colop(c,c0,A[k][c]//A[k][c0]) + nz=[c for c in range(piv,n) if A[k][c]!=0] + if nz: swap(piv,nz[0]); piv+=1 +assert piv==8 +kern=[[U[i][c] for i in range(n)] for c in range(8,n)] +for v in kern: + for k in range(8): assert sum(rows[free[i]][k]*v[i] for i in range(n))==0 +full=[] +for v in kern: + w=[0]*112 + for i,x in zip(free,v): w[i]=x + full.append(w) +kern=full +from fractions import Fraction +EIDX=[0,1,2,4]; T=27 +wt=lambda u:bin(u).count('1') +par=lambda i,q: sum(rows[i][k] for k in range(8) if q>>k&1)&1 +eta=lambda q: sum(par(EIDX[b],q)<F2^4 as list of 4 images of basis +def ap(L,x): + y=0 + for b in range(4): + if x>>b&1: y^=L[b] + return y +rng=random.Random(20) +klines=(list(range(1,16))*2)[:T] +def rand_map(k): + while True: + L=[rng.choice(sorted(etaE)) for _ in range(4)] + if {ap(L,x) for x in range(16)}==etaE and ap(L,k)==0: return L +while True: + Ls=[rand_map(k) for k in klines[:-1]] + last=[0]*4 + for L in Ls: last=[a^b for a,b in zip(last,L)] + if {ap(last,x) for x in range(16)}==etaE and ap(last,klines[-1])==0: Ls.append(last); break +# psi_j : F2^4 -> R' in kernel-basis coordinates (100-bit ints); psi_1 = 0 +NB=len(kern) +MS=5 # number of maps solved at the end +psi=[[0]*4]+[[rng.getrandbits(NB) for _ in range(4)] for _ in range(T-1-MS)] +Phi=[0]*4 # on basis x=1,2,4,8 +for j in range(1,T-MS): + for b in range(4): Phi[b]^=ap(psi[j],ap(Ls[j],1<>t&1: row|=1<<(4*ii+t) + eqs.append(row) +# gaussian elimination over F2 with RHS symbolic per coordinate: reduce eqs, track combination of b +red=[]; +for b,r in enumerate(eqs): + comb=1<>pp&1: r^=pr; comb^=pc + if r: red.append((r,comb,r.bit_length()-1)) + else: assert False,'dependent equations' +# back-substitute to reduced row echelon +for i in range(len(red)): + r,c,p=red[i] + for j in range(len(red)): + if j!=i and red[j][0]>>p&1: red[j]=(red[j][0]^r,red[j][1]^c,red[j][2]) +pivots={p for _,_,p in red}; freev=[v for v in range(nv) if v not in pivots] +out=[[0]*4 for _ in solved] +for c in range(NB): + tgt=[Phi[b]>>c&1 for b in range(4)] + a=0 + for v in freev: + if rng.getrandbits(1): a|=1<>b&1: rhs^=tgt[b] + val=rhs^(bin(r&a&~(1<>(4*ii+t)&1: out[ii][t]|=1<>b&1: v=[x+y for x,y in zip(v,kern[b])] + Vj.append(v) + V.append(Vj) +sparse=[[{str(i):x for i,x in enumerate(v) if x} for v in Vj] for Vj in V] +json.dump({'seed':20,'kernel_lines':klines,'stage_maps_eta':Ls,'V_columns_sparse':sparse},open(sys.argv[1],'w'),indent=0,sort_keys=True) +open(sys.argv[1],'a').write('\n') +print('built; nonzero V entries',sum(1 for Vj in V for v in Vj for x in v if x)) diff --git a/research/refined-recovery-overlap-floor/verify.py b/research/refined-recovery-overlap-floor/verify.py index 4717abc96f..3f7e95de40 100644 --- a/research/refined-recovery-overlap-floor/verify.py +++ b/research/refined-recovery-overlap-floor/verify.py @@ -137,6 +137,71 @@ def zero_fiber_ratio(maps, rho, d): return total +def check_frames(rows, code, rho): + """Exact zero-fiber value of the committed depth-27 frame sequence. + + W_j = I + V_j E (E = rows 0,1,2,4) with M^T V_j = 0 and E V_j = 0, so + U_j = I + (V_j - V_(j+1))E lies in G and (U_(j-1)...U_1)^-1 = W_j, as in #6660. + Returns sum over the binary dependency space D of prod_j rho(a_j). + """ + eidx = (0, 1, 2, 4) + data = json.loads((HERE / "FRAMES27.json").read_text()) + V = [[[0] * N for _ in range(4)] for _ in data["V_columns_sparse"]] + for j, block in enumerate(data["V_columns_sparse"]): + check(len(block) == 4, "four columns per block") + for t, col in enumerate(block): + for i, x in col.items(): + V[j][t][int(i)] = x + T = len(V) + check(T == 27, "27 frames") + check(all(x == 0 for col in V[0] for x in col), "W_1 = I") + for Vj in V: + for v in Vj: + check(all(v[i] == 0 for i in eidx), "E V_j = 0") + check(all(sum(rows[i][k] * v[i] for i in range(N)) == 0 for k in range(MODES)), "M^T V_j = 0") + # binary images of W_j M e_k + columns = [] + for j in range(T): + for k in range(MODES): + m = [rows[i][k] for i in range(N)] + out = m[:] + for t, i in enumerate(eidx): + if m[i]: + out = [a + m[i] * b for a, b in zip(out, V[j][t])] + columns.append(sum(1 << i for i, x in enumerate(out) if x % 2)) + piv, null = {}, [] + for idx, c in enumerate(columns): + v, comb = c, 1 << idx + while v: + p = v.bit_length() - 1 + if p not in piv: + piv[p] = (v, comb) + break + pv, pc = piv[p] + v ^= pv + comb ^= pc + else: + null.append(comb) + check(len(null) == 8 * T - DIM_CAP, "images span 104 dimensions") + rep = lambda u: min(u ^ c for c in code) + D = {tuple([0] * T)} + for g in null: + cos = tuple(rep(g >> (8 * j) & 255) for j in range(T)) + D |= {tuple(rep(a ^ b) for a, b in zip(d, cos)) for d in D} + check(len(D) == 16, "dependency space of dimension 4") + even = lambda a: wt(a) % 2 == 0 + for d in D: + if any(d): + check(all(even(a) for a in d), "every stage coset of D lies in E") + total = Fraction(0) + for d in D: + p = Fraction(1) + for a in d: + p *= rho[a] + total += p + return total + + def main(): rows = load_rows() code = code_from_rows(rows) @@ -208,6 +273,8 @@ def main(): attained = zero_fiber_ratio(maps, rho, 4) check(attained == 1 + 12 * r2 ** 25 + 3 * r2 ** 26, "abstract configuration value") check(attained > L27 and attained - L27 < Fraction(1, 10 ** 4), "d=4 AM-GM bound nearly attained") + realized = check_frames(rows, code, rho) + check(realized == attained, "committed frames realize the near-optimal pattern exactly") # Table for t = 27..40: best certified d, floor, bits; identity-frame upper bound A_t table = [] From cec5ee4167fe63c6467687cf54e903f6a6f150b4 Mon Sep 17 00:00:00 2001 From: armin Date: Sat, 7 Nov 2026 00:15:26 -0500 Subject: [PATCH 4/5] Determine the exact minimum depth-27 zero fiber Over all frame sequences min |fiber(0)| = (1+12rho2^25+3rho2^26) F^27, attained by FRAMES27.json: exhaustive search over mixtures with up to 7 injective maps plus exact AM-GM exclusions. Co-Authored-By: Claude Opus 5.5 --- .../refined-recovery-overlap-floor/PROOF.md | 43 ++++++++++++- .../refined-recovery-overlap-floor/README.md | 11 +++- .../refined-recovery-overlap-floor/TASK.json | 8 +-- .../VERIFY.json | 6 +- .../refined-recovery-overlap-floor/verify.py | 60 +++++++++++++++++++ 5 files changed, 115 insertions(+), 13 deletions(-) diff --git a/research/refined-recovery-overlap-floor/PROOF.md b/research/refined-recovery-overlap-floor/PROOF.md index 052b895a90..639faece44 100644 --- a/research/refined-recovery-overlap-floor/PROOF.md +++ b/research/refined-recovery-overlap-floor/PROOF.md @@ -141,6 +141,43 @@ Hence, at depth 27, A direct-sum prefix of 26 stages cannot work, because it would force the 27th coordinate map to be injective. These frames avoid such a prefix. +## 3½. The exact minimum zero fiber at depth 27 + +**Theorem.** Over all mode-preserving frame sequences at t = 27, + + min |fiber(0)| = (1 + 12ρ₂^25 + 3ρ₂^26) · F^27 = 15.7897746… · F^27, + +and FRAMES27.json attains it. + +*Proof.* + +1. **Reduction to dimension 4.** By (c), dim D ≥ 4. Every term of (1) is + positive, so any 4-dimensional subspace D′ ⊆ D gives a smaller or equal + sum. It therefore suffices to minimize Σ_{x∈F2^4} Π_j ρ(ℓ_j x) over all + 27-tuples of linear maps ℓ_j : F2^4 → Q. Allowing non-injective joint maps + only enlarges the set minimized over; the minimizer found below is + injective and realized. +2. **Map types.** ρ(ℓx) depends only on whether ℓx is 0, in E∖0, or outside E. + verify.py evaluates all 65,536 maps: the per-map product over the 15 nonzero + x takes 8 values. The smallest is ρ₂^14, for a rank-3 map onto E. The next is + ρ₁⁸ρ₂⁷, for an injective map. All others are at least 1.00056·ρ₂^14. +3. **Few injective maps.** With only maps onto E (kernel a line, value 1 there, + ρ₂ elsewhere) and q ≤ 7 injective maps (value ρ₂ on a hyperplane, ρ₁ off it), + verify.py enumerates every multiset of q hyperplanes exactly. For each it + places the 27 − q kernel lines optimally; the cost is separable and convex, + so greedy placement is optimal. The minimum is at q = 0, with kernels on 12 + lines twice and 3 lines once. The value is 1 + 12ρ₂^25 + 3ρ₂^26. +4. **Everything else.** By AM–GM, Σ_{x≠0} ≥ 15·(Π of per-map products)^(1/15). + This lower bound already exceeds the q = 0 value whenever q ≥ 8, and whenever + any map has neither of the two smallest types. These comparisons are exact + rational checks. +5. **Realization.** The §3 frames realize this pattern exactly. ∎ + +So for zero outputs the depth-27 question is closed: the minimum is +⌈log₂((1 + 12ρ₂^25 + 3ρ₂^26)F^27)⌉ = 696 bits. Whether the maximum fiber of the +optimal frames exceeds their zero fiber is still open; if it does not, this is +the depth-27 optimum. + ## 4. Larger depth RESULT.json lists t = 27,…,40 with the best d ≤ 8. For 28 ≤ t ≤ 40, taking d = 8 @@ -153,9 +190,9 @@ evaluate. Asymptotically, d = 4t − 104 gives roughly 16^(t−26) ρ₂^(7t/8) This is a lower bound for the zero fiber, and hence for the optimal maximum fiber, of PR6660's exact interface: fixed known frames in G, one precision bit, -unbounded integers and full output access. At t = 27 explicit frames pin the -minimum zero fiber to a window of relative width 10⁻⁶. The exact minimum and -the maximum fiber of those frames, and hence the exact optimum, remain open. It supplies no codec, physical tag, caller or restoration +unbounded integers and full output access. At t = 27 the minimum zero fiber is determined exactly and attained by explicit +frames. The maximum fiber of those frames, and hence the exact optimum, remain +open. It supplies no codec, physical tag, caller or restoration cost. κ, the selected frontier and its five assumptions are unchanged. PR6660's theorems (Z) and (c) are cited premises at its pinned head, not replayed; that PR is open at the time of writing. The written proof is diff --git a/research/refined-recovery-overlap-floor/README.md b/research/refined-recovery-overlap-floor/README.md index a386b272cd..5e93a7251a 100644 --- a/research/refined-recovery-overlap-floor/README.md +++ b/research/refined-recovery-overlap-floor/README.md @@ -39,9 +39,14 @@ identity-frame value A_t. mode-preserving frames, W_j = I + V_jE as in #6660. Their dependency space consists of exactly those rank-3 maps onto E, so - 15.78976 F^27 ≤ min over frames of |fiber(0)| ≤ 15.789775 F^27 (t = 27). - -This settles the first step of #6660's question to six significant figures. + min over frames of |fiber(0)| = (1 + 12ρ₂^25 + 3ρ₂^26) F^27 = 15.7897746… F^27 (t = 27). + +**This is exact.** Any dependency space contains a 4-dimensional one with a +smaller sum, so 4-dimensional patterns suffice. Every map type and mixture is +then checked: an exhaustive search covers up to 7 injective maps, and exact +AM–GM comparisons exclude everything else. The rank-3-onto-E pattern of the +frames is the unique best type. This settles the first step of #6660's question +completely. [build_frames.py](build_frames.py) regenerates the frames deterministically. See [PROOF.md](PROOF.md). diff --git a/research/refined-recovery-overlap-floor/TASK.json b/research/refined-recovery-overlap-floor/TASK.json index 56456146d5..aa90995de9 100644 --- a/research/refined-recovery-overlap-floor/TASK.json +++ b/research/refined-recovery-overlap-floor/TASK.json @@ -63,7 +63,7 @@ ] }, "scope_status": "changed", - "actual_scope": "Quantitative lower bound on the optimal worst-case recovery fiber of PR6660 refined chains at every depth t>=27, from its zero-fiber kernel formula: |fiber(0)| >= F^t (1+(2^d-1) mu_d^(t/(2^d-1))) for 1<=d<=4t-104, with mu_d exact; at t=27 this is > 15.7897 F^27, i.e. at least 696 tag bits versus 692 for a direct sum. Explicit 27-frame sequence attains 1+12rho2^25+3rho2^26 (15.789775 F^27), pinning the minimum depth-27 zero fiber.", + "actual_scope": "Quantitative lower bound on the optimal worst-case recovery fiber of PR6660 refined chains at every depth t>=27, from its zero-fiber kernel formula: |fiber(0)| >= F^t (1+(2^d-1) mu_d^(t/(2^d-1))) for 1<=d<=4t-104, with mu_d exact; at t=27 this is > 15.7897 F^27, i.e. at least 696 tag bits versus 692 for a direct sum. Explicit 27-frame sequence attains 1+12rho2^25+3rho2^26 (15.789775 F^27), which is the exact minimum depth-27 zero fiber over all frame sequences.", "scope_change_reason": "Answers the first step of PR6660 open question 1 (minimize the zero-fiber kernel sum at t=27 over overlap patterns) with a bound for every overlap pattern. Like its predecessor this is precision-state accounting in the analytic_recovery interface, not a caller-bound discharge of a selected assumption.", "bottleneck_link": "Side result for exact history accounting in the inherited rounded interface; it changes no supplier invoice.", "budget_minutes": 60, @@ -74,10 +74,10 @@ "ai_assistance": "Anthropic Claude (Claude Code) found the argument, wrote the verifier and ran the checks under apoursh direction. Independent human and formal proof-kernel review are unclaimed.", "open_questions": [ { - "question": "Is the maximum fiber of the FRAMES27.json sequence equal to its zero fiber, and what is the exact minimum zero fiber at t=27?", - "why_it_matters": "Either would turn the six-digit window into the exact depth-27 optimum.", + "question": "Is the maximum fiber of the FRAMES27.json sequence equal to its zero fiber?", + "why_it_matters": "If so, (1+12rho2^25+3rho2^26)F^27 (696 bits) is the exact depth-27 optimum.", "first_step": "Extend the PR6660 stage-by-stage box count to the coupled stages of a 4-dimensional E-valued dependency.", - "blocked_by": "Coupled stage cosets break the per-stage box lemma; the abstract minimum over mixed map types is not computed exactly." + "blocked_by": "Coupled stage cosets break the per-stage box lemma." }, { "question": "Can the identity-frame upper bound A_t be improved at t>=27 by a frame sequence with a single 4-dimensional overlap?", diff --git a/research/refined-recovery-overlap-floor/VERIFY.json b/research/refined-recovery-overlap-floor/VERIFY.json index 0d5364ebd4..f8459469bf 100644 --- a/research/refined-recovery-overlap-floor/VERIFY.json +++ b/research/refined-recovery-overlap-floor/VERIFY.json @@ -16,8 +16,8 @@ "-B", "{package}/verify.py" ], - "timeout_seconds": 60, - "checks": "Fixture hash; C=[8,4,4] self-dual from M; exact coset sums and the even-coset plane E; rho2^7=3; certified t=27 floor 49343/3125; abstract near-attaining pattern; FRAMES27.json integrality, M\u1d40V=0, EV=0, 104-dimensional span, 4-dimensional E-valued dependency and exact zero-fiber value; t=27..40 table against A_t; RESULT.json recomputation; controls." + "timeout_seconds": 300, + "checks": "Fixture hash; C=[8,4,4] self-dual from M; exact coset sums and the even-coset plane E; rho2^7=3; certified t=27 floor 49343/3125; abstract near-attaining pattern; FRAMES27.json integrality, M\u1d40V=0, EV=0, 104-dimensional span, 4-dimensional E-valued dependency and exact zero-fiber value; exact depth-27 minimum over all 65,536 map types (q<=7 injective maps enumerated, AM-GM exclusions); t=27..40 table against A_t; RESULT.json recomputation; controls." }, { "argv": [ @@ -29,7 +29,7 @@ "-B", "{package}/verify.py" ], - "timeout_seconds": 60, + "timeout_seconds": 300, "checks": "The same explicit checks under optimized Python." } ] diff --git a/research/refined-recovery-overlap-floor/verify.py b/research/refined-recovery-overlap-floor/verify.py index 3f7e95de40..b228e7564b 100644 --- a/research/refined-recovery-overlap-floor/verify.py +++ b/research/refined-recovery-overlap-floor/verify.py @@ -3,6 +3,8 @@ Prints PASS_REFINED_RECOVERY_OVERLAP_FLOOR on success. """ import hashlib +import heapq +import itertools import json import math import pathlib @@ -202,6 +204,62 @@ def check_frames(rows, code, rho): return total +def exact_minimum_27(r1, r2): + """Exact minimum of sum_{x in F2^4} prod_j rho(l_j x) over all 27-tuples of + linear maps l_j: F2^4 -> Q whose joint map is injective. + + rho depends only on whether l_j x is 0, in E\\0, or outside E, so E may be + modelled as any hyperplane of F2^4. Returns (minimum, checks passed). + """ + T = 27 + pts = range(1, 16) + par = lambda a, b: wt(a & b) & 1 + E = {x for x in range(16) if par(1, x) == 0} + rho = lambda a: Fraction(1) if a == 0 else (r2 if a in E else r1) + # per-map products over the 15 nonzero points, for all 65536 maps + prods = set() + for L in itertools.product(range(16), repeat=4): + p = Fraction(1) + for x in pts: + y = 0 + for b in range(4): + if x >> b & 1: + y ^= L[b] + p *= rho(y) + prods.add(p) + ps = sorted(prods) + prod_e, prod_i, third = ps[0], ps[1], ps[2] + check(prod_e == r2 ** 14 and prod_i == r1 ** 8 * r2 ** 7, "two smallest per-map products: onto E, injective") + # E-type maps (rank 3 onto E) contribute r2 off their kernel line, 1 on it; + # injective maps contribute r2 on the hyperplane l^-1(E), r1 elsewhere. + hyper = [[x for x in pts if par(h, x) == 0] for h in pts] + best = None + for q in range(8): + p_e = T - q + for H in itertools.combinations_with_replacement(range(15), q): + n = {x: 0 for x in pts} + for h in H: + for x in hyper[h]: + n[x] += 1 + terms = {x: r2 ** (p_e + n[x]) * r1 ** (q - n[x]) for x in pts} + heap = [(terms[x] / r2, x) for x in pts] + heapq.heapify(heap) + for _ in range(p_e): # kernels: separable convex, greedy is optimal + v, x = heapq.heappop(heap) + terms[x] = v + heapq.heappush(heap, (v / r2, x)) + val = 1 + sum(terms.values()) + if best is None or val < best[0]: + best = (val, q) + V = best[0] - 1 + check(best[1] == 0, "minimum uses only maps onto E") + # AM-GM: (sum_{x != 0}/15)^15 >= product of all per-map products + for q in range(8, T + 1): + check((V / 15) ** 15 < prod_e ** (T - q) * prod_i ** q, "AM-GM excludes %d injective maps" % q) + check((V / 15) ** 15 < prod_e ** (T - 1) * third, "AM-GM excludes any other map type") + return best[0] + + def main(): rows = load_rows() code = code_from_rows(rows) @@ -275,6 +333,8 @@ def main(): check(attained > L27 and attained - L27 < Fraction(1, 10 ** 4), "d=4 AM-GM bound nearly attained") realized = check_frames(rows, code, rho) check(realized == attained, "committed frames realize the near-optimal pattern exactly") + exact = exact_minimum_27(r1, r2) + check(exact == attained, "the realized pattern is the exact minimum over all dependency patterns") # Table for t = 27..40: best certified d, floor, bits; identity-frame upper bound A_t table = [] From 6197c4b725ef41dfca790b23c354543294490f60 Mon Sep 17 00:00:00 2001 From: armin Date: Sat, 7 Nov 2026 00:15:43 -0500 Subject: [PATCH 5/5] README: correct verifier runtime Co-Authored-By: Claude Opus 5.5 --- research/refined-recovery-overlap-floor/README.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/research/refined-recovery-overlap-floor/README.md b/research/refined-recovery-overlap-floor/README.md index 5e93a7251a..0c616110c1 100644 --- a/research/refined-recovery-overlap-floor/README.md +++ b/research/refined-recovery-overlap-floor/README.md @@ -60,7 +60,7 @@ python3.12 -I -O -W error -B research/refined-recovery-overlap-floor/verify.py python3.12 -B scripts/research_package.py --package research/refined-recovery-overlap-floor ``` -Each run prints `PASS_REFINED_RECOVERY_OVERLAP_FLOOR` in under a second. It +Each run prints `PASS_REFINED_RECOVERY_OVERLAP_FLOOR` in under a minute. It derives C from the pinned matrix and checks every number stated above in exact rational arithmetic, including all 67 subspaces of F2^8/C for μ_d (d ≤ 8). It also checks the committed frames from their integers alone, recomputes