diff --git a/research/staged-fourth-mixture-ceiling/NOTICE.md b/research/staged-fourth-mixture-ceiling/NOTICE.md new file mode 100644 index 000000000..b1118105a --- /dev/null +++ b/research/staged-fourth-mixture-ceiling/NOTICE.md @@ -0,0 +1,26 @@ +# Sources and credit + +This contribution: Ross Richardson, with substantial OpenAI GPT-6.1 Sol +assistance in derivation, implementation and mathematical specialist review. +Apache-2.0. AI team review is not independent human or formal-kernel review. + +The exact source subset in source4088/ is from Cinna Davis's PR4088, +head 76088d49e3ed4142a958659aa996b0ca4da5e88e. Its word and literal fill are +predecessor contributions, not new constructions here. SOURCE-EXPORT.json +records original paths and byte pins. source4088/NOTICE.md retains the complete +source-specific credit and scope. + +The unchanged binary-basis ledger and rational enclosure engine were retained +through Dugongue/PR3945 and Rohan Arun/PR4076. The primary certificate reuses +that rational engine; the separate independent checker does not import it. +The staged-entry mechanism credits Ross Richardson/PR3605 and dataisfire/PR3734; +ChaloupeMusic and Erwan Secousses/PR3949/3815 supply the general staging and +T360 pattern/Hall lineage. Receiver sharing, native/owner closure and the +predecessor all-character proof credit Dugongue and David Ganz/PR4085, +Nick Petalas, Marius-Paul Dumitrean, Sagar Thakrar, roger-sato, zxv and the +earlier geometry/compiler/transfer contributors named in the source notices. + +The new result is the exact pooled mixture optimum and its complete-cost +ceiling, with a piecewise primal/dual proof and a separately implemented +arithmetic check. No chronological fill, supplier admission, kappa improvement +or selected-frontier update is claimed. diff --git a/research/staged-fourth-mixture-ceiling/PROOF.md b/research/staged-fourth-mixture-ceiling/PROOF.md new file mode 100644 index 000000000..c67a80c87 --- /dev/null +++ b/research/staged-fourth-mixture-ceiling/PROOF.md @@ -0,0 +1,257 @@ +# Pooled whole-helper ceiling for the fixed PR4088 words + +Prepared with OpenAI Codex assistance. Apache-2.0. + +## Scope and source premises + +This result fixes PR4088, Cinna Davis, head +`76088d49e3ed4142a958659aa996b0ca4da5e88e`, and its THREE/FOUR word interfaces. +The source inherits the PR4085 receiver-sharing words and PR4076 staged-entry +lineage. Its native, hosting, restoration, precision, controller and outer +transfer premises remain source premises; this calculation does not discharge +them. Source file digests used here are in `RESULT.json`. + +Let `a` be the exponent saving and `H_r(a)=r^(1-a)`, with `H_0=0`. There are +3240 calls, and `x` of them use FOUR. The local profiles are fixed as + +``` +L3 = 2487 H1 + 713 H2 + 224 H3 + 102 H4 + 20 H5 + 8 H8, +d = L4-L3 = 2 H1 + 3 H3 - 3 H4. +``` + +For THREE the whole-helper widths per call are +`{5:28,6:18,7:56,8:93,9:213}`. FOUR changes helper 601 from width 8 to width 7 +and leaves every other helper width unchanged. Thus the pooled demand is + +``` +(N5,N6,N7,N8,N9) = (90720,58320,181440+x,301320-x,690120). +``` + +The source TEMPLATE has 2016 entries, already including all 112 ports. Its +capacity counts are `{8:672,16:448,32:448,48:448}`. Equivalently there are 18 +distinct child slots per port, with counts `{8:6,16:4,32:4,48:4}`. Multiplying +the TEMPLATE counts by 360, once, gives + +``` +(B8,B16,B32,B48) = (241920,161280,161280,161280), +total bins = 725760, total capacity = 17418240. +``` + +The pooled model ignores source windows, chronology, call identity, repeated +physical-family exclusions and any other restrictions on where a helper may +be hosted. It allows real nonnegative pattern multiplicities and real +`0<=x<=3240`. Each pattern still contains whole helpers. This is an explicitly +optimistic relaxation of a legal source owner fill. The result gives a lower +bound on the paid bill of every such fill, including any nonuniform dispatch +of these fixed words. It does not construct a changed supplier. + +## Complete finite pattern program + +A pattern is `(c,n5,n6,n7,n8,n9)` with +`n_w>=0` integral and `sum_w w*n_w<=c`. Its residual rank is +`r=c-sum_w w*n_w`. There are exactly 841 patterns: 5 at capacity8,21 at 16, +158 at 32 and 657 at 48. Empty patterns are included. + +For pattern multiplicities `y>=0`, require exactly `B_c` bins of each capacity +and exactly the demands above. The paid objective is the complete expression + +``` +3240 L3 + x d + sum_patterns y_pattern H_residual. +``` + +Every admissible source allocation maps to such a feasible point. No idle bin +is discarded. The helper rank mass is `10695240-x`, the local rank mass is +`16708680-x`, and the residual rank mass is `6723000+x`. Consequently the full +paid rank mass is always 23431680, or `65088*360`. This is distinct from the +comparison stock mass `(896*360)*73=23546880`. + +## Exact optimum and dual certificate + +For every `a` in `[0.00173,0.00174]`, the unique optimal mixture is `x=1080`. +An integral optimum of the pooled program is: + +| Capacity | Whole helpers in each bin | Multiplicity | Residual | +| --- | --- | ---: | ---: | +| 8 | 8 | 241920 | 0 | +| 16 | 7+9 | 161280 | 0 | +| 32 | 9+9+9 | 1620 | 5 | +| 32 | 7+7+9+9 | 10620 | 0 | +| 32 | 6+8+9+9 | 58320 | 0 | +| 32 | 5+9+9+9 | 90720 | 0 | +| 48 | empty | 138492 | 48 | +| 48 | 9+9+9+9+9 | 22788 | 3 | + +Thus the optimal residual profile is + +``` +I* = 22788 H3 + 1620 H5 + 138492 H48. +``` + +Here is a dual certificate, written as exact rational linear combinations of +the functions `H_r`, rather than rounded decimal prices. Set + +``` +v9 = (H3-H48)/5, +v7 = (v9-H5)/2, +v8 = v7+d, +v6 = 2v7-v8, +v5 = -H5, +u8 = -v8, +u16 = -v7-v9, +u32 = H5-3v9, +u48 = H48. +``` + +For every pattern the checker proves + +``` +u_c + sum_w n_w v_w <= H_residual. +``` + +The eight displayed patterns give exact symbolic equality. All other 833 +constraints have strictly positive slack throughout the stated interval; +the certified minimum of slack divided by `a` is greater than +`0.696988114241`. The mixture coefficient is identically +`d+v7-v8=0`. Weak duality therefore gives the same lower bound for every real +`x` and every feasible pattern allocation. Equality is attained by the table. + +Because every other pattern has positive slack, an optimum uses only the +eight displayed patterns. The nine bin/item equations, including variable +`x`, have determinant `-10`. Their solution is the displayed table and +`x=1080`, proving uniqueness in the pooled program. One can also see the +mixture directly: width 5 fixes 90720 bins of pattern `5+9+9+9`; width 6 fixes +58320 bins of `6+8+9+9`. Width 8 balance then forces +`241920+58320=301320-x`, hence `x=1080`. + +## A genuine mixture breakpoint + +The fixed-mixture optimum can also be stated for every real `x` in the full +range. Let `t=x-1080`, and begin with the table above. Keep the capacity8, +capacity16 and `5+9+9+9` rows fixed. + +For `-1080<=t<=0`, replace the affected multiplicities by + +``` +cap32, 9+9+9: 1620-t/4, +cap32, 7+8+8+9: -t/2, +cap32, 7+7+9+9: 10620+3t/4, +cap32, 6+8+9+9: 58320, +cap48, empty: 138492+t/20, +cap48, five9: 22788-t/20. +``` + +For `0<=t<=2160`, use + +``` +cap32, 9+9+9: 1620+t/2, +cap32, 7+7+9+9: 10620+t/2, +cap32, 6+8+9+9: 58320-t, +cap48, empty: 138492, +cap48, five9: 22788-t/2, +cap48, 6+6+9+9+9+9: t/2. +``` + +All multiplicities are nonnegative on their segments, and all constraints +hold as exact affine identities. These are witnesses in the relaxation. +They do not assert chronological or physical-family feasibility. + +For the left segment replace `v8` by `(v7+v9)/2`; for the right segment set +`v6=(-H48-4v9)/2` and `v8=2v7-v6`. Keep the other dual formulas. The checker +certifies all 841 inequalities for each dual over the same exponent interval, +and each corresponding affine witness is complementary to its dual. +Consequently the optimum complete bill has slopes + +``` +s_left = d-H3/20-H5/4+H48/20, +s_right = d+(H5-H3)/2. +``` + +Throughout the exponent interval, exact bounds give +`s_left/a` in `[-0.348857711147,-0.348494057120]` and `s_right/a` in +`[4.365719222915,4.365911868442]`, using outward rounded displayed bounds. +Thus the bill strictly decreases to 1080 fourth calls and strictly increases +after 1080. Increasing the fourth-call frequency beyond PR4088's one-third +mixture cannot improve even this optimistic pooled bill. + +## Exact root ceiling and remaining headroom + +The complete optimum profile is + +``` +8060040 H1 + 2310120 H2 + 751788 H3 + 327240 H4 + + 66420 H5 + 25920 H8 + 138492 H48. +``` + +Compare this with the same source stock `(896*360) H73`. Rational logarithm +and exponential remainder bounds, imported unchanged from the source engine, +give a strict root bracket + +``` +0.001730980255989036959962 < a* < 0.001730980255989036959963. +``` + +The lower and upper signed moment intervals have signs negative and positive, +respectively; the exact endpoints are in `RESULT.json`. Approximate values are +`-1.73328*10^-17` and `+4.89396*10^-17`. Every positive rank in any feasible +complete profile is less than 73. After division by `73^(1-a)`, its complete +moment is strictly increasing in `a`. Therefore positivity of the pooled lower +bound at the upper endpoint excludes any feasible fixed-word owner allocation +having a larger moment root, including exponents outside the interval where +the displayed dual was certified. The pooled table attains `a*`, so this is a +sharp ceiling for the relaxation. + +PR4088's literal chronological fill already has 1080 FOUR calls. Its residual +profile is `22785 H3+1625 H5+H16+2H32+138490 H48`. Literal minus pooled optimum +is exactly + +``` +D(p) = -3*3^p + 5*5^p + 16^p + 2*32^p - 2*48^p, p=1-a. +``` + +This difference is strictly positive for every `0= 0`, + +by `exp(t)>=1+t` for `t>=0`. Using the lower endpoint for positive-coefficient +lower bounds and the upper endpoint for negative-coefficient lower bounds gives +an outward interval for the whole range. This argument requires the exact zero +rank-mass test; the checker rejects a form that fails it. + +The exact optimal idle profiles for real x in the pooled relaxation are + +``` +0<=x<=1080: + (22842-x/20) H3 + (1890-x/4) H5 + (138438+x/20) H48 +1080<=x<=3240: + (23328-x/2) H3 + (1080+x/2) H5 + 138492 H48. +``` + +The review encodes every proposed multiplicity as exact rational affine +coefficients. It verifies bin and item balance coefficient by coefficient, each +integer pattern's capacity, nonnegative multiplicities at both interval +endpoints, and symbolic complementary slackness with the corresponding dual. +Affineness proves nonnegativity on every real x between endpoints. The complete +left derivative divided by k lies in +`[-0.348857712,-0.348494057]`, while the complete right derivative divided by k +lies in `[4.365719222,4.365911869]`. These signs include the changed local paid +profile and prove the unique optimum x=1080 throughout this broad k interval. + +The broad review rejects a nonzero-mass factorization, an increased capacity-8 +dual that preserves zero rank mass, a missing capacity-48 bin, an extra affine +pattern, and a negative endpoint multiplicity. The result is in +the report emitted by `independent/review_broad.py`. It remains a relaxation with real pattern multiplicities. + +## Root certificate and comparison + +The independent enclosure computes `log r` by range reduction and 108 positive +atanh terms with an explicit geometric tail. It then computes +`H_r=r*exp(-k log r)` on the exact integer lattice of spacing `10^-90`, using +outward term recurrences and even/odd alternating Taylor bounds through degrees +64 and 65. Signed coefficients reverse interval endpoints. The source pricing +engine is not imported or called. + +For the ideal profile, complete moment minus `W*H73` is strictly negative at +the lower endpoint (approximately `-1.7332795175363e-17`) and strictly positive +at the upper endpoint (approximately `4.8939596059017e-17`). Every positive rank +is below 73. Therefore its normalized moment is strictly increasing in k, giving +the displayed root bracket. At the upper endpoint, duality puts **every** legal +frozen-interface mixture strictly above stock; monotonicity bounds every such +mixture's root by that endpoint. The pooled primal makes the bracket sharp for +the relaxed model. + +The PR4088 literal profile has the independently checked root bracket + +`[0.001730978305075885693430,0.001730978305075885693431]`. + +Subtracting brackets puts the pooled ceiling's root headroom over the literal +root in + +`[0.000000001950913151266531,0.000000001950913151266533]`. + +The literal-minus-ideal idle profile is +`-3H3+5H5+H16+2H32-2H48`. Its truncated-rank sums at the knots 3,5,16,32,48 +are 9,21,32,32,0. Between knots these are affine and nonnegative, strictly +positive on a set of positive measure. Since for `0= 1, 'log argument') + if r == 1: + return (0, 0) + + def log_unit(y): + need(1 <= y <= 2, 'range reduction') + t = (y - 1) / (y + 1) + term = t + partial = Q(0) + count = 108 + for j in range(count): + partial += term / (2 * j + 1) + term *= t * t + lower = 2 * partial + upper = lower + 2 * term / ((2 * count + 1) * (1 - t * t)) + return lower, upper + + exponent = r.bit_length() - 1 + yl, yh = log_unit(Q(r, 1 << exponent)) + tl, th = log_unit(Q(2)) + lower, upper = yl + exponent * tl, yh + exponent * th + return ((lower * SCALE).numerator // (lower * SCALE).denominator, + -(-(upper * SCALE).numerator // (upper * SCALE).denominator)) + + +def ceil_div(n, d): + return -(-n // d) + + +def exp_neg_enclosure(zlo, zhi): + """Exact fixed-point interval Taylor arithmetic for exp(-z), 0<=z<=1. + + Each positive term is propagated outwards. Partial sum through degree 64 + is an upper bound, and subtracting the interval upper degree-65 term gives + a lower bound by the alternating-series theorem. + """ + need(0 <= zlo <= zhi <= SCALE, 'exponential range') + tlo = thi = SCALE + slo = shi = SCALE + for j in range(1, 65): + tlo = tlo * zlo // (SCALE * j) + thi = ceil_div(thi * zhi, SCALE * j) + if j % 2: + slo -= thi + shi -= tlo + else: + slo += tlo + shi += thi + next_hi = ceil_div(thi * zhi, SCALE * 65) + return slo - next_hi, shi + + +def power_enclosure(r, k): + """Enclose r^(1-k) on the SCALE lattice. No floating-point functions.""" + need(0 <= k <= Q(1, 100), 'checked k domain is [0,0.01]') + if r == 0: + return (0, 0) + if r == 1 or k == 0: + return (r * SCALE, r * SCALE) + ll, lh = log_enclosure(r) + zlo = ll * k.numerator // k.denominator + zhi = ceil_div(lh * k.numerator, k.denominator) + lo, hi = exp_neg_enclosure(zlo, zhi) + return r * lo, r * hi + + +def vec(*terms): + out = Counter() + for coefficient, source in terms: + for rank_, value in source.items(): + out[rank_] += Q(coefficient) * value + return {r: v for r, v in out.items() if v} + + +def h(r): + return {r: Q(1)} if r else {} + + +def dual_vectors(): + """Nominated owner dual, reconstructed as exact sparse linear forms in H_r.""" + d = dict(LOCAL_DELTA) + v9 = vec((Q(1, 5), h(3)), (-Q(1, 5), h(48))) + v7 = vec((Q(1, 2), v9), (-Q(1, 2), h(5))) + v8 = vec((1, v7), (1, d)) + v6 = vec((1, v7), (-1, d)) + v5 = vec((-1, h(5))) + u8 = vec((-1, v8)) + u16 = vec((-1, v7), (-1, v9)) + u32 = vec((1, h(5)), (-3, v9)) + return {8: u8, 16: u16, 32: u32, 48: h(48)}, {5: v5, 6: v6, 7: v7, 8: v8, 9: v9} + + +def patterns(capacity): + """Exhaust all five nonnegative integer counts, including the empty pattern.""" + def walk(index, room, counts): + if index == len(WIDTHS): + yield tuple(counts), room + return + w = WIDTHS[index] + for count in range(room // w + 1): + yield from walk(index + 1, room - count * w, counts + [count]) + yield from walk(0, capacity, []) + + +def eval_vec(form, power): + lower = upper = Q(0) + for r, coefficient in form.items(): + lo, hi = power[r] + if coefficient > 0: + lower += coefficient * lo + upper += coefficient * hi + else: + lower += coefficient * hi + upper += coefficient * lo + return lower / SCALE, upper / SCALE + + +def check_dual(bins, demands, local, k, *, tamper=None): + power = {r: power_enclosure(r, k) for r in range(74)} + u, v = dual_vectors() + if tamper == 'wrong_bin_sign': + u[8] = vec((-1, u[8])) + if tamper == 'raise_u48': + u[48] = vec((1, u[48]), (Q(1, 10**12), h(1))) + need(vec((1, LOCAL_DELTA), (1, v[7]), (-1, v[8])) == {}, 'global x cancellation') + total_patterns = 0 + exact_ties = 0 + pattern_counts = {} + minimum = None + minimum_pattern = None + ties = {} + for capacity in CAPACITIES: + patterns_here = list(patterns(capacity)) + pattern_counts[capacity] = len(patterns_here) + ties[capacity] = [] + for counts, remainder in patterns_here: + slack = vec((1, h(remainder)), (-1, u[capacity]), + *((-n, v[w]) for w, n in zip(WIDTHS, counts))) + total_patterns += 1 + if not slack: + exact_ties += 1 + ties[capacity].append(list(counts)) + else: + lo, hi = eval_vec(slack, power) + need(lo > 0, f'dual pattern not strictly feasible: c={capacity}, n={counts}, slack=[{lo},{hi}]') + if minimum is None or lo < minimum: + minimum = lo + minimum_pattern = [capacity, list(counts), remainder] + need(total_patterns == 841, 'incomplete integer-pattern coverage') + bound_form = vec((1, local), *((n, u[c]) for c, n in bins.items()), + *((n, v[w]) for w, n in demands.items())) + ideal = dict(local) + for r, n in LOCAL_DELTA.items(): + ideal[r] = ideal.get(r, 0) + 1080 * n + for r, n in {3: 22788, 5: 1620, 48: 138492}.items(): + ideal[r] = ideal.get(r, 0) + n + need(all(0 < r < 73 and n > 0 for r, n in ideal.items()), 'strict normalized-moment monotonicity premises') + need(bound_form == {r: Q(n) for r, n in ideal.items()}, 'dual does not equal nominated ideal histogram') + bound_minus_stock = vec((1, bound_form), (-STOCK, h(73))) + lo, hi = eval_vec(bound_minus_stock, power) + return {'target_k': str(k), 'pattern_counts': pattern_counts, 'total_patterns': total_patterns, + 'exact_ties': exact_ties, 'active_count_vectors_widths5to9': ties, + 'minimum_nonidentity_slack_lower': str(minimum), 'minimum_pattern': minimum_pattern, + 'ideal_profile': ideal, 'lower_bound_minus_stock_interval': [str(lo), str(hi)], + 'lower_bound_minus_stock_decimal': [decimal_str(lo), decimal_str(hi)], + 'strict_all_x_rejection': lo > 0} + + +def decimal_str(x, digits=30): + negative = x < 0 + x = abs(Q(x)) + scale = 10**digits + q = x.numerator * scale // x.denominator + whole, part = divmod(q, scale) + return ('-' if negative else '') + str(whole) + '.' + str(part).zfill(digits) + + +def check_majorization(): + difference = {3: -3, 5: 5, 16: 1, 32: 2, 48: -2} + sums = {t: sum(n * min(r, t) for r, n in difference.items()) for t in sorted(difference)} + need(sums == {3: 9, 5: 21, 16: 32, 32: 32, 48: 0}, 'literal versus ideal truncated masses') + need(sum(r * n for r, n in difference.items()) == 0, 'comparison rank masses differ') + return {'literal_minus_ideal': difference, 'truncated_rank_sums': sums, + 'conclusion': 'literal moment strictly exceeds ideal moment for every 0 < k < 1'} + + +def check_primal(bins, demands): + """An exact integral pooled witness, with chronology/family conditions erased.""" + rows = [ + (8, (0, 0, 0, 1, 0), 241920), + (16, (0, 0, 1, 0, 1), 161280), + (32, (0, 0, 0, 0, 3), 1620), + (32, (0, 0, 2, 0, 2), 10620), + (32, (0, 1, 0, 1, 2), 58320), + (32, (1, 0, 0, 0, 3), 90720), + (48, (0, 0, 0, 0, 0), 138492), + (48, (0, 0, 0, 0, 5), 22788), + ] + observed_bins = Counter() + observed_demands = Counter() + idle = Counter() + u, v = dual_vectors() + for capacity, counts, multiplicity in rows: + need(type(multiplicity) is int and multiplicity >= 0, 'primal multiplicity') + remainder = capacity - sum(w * n for w, n in zip(WIDTHS, counts)) + need(remainder >= 0, 'primal capacity') + need(vec((1, h(remainder)), (-1, u[capacity]), + *((-n, v[w]) for w, n in zip(WIDTHS, counts))) == {}, 'primal pattern not symbolically tight') + observed_bins[capacity] += multiplicity + for w, n in zip(WIDTHS, counts): + observed_demands[w] += multiplicity * n + if remainder: + idle[remainder] += multiplicity + need(dict(observed_bins) == bins, 'primal bin counts') + expected_demands = dict(demands) + expected_demands[7] += 1080 + expected_demands[8] -= 1080 + need(dict(observed_demands) == expected_demands, 'primal item counts') + need(dict(idle) == {3: 22788, 5: 1620, 48: 138492}, 'primal idle invoice') + # With all nonidentity pattern slacks strict, every optimizer uses precisely + # the eight active patterns. The cap8 patterns consume B8 width8s; width6 + # demand forces the only other width8 pattern count. Thus x is unique. + forced_x = demands[8] - bins[8] - demands[6] + need(forced_x == 1080, 'stationary mixture not forced by tight patterns') + return {'x': 1080, 'rows': [[c, list(n), z] for c, n, z in rows], 'idle': dict(idle), + 'forced_x_identity': 'x = N8(0) - B8 - N6 = 1080', + 'scope': 'Integral pooled patterns only; chronology, family constraints and helper identities erased.'} + + +def check_literal_root(source, local): + record = read(source / 'RESULT.json') + literal = {int(r): n for r, n in record['profile'].items()} + expected = dict(local) + for r, n in LOCAL_DELTA.items(): + expected[r] = expected.get(r, 0) + 1080 * n + for r, n in {3: 22785, 5: 1625, 16: 1, 32: 2, 48: 138490}.items(): + expected[r] = expected.get(r, 0) + n + need(literal == expected, 'literal source result invoice') + difference = vec((1, literal), (-STOCK, h(73))) + lower, upper = Q(record['root_lower']), Q(record['root_upper']) + lower_sign = eval_vec(difference, {r: power_enclosure(r, lower) for r in difference}) + upper_sign = eval_vec(difference, {r: power_enclosure(r, upper) for r in difference}) + need(lower_sign[1] < 0 and upper_sign[0] > 0, 'literal source root bracket not independently certified') + ideal_lower = Q('0.001730980255989036959962') + ideal_upper = Q('0.001730980255989036959963') + return {'literal_root': [str(lower), str(upper)], + 'independent_literal_endpoint_sign_intervals': [[str(x) for x in z] for z in (lower_sign, upper_sign)], + 'pooled_ceiling_minus_literal_root': [str(ideal_lower - upper), str(ideal_upper - lower)], + 'pooled_ceiling_minus_literal_root_decimal': [decimal_str(ideal_lower - upper), decimal_str(ideal_upper - lower)], + 'limits': 'A bound on the retained complete-moment root; no all-size construction or outer transfer established.'} + + +def check_dual_over_root_bracket(): + lower = Q('0.001730980255989036959962') + upper = Q('0.001730980255989036959963') + # H_r(k)=r*exp(-k log r) decreases in k, with r=0,1 constant. + power = {r: (power_enclosure(r, upper)[0], power_enclosure(r, lower)[1]) for r in range(49)} + u, v = dual_vectors() + ties = strict = 0 + minimum = None + for capacity in CAPACITIES: + for counts, remainder in patterns(capacity): + slack = vec((1, h(remainder)), (-1, u[capacity]), + *((-n, v[w]) for w, n in zip(WIDTHS, counts))) + if not slack: + ties += 1 + else: + lo, _ = eval_vec(slack, power) + need(lo > 0, 'uniform bracket dual feasibility') + strict += 1 + minimum = lo if minimum is None else min(minimum, lo) + need((ties, strict) == (8, 833), 'uniform bracket pattern count') + return {'k_interval': [str(lower), str(upper)], 'identities': ties, 'strict_patterns': strict, + 'minimum_nonidentity_slack_lower': str(minimum), + 'conclusion': 'The pooled optimum profile and unique mix x=1080 hold throughout this entire root bracket.'} + + +def controls(bins, demands, local, k): + rejected = [] + for name in ('wrong_bin_sign', 'raise_u48'): + try: + check_dual(bins, demands, local, k, tamper=name) + except ValueError: + rejected.append(name) + else: + raise ValueError('control not rejected: ' + name) + bad = dict(bins) + bad[48] -= 1 + try: + check_dual(bad, demands, local, k) + except ValueError: + rejected.append('missing_capacity48_bin') + else: + raise ValueError('missing bin control not rejected') + need(power_enclosure(0, Q(0)) == (0, 0), 'zero power') + need(all(power_enclosure(r, Q(0)) == (r * SCALE, r * SCALE) for r in range(74)), 'k=0 exact powers') + # A nonzero logarithm/exponential control with an exactly known result: + # (2^100)^(1-1/100)=2^99. This exercises the full nontrivial enclosure path. + lo, hi = power_enclosure(2**100, Q(1, 100)) + need(lo <= (2**99) * SCALE <= hi, 'nontrivial perfect-power enclosure') + return rejected + ['exact_integer_powers_at_k0', 'nontrivial_perfect_power', + 'symbolic_x_cancellation', 'all_empty_patterns_included'] + + +def main(): + parser = argparse.ArgumentParser() + parser.add_argument('--source', type=Path, default=Path(__file__).resolve().parent.parent / 'source4088') + parser.add_argument('--target-k', type=Q) + parser.add_argument('--output', type=Path) + parser.add_argument('--controls', action='store_true') + args = parser.parse_args() + bins, demands, local, accounts = source_accounting(args.source) + bracket_lower = check_dual(bins, demands, local, Q('0.001730980255989036959962')) + bracket_upper = check_dual(bins, demands, local, Q('0.001730980255989036959963')) + need(Q(bracket_lower['lower_bound_minus_stock_interval'][1]) < 0 < Q(bracket_upper['lower_bound_minus_stock_interval'][0]), 'strict independent pooled root bracket') + result = {'status': 'PASS_INDEPENDENT_POOLED_CEILING', 'source': str(args.source), + 'accounting': accounts, 'majorization': check_majorization(), + 'pooled_primal': check_primal(bins, demands), + 'comparison': check_literal_root(args.source, local), + 'uniform_root_bracket': check_dual_over_root_bracket(), + 'bracket_checks': {'lower': bracket_lower, 'upper': bracket_upper}} + if args.target_k is not None: + result['dual'] = check_dual(bins, demands, local, args.target_k) + if args.controls: + result['controls'] = controls(bins, demands, local, args.target_k or Q('0.001730980255989036959963')) + if args.output: + args.output.write_text(json.dumps(result, sort_keys=True, indent=2) + '\n') + print(json.dumps({'status': result['status'], 'pooled_optimal_mix': 1080, + 'root_bracket': ['0.001730980255989036959962', '0.001730980255989036959963'], + 'patterns': 841, + **({'dual': {k: v for k, v in result['dual'].items() if k not in ('active_count_vectors_widths5to9',)}} if 'dual' in result else {})}, sort_keys=True)) + + +if __name__ == '__main__': + main() diff --git a/research/staged-fourth-mixture-ceiling/independent/review_broad.py b/research/staged-fourth-mixture-ceiling/independent/review_broad.py new file mode 100644 index 000000000..46a4b9a5d --- /dev/null +++ b/research/staged-fourth-mixture-ceiling/independent/review_broad.py @@ -0,0 +1,196 @@ +"""Independent review of the three broad-interval owner duals and affine fills. + +Imports only this directory's independent enclosure implementation; no solver, +source pricing implementation or owner checker is executed/imported. +""" +from fractions import Fraction as Q +import argparse +import importlib.util +import json +from pathlib import Path + +_spec = importlib.util.spec_from_file_location('independent_pooled_check', Path(__file__).resolve().with_name('check.py')) +C = importlib.util.module_from_spec(_spec) +_spec.loader.exec_module(C) + +LO, HI = Q('.00173'), Q('.00174') + + +def potentials(piece): + u, v = C.dual_vectors() + if piece == 'left': + v[8] = C.vec((Q(1, 2), v[7]), (Q(1, 2), v[9])) + v[6] = C.vec((2, v[7]), (-1, v[8])) + elif piece == 'right': + v[6] = C.vec((-Q(1, 2), C.h(48)), (-2, v[9])) + v[8] = C.vec((2, v[7]), (-1, v[6])) + else: + C.need(piece == 'middle', 'dual piece') + u[8] = C.vec((-1, v[8])) + return u, v + + +def divided_difference_bounds(): + # For t=log(r)>=0, g(a)=r(exp(-at)-1)/a has derivative + # r[1-(1+at)exp(-at)]/a^2>=0, by exp(at)>=1+at. + # Thus its entire interval is enclosed by its two endpoint values. + result = {} + for r in range(1, 49): + pl = C.power_enclosure(r, LO) + ph = C.power_enclosure(r, HI) + result[r] = ((Q(pl[0], C.SCALE) - r) / LO, + (Q(ph[1], C.SCALE) - r) / HI) + return result + + +def normalized_enclosure(form, divided): + C.need(sum(r * n for r, n in form.items()) == 0, 'factoring nonzero rank mass') + lo = hi = Q(0) + for r, n in form.items(): + a, b = divided[r] + lo += n * (a if n > 0 else b) + hi += n * (b if n > 0 else a) + return lo, hi + + +def verify_dual(piece, divided, *, perturb=False): + u, v = potentials(piece) + if perturb: + # Preserve zero rank mass while making the formerly tight cap8 pattern + # infeasible: 2H1-H2>0 throughout the checked positive-k interval. + u[8] = C.vec((1, u[8]), (2, C.h(1)), (-1, C.h(2))) + identities = 0 + strict = 0 + minimum = None + for capacity in C.CAPACITIES: + for counts, remainder in C.patterns(capacity): + slack = C.vec((1, C.h(remainder)), (-1, u[capacity]), + *((-n, v[w]) for w, n in zip(C.WIDTHS, counts))) + if not slack: + identities += 1 + else: + interval = normalized_enclosure(slack, divided) + C.need(interval[0] > 0, 'broad interval pattern slack') + strict += 1 + if minimum is None or interval[0] < minimum: + minimum = interval[0] + C.need(identities + strict == 841, 'complete broad pattern coverage') + slope = C.vec((1, C.LOCAL_DELTA), (1, v[7]), (-1, v[8])) + slo, shi = normalized_enclosure(slope, divided) + if piece == 'left': + C.need(shi < 0, 'left slope not strictly negative') + elif piece == 'right': + C.need(slo > 0, 'right slope not strictly positive') + else: + C.need(not slope and slo == shi == 0, 'middle slope not identically zero') + return {'identities': identities, 'strict_patterns': strict, + 'minimum_normalized_slack_lower': str(minimum), + 'slope_over_k_interval': [str(slo), str(shi)], + 'slope_over_k_decimal': [C.decimal_str(slo), C.decimal_str(shi)]} + + +def affine_rows(piece): + """Each row is capacity, integer width counts, constant y0, x coefficient y1.""" + common = [ + (8, (0, 0, 0, 1, 0), Q(241920), Q(0)), + (16, (0, 0, 1, 0, 1), Q(161280), Q(0)), + (32, (1, 0, 0, 0, 3), Q(90720), Q(0)), + ] + if piece == 'left': + return common + [ + (32, (0, 0, 0, 0, 3), Q(1890), -Q(1, 4)), + (32, (0, 0, 1, 2, 1), Q(540), -Q(1, 2)), + (32, (0, 0, 2, 0, 2), Q(9810), Q(3, 4)), + (32, (0, 1, 0, 1, 2), Q(58320), Q(0)), + (48, (0, 0, 0, 0, 0), Q(138438), Q(1, 20)), + (48, (0, 0, 0, 0, 5), Q(22842), -Q(1, 20)), + ] + C.need(piece == 'right', 'affine fill piece') + return common + [ + (32, (0, 0, 0, 0, 3), Q(1080), Q(1, 2)), + (32, (0, 0, 2, 0, 2), Q(10080), Q(1, 2)), + (32, (0, 1, 0, 1, 2), Q(59400), -Q(1)), + (48, (0, 0, 0, 0, 0), Q(138492), Q(0)), + (48, (0, 0, 0, 0, 5), Q(23328), -Q(1, 2)), + (48, (0, 2, 0, 0, 4), -Q(540), Q(1, 2)), + ] + + +def verify_affine(piece, bins, demands, *, rows=None): + u, v = potentials(piece) + region = (Q(0), Q(1080)) if piece == 'left' else (Q(1080), Q(3240)) + bin_forms = {c: [Q(0), Q(0)] for c in C.CAPACITIES} + item_forms = {w: [Q(0), Q(0)] for w in C.WIDTHS} + idle_forms = {} + for capacity, counts, y0, y1 in (affine_rows(piece) if rows is None else rows): + C.need(all(type(n) is int and n >= 0 for n in counts), 'whole integer widths') + remainder = capacity - sum(w * n for w, n in zip(C.WIDTHS, counts)) + C.need(remainder >= 0, 'affine pattern capacity') + C.need(all(y0 + y1 * x >= 0 for x in region), 'nonnegative affine endpoints') + # Affineness implies endpoint nonnegativity on every real x in the segment. + slack = C.vec((1, C.h(remainder)), (-1, u[capacity]), + *((-n, v[w]) for w, n in zip(C.WIDTHS, counts))) + C.need(not slack, 'affine complementary slackness identity') + bin_forms[capacity][0] += y0 + bin_forms[capacity][1] += y1 + for w, n in zip(C.WIDTHS, counts): + item_forms[w][0] += n * y0 + item_forms[w][1] += n * y1 + if remainder: + idle_forms.setdefault(remainder, [Q(0), Q(0)]) + idle_forms[remainder][0] += y0 + idle_forms[remainder][1] += y1 + C.need(bin_forms == {c: [Q(n), Q(0)] for c, n in bins.items()}, 'affine bin polynomial coefficients') + C.need(item_forms == {w: [Q(n), Q(int(w == 7) - int(w == 8))] for w, n in demands.items()}, 'affine item polynomial coefficients') + return {'x_interval': [str(x) for x in region], + 'all_coefficients_exact': True, 'all_multiplicities_nonnegative': True, + 'idle_coefficients_y0_plus_x_y1': {r: [str(x) for x in form] for r, form in idle_forms.items()}, + 'scope': 'Real multiplicities; integral helper patterns; no chronology or family allocation.'} + + +def controls(bins, demands, divided): + out = [] + + def rejects(name, callback): + try: + callback() + except ValueError: + out.append(name) + else: + raise ValueError('broad control was accepted: ' + name) + + rejects('factoring_nonzero_rank_mass', lambda: normalized_enclosure(C.h(1), divided)) + rejects('raised_zero_mass_capacity8_dual', lambda: verify_dual('middle', divided, perturb=True)) + bad_bins = dict(bins) + bad_bins[48] -= 1 + rejects('one_missing_capacity48_bin', lambda: verify_affine('right', bad_bins, demands)) + bad_rows = affine_rows('left') + c, nn, y0, y1 = bad_rows[3] + bad_rows[3] = (c, nn, y0 + 1, y1) + rejects('one_extra_affine_pattern', lambda: verify_affine('left', bins, demands, rows=bad_rows)) + bad_rows = affine_rows('right') + c, nn, y0, y1 = bad_rows[-1] + bad_rows[-1] = (c, nn, y0 - 1, y1) + rejects('negative_endpoint_multiplicity', lambda: verify_affine('right', bins, demands, rows=bad_rows)) + return out + + +def main(): + parser = argparse.ArgumentParser() + parser.add_argument('--source', type=Path, required=True) + parser.add_argument('--output', type=Path) + args = parser.parse_args() + bins, demands, _, _ = C.source_accounting(args.source) + divided = divided_difference_bounds() + result = {'status': 'PASS_INDEPENDENT_BROAD_DUAL_AND_AFFINE_REVIEW', + 'k_interval': [str(LO), str(HI)], + 'duals': {piece: verify_dual(piece, divided) for piece in ('left', 'middle', 'right')}, + 'affine_primal': {piece: verify_affine(piece, bins, demands) for piece in ('left', 'right')}, + 'controls': controls(bins, demands, divided)} + if args.output: + args.output.write_text(json.dumps(result, sort_keys=True, indent=2) + '\n') + print(json.dumps(result, sort_keys=True)) + + +if __name__ == '__main__': + main() diff --git a/research/staged-fourth-mixture-ceiling/source4088/INPUTS.json b/research/staged-fourth-mixture-ceiling/source4088/INPUTS.json new file mode 100644 index 000000000..5898f7e11 --- /dev/null +++ b/research/staged-fourth-mixture-ceiling/source4088/INPUTS.json @@ -0,0 +1,8 @@ +{ + "canonical_sha256": { + "THREE-base.json.gz": "960867f94fe43489c5108eaff4cc159714a338a8a056837e5c497ded3d72c283", + "FOUR-base.json.gz": "cc8e27b329defb34e5fe89bc18f886a4c9ff0f99a08bd4f686f4298b0eb39e04", + "THREE-extra.json.gz": "ef1ca8b7d40346fc2b3261b93dab740322064e47ea194b7d989bac3650e37255", + "FOUR-extra.json.gz": "c517eed7547e48ddc9f1f561e2fcc436b5999dab4aeb0cc634806c910d5444fc" + } +} diff --git a/research/staged-fourth-mixture-ceiling/source4088/NOTICE.md b/research/staged-fourth-mixture-ceiling/source4088/NOTICE.md new file mode 100644 index 000000000..b844df5ef --- /dev/null +++ b/research/staged-fourth-mixture-ceiling/source4088/NOTICE.md @@ -0,0 +1,39 @@ +# Attribution and source boundaries + +New work: Cinna Davis with substantial OpenAI Codex assistance, Apache-2.0. +No independent human or formal-kernel review is claimed. + +- Rohan Arun, PR4076: three staged entries, exact source words, T360 literal + fill, replay integration and predecessor exports. The present result starts + from his exact head 9744f9df268590295a9872b1952c695a678192b9, then + composes the later receiver-sharing improvement below. +- Dugongue / David Ganz, PR4085: receiver sharing composed with the staged + supplier, inherited native receipts, exact all-character Z4 operator proof + and event-level owner admission. The shared-covector rewrite follows Nick + Petalas' adaptive-continuation construction. All exports are pinned at + c5854c77620723aae6914c32122870519a6f820d. +- Dugongue, PR3945: terminal-width-five words, native wrapper, binary-basis + ledger, rational root enclosures and owner audit. The unmodified functions + and source-specific notices remain in their files. +- Ross Richardson, PR3605, and dataisfire, PR3734: staged-entry mechanism and + literal producer-return source construction. +- ChaloupeMusic / Erwan Secousses, PR3949: general staged-entry construction, + candidate/commuting-range machinery; PR3815: T360 clock, pattern/Hall model + and original EDF fill builder. Discovery adapted those tools to nonuniform + per-call widths and call-wide augmenting matching. +- Marius-Paul Dumitrean: exact frame solver in + research/rank7-skip-restore-optimum/frames_exact.py. Discovery used the + repository's integer-surrogate solver; explicit resulting frames, not an + asserted new optimality theorem, are certified here. +- Sagar Thakrar and roger-sato, PR3687/3693: retained exact point-set and + arbitrary-dirty semantics interpreters. Their reuse is not an independently + invented semantics engine. +- zxv, PR3682, and the complete older geometry, native, compiler, frame, owner, + packing and outer-transfer lineage retained by the predecessor packages. + +vendor/PR4076-NOTICE.md preserves the predecessor notice, and native/ preserves +its complete source-specific native and accelerator notices and licenses. +EXPORTED-SOURCES.json records byte-identical exports and source commits. +The one-third selector, four-entry source binding, new literal integer fill, +complete mixed-profile certificate and their integration are the contribution +of this package. Unsuccessful bounded searches are not claimed as barriers. diff --git a/research/staged-fourth-mixture-ceiling/source4088/PROOF.md b/research/staged-fourth-mixture-ceiling/source4088/PROOF.md new file mode 100644 index 000000000..f66b928f2 --- /dev/null +++ b/research/staged-fourth-mixture-ceiling/source4088/PROOF.md @@ -0,0 +1,131 @@ +# Finite mixed-provider construction and exact moment + +Prepared by Cinna Davis with OpenAI Codex assistance. Apache-2.0. + +## 1. Sources and common interface + +The immediate source is PR4085 at `c5854c77620723aae6914c32122870519a6f820d`, +composing receiver sharing with PR4076 at +`9744f9df268590295a9872b1952c695a678192b9` on the PR3945/3734 staged544 lineage. +PR4085 replaces the two helper544-to672/676 reads by a three-shear shared +receiver circuit. The resulting THREE words here are byte-identical exports; +the same rewrite is explicitly included in each FOUR word. Both orientations have 632 live registers and +91 private dirty buffers. Their endpoint map is `(x,y,h,b) -> (x,y+x,h,b)` in +the retained free-native-operator model, together with the dual and cleanup +boundary contracts. Ports, removed registers, native lenders, native matrices, +wrappers, cuts, protected terminals, source order and the owner template retain +those source contracts. + +## 2. Fourth-entry word + +In each retained three-entry word, helper 601 enters at `span(45)`. Raise this +to `span(127,45)`. Delete the four quarter-weight reads into targets +183, 202, 175 and 123. Before the original chronological event 10515, the exact +prefix propagation of `v=e601-e602` has + +`M v - e601 = -e602 + (1/2)e123`. + +Every encountered native/correction consumer annihilates that prefix vector. +Place `123 += 601/2` at that cut and slide `602 -= 601` through its commuting +range to original event 11161. Event numbers refer to the pinned PR4085 event +list; the literal record is the definitive source-bound construction. + +The exact frame solver supplies explicit gate frames, and cleanup is regenerated +from the complete changed word. For verification, no prefix argument or solver +output is trusted in isolation: the retained exact symbolic interpreter runs all +723 independent input symbols through both complete orientations and compares +forward, dual, reverse pullback and cleanup endpoints. All private buffer symbols +return identically and have zero leakage into live outputs. Omitting or reversing +either release is rejected even after regenerating its cleanup. + +A separate binary-basis ledger and the point-set ledger agree on + +`L3 = 2487 H1 + 713 H2 + 224 H3 + 102 H4 + 20 H5 + 8 H8`, + +`L4 = L3 + 2 H1 + 3 H3 - 3 H4`. + +Only helper 601 changes hosted width, from 8 to 7. The local paid-rank change is +`2 + 3*3 - 3*4 = -1`. Both new words additionally pass fresh native transport, +ledgers, local replay, wrappers and phases, including all-column native recipes. +These finite native checks do not establish the inherited all-size hypotheses. + +## 3. Explicit mixed schedule and owner construction + +The unchanged order contains all nine stages for each of 360 replicas, respecting +per-replica stage order. At time `t=0,...,3239`, use the fourth-entry variant of +the original orientation exactly when `t mod 3 = 0`. Thus there are 1080 fourth +calls and 2160 third calls. `MIXED-DISPATCH.json` lists every choice. + +Each variant has the same required endpoint and interface. Substituting one +correct implementation for another therefore preserves composition of the parent +operator, provided each call receives its declared legal hosted slices. The +explicit dispatch is a fixed finite table. It adds no new recursive call; the +retained uniform-implementation hypotheses must cover its fixed selection logic +and all four finite words, as they cover the predecessor's two orientations. + +For every owner and child, the verifier derives `(capacity,lo,hi]` from the +retained execution schedule and actual call order. A row `(t,h,o,c,p,z)` of the +new fill must satisfy: + +- exactly one row for each ordered `(t,h)`, over all 3240*408 roles; +- `lo < t <= hi` for that exact owner/child and a valid port `p`; +- no repeated owner source-family/port in a call; +- offset `z` equal to the accumulated earlier widths of that exact bin; +- accumulated width plus the actual selected provider's helper width at most + the child's capacity. + +The verifier also checks that different children of a common owner family have +disjoint call windows. It scans all 725760 bins, including empty bins. The +resulting idle counts are exactly + +`I = 22785 H3 + 1625 H5 + H16 + 2 H32 + 138490 H48`. + +The independent operator replay uses PR4085's unmodified exact Z4-polynomial +normalizer and event-level observer definitions. It checks every literal role +strictly after its last scalar observation and before its original idle endpoint, +productive/helper nonaliasing, disjoint slices of each original phase-axis list, +and the exact complementary residual. No axes move between child slots. +All 10,416 phase identities at the 112 ordered ports and the complete signed +eight-stream scalar controller hold. These polynomial identities hold for every +character; adding the identities modulo four extends them to every positive +tensor multiplicity. The hosted-factor collapse uses the freshly scanned mixed +fill, not a retained certificate for a different dispatch. Native endpoints and +common-cover embeddings remain the declared source interface. + +This is an integer, chronological, distinct-family witness. The discovery LP and +its floating-point solves are unnecessary for this proposition. + +## 4. Complete cost and comparison + +The full profile is `2160 L3 + 1080 L4 + I`, namely + +`8060040 H1 + 2310120 H2 + 751785 H3 + 327240 H4 + 66425 H5 + 25920 H8 + H16 + 2 H32 + 138490 H48`. + +Relative to PR4085, idle changes by + +`-57 H3 - 265 H5 + H16 + 2 H32 + 52 H48`. + +Its rank mass is 1080, exactly balancing the local rank-mass reduction -1080. +The total paid rank mass remains `65088*360`. + +Let `M(k)=sum_r n_r r^(1-k) - (896*360)73^(1-k)`. Dividing by +`73^(1-k)` gives a strictly increasing function of `k`, since every paid rank is +strictly below 73 and every count is positive. The retained rational logarithm +and alternating-exponential remainder bounds certify + +`M(0.001730978305075885693430) < 0`, + +`M(0.001730978305075885693431) > 0`. + +The exact interval endpoints are in RESULT.json and regenerated by price.py. +The same engine freshly certifies PR4085's earlier bracket. All signs and the root comparison use rational enclosures. +After subtracting the retained `10^-46 + 10^-70` outer padding, the new endpoint +still exceeds PR4085's upper endpoint by more than +`7.885876721990690*10^-9`. + +The conditional outer conclusion uses the same analytic, source, hosting, +precision, tape, recovery and BIT transfer hypotheses as the predecessor, with +the explicit finite mixed dispatch above. This package does not report a fresh +full ordinary/outer admission release. Source-registry integration and that +end-to-end replay are a separately identified remaining obligation; the finite +construction and complete moment comparison stand independently of such a run. diff --git a/research/staged-fourth-mixture-ceiling/source4088/RESULT.json b/research/staged-fourth-mixture-ceiling/source4088/RESULT.json new file mode 100644 index 000000000..d110afeae --- /dev/null +++ b/research/staged-fourth-mixture-ceiling/source4088/RESULT.json @@ -0,0 +1,40 @@ +{ + "status": "VERIFIED_FINITE_CONDITIONAL_CONSTRUCTION", + "profile": { + "1": 8060040, + "2": 2310120, + "3": 751785, + "4": 327240, + "5": 66425, + "8": 25920, + "16": 1, + "32": 2, + "48": 138490 + }, + "root_lower": "173097830507588569343/100000000000000000000000", + "root_upper": "1730978305075885693431/1000000000000000000000000", + "root_lower_decimal": "0.001730978305075885693430", + "root_upper_decimal": "0.001730978305075885693431", + "conditional_kappa": "17309783050758856934299999999999999999999998999999999999999999999999/10000000000000000000000000000000000000000000000000000000000000000000000", + "predecessor_lower": "865485209599581851369/500000000000000000000000", + "predecessor_upper": "1730970419199163702739/1000000000000000000000000", + "gain_lower_bound": "78858767219906909999999999999999999998999999999999999999999999/10000000000000000000000000000000000000000000000000000000000000000000000", + "lower_moment_interval": [ + "-32423757958362547952536091365961055478870881/1000000000000000000000000000000000000000000000000000000000000", + "-202648487239765924703350571037256596742943/6250000000000000000000000000000000000000000000000000000000" + ], + "upper_moment_interval": [ + "8462177043238460235245149633804121329928891/250000000000000000000000000000000000000000000000000000000000", + "6769741634590768188196119707043297063943113/200000000000000000000000000000000000000000000000000000000000" + ], + "calls": 3240, + "fourth_calls": 1080, + "idle": { + "3": 22785, + "5": 1625, + "16": 1, + "32": 2, + "48": 138490 + }, + "scope": "Exact finite words, fresh four-entry native replays, inherited source-pinned three-entry native receipts, complete mixed owner fill, exact Z4 phase operator for all112 ports and rational moment. Conditional on inherited uniform native, common-cover, analytic, precision, tape, recovery and BIT transfer hypotheses. Full ordinary/outer release has not been rerun for the mixed dispatch; selected frontier unchanged." +} diff --git a/research/staged-fourth-mixture-ceiling/source4088/checks/inherited_frames.py b/research/staged-fourth-mixture-ceiling/source4088/checks/inherited_frames.py new file mode 100644 index 000000000..a87dde507 --- /dev/null +++ b/research/staged-fourth-mixture-ceiling/source4088/checks/inherited_frames.py @@ -0,0 +1,160 @@ +"""Independent binary-basis ledger and declared free-operator contract for the three staged entries. + +The basis walker (b, subset, perpendicular, transform, inverse, ledger) is PR3945's checks/independent_frames.py +unchanged (Dugongue, OpenAI Codex assisted); the staged-entry contract and controls are new. +Prepared by Rohan Arun with Anthropic Claude assistance. Apache-2.0. Standard library only. +""" +from pathlib import Path +from collections import Counter +from fractions import Fraction as Q +import json,gzip,hashlib,sys,copy +PACKAGE=Path(__file__).resolve().parent.parent + +def need(ok,why): + if not ok:raise ValueError(why) + +def b(vectors): + pivots={} + for x in vectors: + need(type(x) is int and 0<=x<512,'bad frame vector') + while x: + p=x.bit_length()-1 + if p in pivots:x^=pivots[p] + else:pivots[p]=x;break + for p in sorted(pivots): + for q in sorted(pivots,reverse=True): + if q>p and (pivots[q]>>p)&1:pivots[q]^=pivots[p] + return tuple(pivots[p] for p in sorted(pivots,reverse=True)) + +def subset(A,B):return b(A+B)==B +FULL=b([1<>j)&1 else 0) for j in range(9) if j!=pivot]) +def transform(F,G): + def apply(x): + y=0 + for j in range(9): + if (x>>j)&1:y^=G[j] + return y + return b([apply(x) for x in F]) +def inverse(G): + inv={} + for x in range(512): + y=0 + for j in range(9): + if x>>j&1:y^=G[j] + need(y not in inv,'singular native matrix');inv[y]=x + return [inv[1<=224 else perpendicular(w['ports'][r-112])) for r in live} + for r,F in w['helper_final'].items():end[int(r)]=b(F) + cur=dict(start);profile=Counter() + def climb(r,F): + F=b(F);need(subset(cur[r],F),'nonmonotone frame at '+str(r));d=len(F)-len(cur[r]);cur[r]=F + if d:profile[d]+=1 + def scalar(g): + for r in g[1:3] if g[0]=='add' else g[1:2]:climb(r,g[-1]) + for g in w['A']: + if g[0]!='warp':scalar(g);continue + _,r,op,U,E=g;G=w['warps'][abs(op)-1][2] + if op<0:G=inverse(G) + need(cur[r]==b(U),'A native entry');need(transform(b(U),G)==b(E),'A native map');cur[r]=b(E) + for t in range(112,224):need(cur[t]==b(w['target_levels'].get(str(t-112),[])),'target cut level') + for r,U in zip(w['centers'],w['center_frames']): + need(cur[r]==b(U),'centre entry');temporary=b(U) + served={b(w['target_levels'].get(str(g[1]-112),[])) for g in w['cut'] if g[2]==r} + for T in sorted(served,key=lambda F:-len(F)): + need(subset(T,temporary),'centre nesting');d=len(temporary)-len(T) + if d:profile[d]+=1 + temporary=T + # The actual descent is on a private copy; live cur[r] stays U. + at={} + for record in w['warps']:at.setdefault(record[0],[]).append(record) + for i in range(len(w['B'])+1): + for _,r,G,U,E in at.get(i,[]): + need(cur[r]==b(U),'B native entry');need(transform(b(U),G)==b(E),'B native map');cur[r]=b(E) + if i=224) + need(dict(profile)=={int(r):n for r,n in w['report']['local_profile'].items()},'profile mismatch') + need(dict(inventory)=={int(r):n for r,n in w['report']['width_inventory'].items()},'inventory mismatch') + return profile,inventory + +PINS=json.loads((PACKAGE/'INPUTS.json').read_text(encoding='utf8'))['canonical_sha256'] +STAGED={'600':([45],[127,45]),'608':([45],[97,45]),'609':([45],[97,45])} +DELETED=[['add',183,600,1,4],['add',202,600,-1,4],['add',175,600,1,4],['add',123,600,-1,4], + ['add',114,608,1,4],['add',137,608,-1,4],['add',173,608,1,4],['add',121,608,-1,4], + ['add',114,609,1,4],['add',137,609,1,4],['add',173,609,1,4],['add',121,609,1,4]] +RELEASES=[['add',121,609,1,2],['add',137,608,-1,2],['add',202,600,-1,2],['add',602,600,-1,1],['add',610,608,-1,1],['add',610,609,-1,1]] +DELETED_AT=[77,78,79,80,93,94,95,96,97,98,99,100] +RELEASED_AT=[388,410,474,927,948,950] +DELTA={1:6,2:2,3:5,4:-7} + +def read(name): + w=json.loads(gzip.decompress((PACKAGE/'inputs'/name).read_bytes())) + scientific=hashlib.sha256(json.dumps(w,sort_keys=True,separators=(',',':')).encode()).hexdigest() + need(scientific==PINS[name],'canonical source guard '+name) + return w + +def signature(seq): + return [g[:3] if g[0]=='warp' else g[:-1] for g in seq + if not(g[0]=='scale' and Q(g[2],g[3])==1)] + +def compare(old,new): + for field in old: + if field not in ('A','B','restore','cleanup','start_extra','report','warps'): + need(old[field]==new[field],'changed caller field '+field) + need(old['helper_final']==new['helper_final'] and len(new['helper_final'])==91,'returns unchanged') + keys=set(old['start_extra'])|set(new['start_extra']) + changed={r:(old['start_extra'].get(r),new['start_extra'].get(r)) for r in keys if old['start_extra'].get(r)!=new['start_extra'].get(r)} + need(changed=={r:(list(x),list(y)) for r,(x,y) in STAGED.items()},'staged entrance set') + for r,(x,y) in changed.items(): + need(subset(b(x),b(y)) and len(b(y))==len(b(x))+1 and r not in new['helper_final'],'entrance raised by one dimension on an ordinary helper') + for sec in ('A','restore'): + need(signature(old[sec])==signature(new[sec]),'free opcode sequence '+sec) + so,sn=signature(old['B']),signature(new['B']) + need([so[i] for i in DELETED_AT]==DELETED,'declared deleted reads at their source positions') + need([sn[i] for i in RELEASED_AT]==RELEASES,'declared releases at their target positions') + need([g for i,g in enumerate(so) if i not in DELETED_AT]==[g for i,g in enumerate(sn) if i not in RELEASED_AT],'B opcode sequence differs only by declared deletions and releases') + need(Counter(map(json.dumps,sn))==Counter(map(json.dumps,so))-Counter(map(json.dumps,DELETED))+Counter(map(json.dumps,RELEASES)),'opcode multiset balance') + need([r[1:3] for r in old['warps']]==[r[1:3] for r in new['warps']],'native matrices/lenders') + po,io=ledger(old);pn,inn=ledger(new) + delta={r:pn[r]-po[r] for r in set(po)|set(pn) if pn[r]!=po[r]} + need(delta==DELTA and sum(r*n for r,n in delta.items())==-3,'local profile delta/rank mass') + need(io==Counter({5:28,6:18,7:53,8:96,9:213}),'old width inventory') + need(inn==Counter({5:28,6:18,7:56,8:93,9:213}),'new width inventory') + return {'old_profile':dict(po),'new_profile':dict(pn),'local_profile_delta':delta,'staged_entrances':sorted(changed,key=int),'deleted_reads':len(DELETED),'releases':len(RELEASES),'buffers':91} + +def controls(old,new): + outcomes=[] + def reject(label,callback): + try:callback() + except ValueError:outcomes.append(label);return + raise ValueError('mutation was accepted: '+label) + z=copy.deepcopy(new);z['report']['local_profile']['1']+=1 + reject('wrong paid histogram',lambda:ledger(z)) + z=copy.deepcopy(new);z['warps'][0][4]=[] + reject('wrong native exit frame',lambda:ledger(z)) + z=copy.deepcopy(new);z['start_extra']['608']=[45] + reject('missing staged entrance',lambda:compare(old,z)) + z=copy.deepcopy(new);k=next(i for i,g in enumerate(z['B']) if g[:-1]==RELEASES[0]);z['B'][k][3]+=1 + reject('changed release coefficient',lambda:compare(old,z)) + z=copy.deepcopy(new);g=next(g for g in z['A'] if g[0]=='add');g[3]+=1 + reject('changed scalar operator',lambda:compare(old,z)) + return outcomes + +def main(): + results={};mutation_checks=[] + for provider in ('base','extra'): + old,new=read('OLD-'+provider+'.json.gz'),read('NEW-'+provider+'.json.gz') + results[provider]=compare(old,new) + if '--controls' in sys.argv:mutation_checks += [provider+': '+x for x in controls(old,new)] + print(json.dumps({'status':'PASS_INDEPENDENT_BINARY_BASIS_LEDGER','canonical_source_sha256':PINS,'providers':results,'rejected_controls':mutation_checks,'scope':'Independent local binary frames, exact histogram/inventory and declared staged-entry operator contract; native phases, dirty semantics and literal owner/outer assembly checked separately.'},sort_keys=True)) + +if __name__=='__main__':main() diff --git a/research/staged-fourth-mixture-ceiling/source4088/inputs/FOUR-base.json.gz b/research/staged-fourth-mixture-ceiling/source4088/inputs/FOUR-base.json.gz new file mode 100644 index 000000000..65957e5ca Binary files /dev/null and b/research/staged-fourth-mixture-ceiling/source4088/inputs/FOUR-base.json.gz differ diff --git a/research/staged-fourth-mixture-ceiling/source4088/inputs/FOUR-extra.json.gz b/research/staged-fourth-mixture-ceiling/source4088/inputs/FOUR-extra.json.gz new file mode 100644 index 000000000..1f3239c30 Binary files /dev/null and b/research/staged-fourth-mixture-ceiling/source4088/inputs/FOUR-extra.json.gz differ diff --git a/research/staged-fourth-mixture-ceiling/source4088/inputs/THREE-base.json.gz b/research/staged-fourth-mixture-ceiling/source4088/inputs/THREE-base.json.gz new file mode 100644 index 000000000..137793e27 Binary files /dev/null and b/research/staged-fourth-mixture-ceiling/source4088/inputs/THREE-base.json.gz differ diff --git a/research/staged-fourth-mixture-ceiling/source4088/inputs/THREE-extra.json.gz b/research/staged-fourth-mixture-ceiling/source4088/inputs/THREE-extra.json.gz new file mode 100644 index 000000000..7cce921b2 Binary files /dev/null and b/research/staged-fourth-mixture-ceiling/source4088/inputs/THREE-extra.json.gz differ diff --git a/research/staged-fourth-mixture-ceiling/source4088/owner/ORDER.json b/research/staged-fourth-mixture-ceiling/source4088/owner/ORDER.json new file mode 100644 index 000000000..58d4b4c34 --- /dev/null +++ b/research/staged-fourth-mixture-ceiling/source4088/owner/ORDER.json @@ -0,0 +1 @@ +[[0, 0], [0, 45], [0, 90], [0, 135], [0, 180], [0, 225], [0, 270], [0, 315], [0, 1], [0, 46], [0, 91], [0, 136], [0, 181], [0, 226], [0, 271], [0, 316], [0, 2], [0, 47], [0, 92], [0, 137], [0, 182], [0, 227], [0, 272], [0, 317], [0, 3], [0, 48], [0, 93], [0, 138], [0, 183], [0, 228], [0, 273], [0, 318], [0, 4], [0, 49], [0, 94], [0, 139], [0, 184], [0, 229], [0, 274], [0, 319], [1, 0], [1, 45], [1, 90], [1, 135], [1, 180], [1, 225], [1, 270], [1, 315], [0, 5], [0, 50], [0, 95], [0, 140], [0, 185], [0, 230], [0, 275], [0, 320], [1, 1], [1, 46], [1, 91], [1, 136], [1, 181], [1, 226], [0, 6], [1, 271], [0, 51], [0, 96], [0, 141], [1, 316], [0, 186], [0, 231], [0, 276], [0, 321], [1, 2], [0, 7], [0, 52], [0, 97], [1, 47], [0, 142], [0, 187], [0, 232], [1, 92], [0, 277], [0, 322], [0, 8], [1, 137], [0, 53], [0, 98], [0, 143], [1, 182], [0, 188], [0, 233], [0, 278], [1, 227], [0, 323], [0, 9], [0, 54], [0, 99], [1, 272], [0, 144], [0, 189], [0, 234], [1, 317], [0, 279], [0, 324], [2, 0], [1, 3], [2, 45], [2, 90], [2, 135], [1, 48], [2, 180], [2, 225], [2, 270], [2, 315], [1, 93], [0, 10], [0, 55], [0, 100], [1, 138], [0, 145], [0, 190], [0, 235], [1, 183], [0, 280], [0, 325], [2, 1], [1, 228], [2, 46], [2, 91], [2, 136], [2, 181], [1, 273], [2, 226], [2, 271], [2, 316], [1, 318], [0, 11], [0, 56], [0, 101], [1, 4], [0, 146], [0, 191], [0, 236], [1, 49], [0, 281], [0, 326], [2, 2], [1, 94], [2, 47], [2, 92], [2, 137], [2, 182], [1, 139], [2, 227], [2, 272], [2, 317], [1, 184], [0, 12], [0, 57], [0, 102], [1, 229], [0, 147], [0, 192], [0, 237], [1, 274], [0, 282], [0, 327], [2, 3], [2, 48], [1, 319], [2, 93], [2, 138], [2, 183], [1, 5], [2, 228], [2, 273], [2, 318], [1, 50], [0, 13], [0, 58], [0, 103], [1, 95], [0, 148], [0, 193], [0, 238], [1, 140], [0, 283], [0, 328], [2, 4], [2, 49], [1, 185], [2, 94], [2, 139], [2, 184], [1, 230], [2, 229], [2, 274], [2, 319], [1, 275], [3, 0], [3, 45], [3, 90], [1, 320], [3, 135], [3, 180], [3, 225], [3, 270], [1, 6], [3, 315], [0, 14], [0, 59], [1, 51], [0, 104], [0, 149], [0, 194], [1, 96], [0, 239], [0, 284], [0, 329], [1, 141], [2, 5], [2, 50], [2, 95], [1, 186], [2, 140], [2, 185], [2, 230], [2, 275], [1, 231], [2, 320], [3, 1], [3, 46], [1, 276], [3, 91], [3, 136], [3, 181], [1, 321], [3, 226], [3, 271], [3, 316], [1, 7], [0, 15], [0, 60], [0, 105], [0, 150], [1, 52], [0, 195], [0, 240], [0, 285], [1, 97], [0, 330], [2, 6], [2, 51], [1, 142], [2, 96], [2, 141], [2, 186], [1, 187], [2, 231], [2, 276], [2, 321], [3, 2], [1, 232], [3, 47], [3, 92], [3, 137], [1, 277], [3, 182], [3, 227], [3, 272], [1, 322], [3, 317], [0, 16], [0, 61], [1, 8], [0, 106], [0, 151], [0, 196], [1, 53], [0, 241], [0, 286], [0, 331], [2, 7], [1, 98], [2, 52], [2, 97], [2, 142], [1, 143], [2, 187], [2, 232], [2, 277], [1, 188], [2, 322], [3, 3], [3, 48], [1, 233], [3, 93], [3, 138], [3, 183], [3, 228], [1, 278], [3, 273], [3, 318], [0, 17], [1, 323], [0, 62], [0, 107], [0, 152], [1, 9], [0, 197], [0, 242], [0, 287], [1, 54], [0, 332], [2, 8], [2, 53], [1, 99], [2, 98], [2, 143], [2, 188], [2, 233], [1, 144], [2, 278], [2, 323], [3, 4], [1, 189], [3, 49], [3, 94], [3, 139], [1, 234], [3, 184], [3, 229], [3, 274], [1, 279], [3, 319], [0, 18], [0, 63], [0, 108], [1, 324], [0, 153], [0, 198], [0, 243], [1, 10], [0, 288], [0, 333], [2, 9], [1, 55], [2, 54], [2, 99], [2, 144], [1, 100], [2, 189], [2, 234], [2, 279], [2, 324], [1, 145], [4, 0], [4, 45], [4, 90], [1, 190], [4, 135], [4, 180], [4, 225], [1, 235], [4, 270], [4, 315], [3, 5], [1, 280], [3, 50], [3, 95], [3, 140], [1, 325], [3, 185], [3, 230], [3, 275], [3, 320], [1, 11], [0, 19], [0, 64], [0, 109], [1, 56], [0, 154], [0, 199], [0, 244], [1, 101], [0, 289], [0, 334], [2, 10], [1, 146], [2, 55], [2, 100], [2, 145], [2, 190], [1, 191], [2, 235], [2, 280], [2, 325], [1, 236], [4, 1], [4, 46], [4, 91], [1, 281], [4, 136], [4, 181], [4, 226], [1, 326], [4, 271], [4, 316], [3, 6], [1, 12], [3, 51], [3, 96], [3, 141], [3, 186], [1, 57], [3, 231], [3, 276], [3, 321], [1, 102], [0, 20], [0, 65], [0, 110], [1, 147], [0, 155], [0, 200], [0, 245], [1, 192], [0, 290], [0, 335], [2, 11], [2, 56], [1, 237], [2, 101], [2, 146], [2, 191], [1, 282], [2, 236], [2, 281], [2, 326], [1, 327], [4, 2], [4, 47], [4, 92], [1, 13], [4, 137], [4, 182], [4, 227], [1, 58], [4, 272], [4, 317], [3, 7], [3, 52], [1, 103], [3, 97], [3, 142], [3, 187], [1, 148], [3, 232], [3, 277], [3, 322], [1, 193], [0, 21], [0, 66], [0, 111], [1, 238], [0, 156], [0, 201], [0, 246], [0, 291], [1, 283], [0, 336], [2, 12], [2, 57], [1, 328], [2, 102], [2, 147], [2, 192], [1, 14], [2, 237], [2, 282], [2, 327], [1, 59], [4, 3], [4, 48], [4, 93], [4, 138], [1, 104], [4, 183], [4, 228], [4, 273], [1, 149], [4, 318], [3, 8], [3, 53], [1, 194], [3, 98], [3, 143], [3, 188], [1, 239], [3, 233], [3, 278], [3, 323], [1, 284], [0, 22], [0, 67], [0, 112], [0, 157], [1, 329], [0, 202], [0, 247], [0, 292], [1, 15], [0, 337], [2, 13], [2, 58], [1, 60], [2, 103], [2, 148], [2, 193], [1, 105], [2, 238], [2, 283], [2, 328], [4, 4], [1, 150], [4, 49], [4, 94], [4, 139], [1, 195], [4, 184], [4, 229], [4, 274], [1, 240], [4, 319], [3, 9], [3, 54], [1, 285], [3, 99], [3, 144], [3, 189], [1, 330], [3, 234], [3, 279], [3, 324], [0, 23], [1, 16], [0, 68], [0, 113], [0, 158], [1, 61], [0, 203], [0, 248], [0, 293], [1, 106], [0, 338], [5, 0], [5, 45], [1, 151], [5, 90], [5, 135], [5, 180], [5, 225], [1, 196], [5, 270], [5, 315], [2, 14], [1, 241], [2, 59], [2, 104], [2, 149], [1, 286], [2, 194], [2, 239], [2, 284], [1, 331], [2, 329], [4, 5], [4, 50], [4, 95], [1, 17], [4, 140], [4, 185], [4, 230], [1, 62], [4, 275], [4, 320], [3, 10], [1, 107], [3, 55], [3, 100], [3, 145], [1, 152], [3, 190], [3, 235], [3, 280], [1, 197], [3, 325], [0, 24], [0, 69], [0, 114], [1, 242], [0, 159], [0, 204], [0, 249], [1, 287], [0, 294], [0, 339], [5, 1], [1, 332], [5, 46], [5, 91], [5, 136], [1, 18], [5, 181], [5, 226], [5, 271], [5, 316], [1, 63], [2, 15], [2, 60], [2, 105], [1, 108], [2, 150], [2, 195], [2, 240], [1, 153], [2, 285], [2, 330], [4, 6], [1, 198], [4, 51], [4, 96], [4, 141], [1, 243], [4, 186], [4, 231], [4, 276], [4, 321], [1, 288], [3, 11], [3, 56], [3, 101], [1, 333], [3, 146], [3, 191], [3, 236], [1, 19], [3, 281], [3, 326], [0, 25], [1, 64], [0, 70], [0, 115], [0, 160], [0, 205], [1, 109], [0, 250], [0, 295], [0, 340], [1, 154], [5, 2], [5, 47], [5, 92], [1, 199], [5, 137], [5, 182], [5, 227], [1, 244], [5, 272], [5, 317], [2, 16], [1, 289], [2, 61], [2, 106], [2, 151], [2, 196], [1, 334], [2, 241], [2, 286], [2, 331], [1, 20], [4, 7], [4, 52], [4, 97], [1, 65], [4, 142], [4, 187], [4, 232], [1, 110], [4, 277], [4, 322], [3, 12], [3, 57], [1, 155], [3, 102], [3, 147], [3, 192], [1, 200], [3, 237], [3, 282], [3, 327], [1, 245], [0, 26], [0, 71], [0, 116], [1, 290], [0, 161], [0, 206], [0, 251], [0, 296], [1, 335], [0, 341], [5, 3], [5, 48], [1, 21], [5, 93], [5, 138], [5, 183], [1, 66], [5, 228], [5, 273], [5, 318], [1, 111], [2, 17], [2, 62], [2, 107], [1, 156], [2, 152], [2, 197], [2, 242], [2, 287], [1, 201], [2, 332], [4, 8], [4, 53], [1, 246], [4, 98], [4, 143], [4, 188], [1, 291], [4, 233], [4, 278], [4, 323], [1, 336], [3, 13], [3, 58], [3, 103], [3, 148], [1, 22], [3, 193], [3, 238], [3, 283], [1, 67], [3, 328], [0, 27], [0, 72], [1, 112], [0, 117], [0, 162], [0, 207], [1, 157], [0, 252], [0, 297], [0, 342], [1, 202], [5, 4], [5, 49], [5, 94], [5, 139], [1, 247], [5, 184], [5, 229], [5, 274], [1, 292], [5, 319], [2, 18], [2, 63], [1, 337], [2, 108], [2, 153], [2, 198], [2, 243], [2, 288], [2, 333], [4, 9], [4, 54], [4, 99], [4, 144], [4, 189], [4, 234], [4, 279], [4, 324], [1, 23], [1, 68], [1, 113], [1, 158], [6, 0], [6, 45], [1, 203], [6, 90], [6, 135], [6, 180], [6, 225], [1, 248], [6, 270], [6, 315], [3, 14], [1, 293], [3, 59], [3, 104], [3, 149], [1, 338], [3, 194], [3, 239], [3, 284], [3, 329], [0, 28], [0, 73], [0, 118], [0, 163], [0, 208], [0, 253], [0, 298], [0, 343], [5, 5], [5, 50], [5, 95], [5, 140], [5, 185], [5, 230], [5, 275], [5, 320], [2, 19], [2, 64], [2, 109], [2, 154], [2, 199], [2, 244], [2, 289], [2, 334], [4, 10], [4, 55], [4, 100], [4, 145], [4, 190], [4, 235], [4, 280], [4, 325], [1, 24], [1, 69], [1, 114], [1, 159], [1, 204], [1, 249], [1, 294], [1, 339], [6, 1], [6, 46], [6, 91], [6, 136], [6, 181], [6, 226], [6, 271], [6, 316], [3, 15], [3, 60], [3, 105], [3, 150], [3, 195], [3, 240], [3, 285], [3, 330], [0, 29], [0, 74], [0, 119], [0, 164], [0, 209], [0, 254], [0, 299], [0, 344], [5, 6], [5, 51], [5, 96], [5, 141], [5, 186], [5, 231], [5, 276], [5, 321], [2, 20], [2, 65], [2, 110], [2, 155], [2, 200], [2, 245], [2, 290], [2, 335], [4, 11], [4, 56], [4, 101], [4, 146], [4, 191], [4, 236], [4, 281], [4, 326], [1, 25], [1, 70], [1, 115], [1, 160], [1, 205], [1, 250], [1, 295], [1, 340], [6, 2], [6, 47], [6, 92], [6, 137], [6, 182], [6, 227], [6, 272], [6, 317], [3, 16], [3, 61], [3, 106], [3, 151], [3, 196], [3, 241], [3, 286], [3, 331], [0, 30], [0, 75], [0, 120], [0, 165], [0, 210], [0, 255], [0, 300], [0, 345], [5, 7], [5, 52], [5, 97], [5, 142], [5, 187], [5, 232], [5, 277], [5, 322], [2, 21], [2, 66], [2, 111], [2, 156], [2, 201], [2, 246], [2, 291], [2, 336], [4, 12], [4, 57], [4, 102], [4, 147], [4, 192], [4, 237], [4, 282], [4, 327], [1, 26], [1, 71], [1, 116], [1, 161], [1, 206], [1, 251], [1, 296], [1, 341], [6, 3], [6, 48], [6, 93], [6, 138], [6, 183], [6, 228], [6, 273], [6, 318], [3, 17], [3, 62], [3, 107], [3, 152], [3, 197], [3, 242], [3, 287], [3, 332], [0, 31], [0, 76], [0, 121], [0, 166], [0, 211], [0, 256], [0, 301], [0, 346], [5, 8], [5, 53], [5, 98], [5, 143], [5, 188], [5, 233], [5, 278], [5, 323], [2, 22], [2, 67], [2, 112], [2, 157], [2, 202], [2, 247], [2, 292], [2, 337], [4, 13], [4, 58], [4, 103], [4, 148], [4, 193], [4, 238], [4, 283], [4, 328], [1, 27], [1, 72], [1, 117], [1, 162], [1, 207], [1, 252], [1, 297], [1, 342], [6, 4], [6, 49], [6, 94], [6, 139], [6, 184], [6, 229], [6, 274], [6, 319], [3, 18], [3, 63], [3, 108], [3, 153], [3, 198], [3, 243], [3, 288], [3, 333], [0, 32], [0, 77], [0, 122], [0, 167], [0, 212], [0, 257], [0, 302], [0, 347], [5, 9], [5, 54], [5, 99], [5, 144], [5, 189], [5, 234], [5, 279], [5, 324], [2, 23], [2, 68], [2, 113], [2, 158], [2, 203], [2, 248], [2, 293], [2, 338], [7, 0], [7, 45], [7, 90], [7, 135], [7, 180], [7, 225], [7, 270], [7, 315], [4, 14], [4, 59], [4, 104], [4, 149], [4, 194], [4, 239], [4, 284], [4, 329], [1, 28], [1, 73], [1, 118], [1, 163], [1, 208], [1, 253], [1, 298], [1, 343], [6, 5], [6, 50], [6, 95], [6, 140], [6, 185], [6, 230], [6, 275], [6, 320], [3, 19], [3, 64], [3, 109], [3, 154], [3, 199], [3, 244], [3, 289], [3, 334], [0, 33], [0, 78], [0, 123], [0, 168], [0, 213], [0, 258], [0, 303], [0, 348], [5, 10], [5, 55], [5, 100], [5, 145], [5, 190], [5, 235], [5, 280], [5, 325], [2, 24], [2, 69], [2, 114], [2, 159], [2, 204], [2, 249], [2, 294], [2, 339], [7, 1], [7, 46], [7, 91], [7, 136], [7, 181], [7, 226], [7, 271], [7, 316], [4, 15], [4, 60], [4, 105], [4, 150], [4, 195], [4, 240], [4, 285], [4, 330], [1, 29], [1, 74], [1, 119], [1, 164], [1, 209], [1, 254], [1, 299], [1, 344], [6, 6], [6, 51], [6, 96], [6, 141], [6, 186], [6, 231], [6, 276], [6, 321], [3, 20], [3, 65], [3, 110], [3, 155], [3, 200], [3, 245], [3, 290], [3, 335], [0, 34], [0, 79], [0, 124], [0, 169], [0, 214], [0, 259], [0, 304], [0, 349], [5, 11], [5, 56], [5, 101], [5, 146], [5, 191], [5, 236], [5, 281], [5, 326], [2, 25], [2, 70], [2, 115], [2, 160], [2, 205], [2, 250], [2, 295], [2, 340], [7, 2], [7, 47], [7, 92], [7, 137], [7, 182], [7, 227], [7, 272], [7, 317], [4, 16], [4, 61], [4, 106], [4, 151], [4, 196], [4, 241], [4, 286], [4, 331], [1, 30], [1, 75], [1, 120], [1, 165], [1, 210], [1, 255], [1, 300], [1, 345], [6, 7], [6, 52], [6, 97], [6, 142], [6, 187], [6, 232], [6, 277], [6, 322], [3, 21], [3, 66], [3, 111], [3, 156], [3, 201], [3, 246], [3, 291], [3, 336], [0, 35], [0, 80], [0, 125], [0, 170], [0, 215], [0, 260], [0, 305], [0, 350], [5, 12], [5, 57], [5, 102], [5, 147], [5, 192], [5, 237], [5, 282], [5, 327], [2, 26], [2, 71], [2, 116], [2, 161], [2, 206], [2, 251], [2, 296], [2, 341], [7, 3], [7, 48], [7, 93], [7, 138], [7, 183], [7, 228], [7, 273], [7, 318], [4, 17], [4, 62], [4, 107], [4, 152], [4, 197], [4, 242], [4, 287], [4, 332], [1, 31], [1, 76], [1, 121], [1, 166], [1, 211], [1, 256], [1, 301], [1, 346], [6, 8], [6, 53], [6, 98], [6, 143], [6, 188], [6, 233], [6, 278], [6, 323], [3, 22], [3, 67], [3, 112], [3, 157], [3, 202], [3, 247], [3, 292], [3, 337], [0, 36], [0, 81], [0, 126], [0, 171], [0, 216], [0, 261], [0, 306], [0, 351], [5, 13], [5, 58], [5, 103], [5, 148], [5, 193], [5, 238], [5, 283], [5, 328], [2, 27], [2, 72], [2, 117], [2, 162], [2, 207], [2, 252], [2, 297], [2, 342], [7, 4], [7, 49], [7, 94], [7, 139], [7, 184], [7, 229], [7, 274], [7, 319], [4, 18], [4, 63], [4, 108], [4, 153], [4, 198], [4, 243], [4, 288], [4, 333], [1, 32], [1, 77], [1, 122], [1, 167], [1, 212], [1, 257], [1, 302], [1, 347], [6, 9], [6, 54], [6, 99], [6, 144], [6, 189], [6, 234], [6, 279], [6, 324], [3, 23], [3, 68], [3, 113], [3, 158], [3, 203], [3, 248], [3, 293], [3, 338], [8, 0], [8, 45], [8, 90], [8, 135], [8, 180], [8, 225], [8, 270], [8, 315], [5, 14], [5, 59], [5, 104], [5, 149], [5, 194], [5, 239], [5, 284], [5, 329], [2, 28], [2, 73], [2, 118], [2, 163], [2, 208], [2, 253], [2, 298], [2, 343], [7, 5], [7, 50], [7, 95], [7, 140], [7, 185], [7, 230], [7, 275], [7, 320], [4, 19], [4, 64], [4, 109], [4, 154], [4, 199], [4, 244], [4, 289], [4, 334], [1, 33], [1, 78], [1, 123], [1, 168], [1, 213], [1, 258], [1, 303], [1, 348], [6, 10], [6, 55], [6, 100], [6, 145], [6, 190], [6, 235], [6, 280], [6, 325], [3, 24], [3, 69], [3, 114], [3, 159], [3, 204], [3, 249], [3, 294], [3, 339], [8, 1], [8, 46], [8, 91], [8, 136], [8, 181], [8, 226], [8, 271], [8, 316], [5, 15], [5, 60], [5, 105], [5, 150], [5, 195], [5, 240], [5, 285], [5, 330], [2, 29], [2, 74], [2, 119], [2, 164], [2, 209], [2, 254], [2, 299], [2, 344], [7, 6], [7, 51], [7, 96], [7, 141], [7, 186], [7, 231], [7, 276], [7, 321], [4, 20], [4, 65], [4, 110], [4, 155], [4, 200], [4, 245], [4, 290], [4, 335], [1, 34], [1, 79], [1, 124], [1, 169], [1, 214], [1, 259], [1, 304], [1, 349], [6, 11], [6, 56], [6, 101], [6, 146], [6, 191], [6, 236], [6, 281], [6, 326], [3, 25], [3, 70], [3, 115], [3, 160], [3, 205], [3, 250], [3, 295], [3, 340], [8, 2], [8, 47], [8, 92], [8, 137], [8, 182], [8, 227], [8, 272], [8, 317], [5, 16], [5, 61], [5, 106], [5, 151], [5, 196], [5, 241], [5, 286], [5, 331], [2, 30], [2, 75], [2, 120], [2, 165], [2, 210], [2, 255], [2, 300], [2, 345], [7, 7], [7, 52], [7, 97], [7, 142], [7, 187], [7, 232], [7, 277], [7, 322], [4, 21], [4, 66], [4, 111], [4, 156], [4, 201], [4, 246], [4, 291], [4, 336], [1, 35], [1, 80], [1, 125], [1, 170], [1, 215], [1, 260], [1, 305], [1, 350], [6, 12], [6, 57], [6, 102], [6, 147], [6, 192], [6, 237], [6, 282], [6, 327], [3, 26], [3, 71], [3, 116], [3, 161], [3, 206], [3, 251], [3, 296], [3, 341], [8, 3], [8, 48], [8, 93], [8, 138], [8, 183], [8, 228], [8, 273], [8, 318], [5, 17], [5, 62], [5, 107], [5, 152], [5, 197], [5, 242], [5, 287], [5, 332], [2, 31], [2, 76], [2, 121], [2, 166], [2, 211], [2, 256], [2, 301], [2, 346], [7, 8], [7, 53], [7, 98], [7, 143], [7, 188], [7, 233], [7, 278], [7, 323], [4, 22], [4, 67], [4, 112], [4, 157], [4, 202], [4, 247], [4, 292], [4, 337], [1, 36], [1, 81], [1, 126], [1, 171], [1, 216], [1, 261], [1, 306], [1, 351], [6, 13], [6, 58], [6, 103], [6, 148], [6, 193], [6, 238], [6, 283], [6, 328], [3, 27], [3, 72], [3, 117], [3, 162], [3, 207], [3, 252], [3, 297], [3, 342], [8, 4], [8, 49], [8, 94], [8, 139], [8, 184], [8, 229], [8, 274], [8, 319], [5, 18], [5, 63], [5, 108], [5, 153], [5, 198], [5, 243], [5, 288], [5, 333], [2, 32], [2, 77], [2, 122], [2, 167], [2, 212], [2, 257], [2, 302], [2, 347], [7, 9], [7, 54], [7, 99], [7, 144], [7, 189], [7, 234], [7, 279], [7, 324], [4, 23], [4, 68], [4, 113], [4, 158], [4, 203], [4, 248], [4, 293], [4, 338], [6, 14], [6, 59], [6, 104], [6, 149], [6, 194], [6, 239], [6, 284], [6, 329], [3, 28], [3, 73], [3, 118], [3, 163], [3, 208], [3, 253], [3, 298], [3, 343], [8, 5], [8, 50], [8, 95], [8, 140], [8, 185], [8, 230], [8, 275], [8, 320], [5, 19], [5, 64], [5, 109], [5, 154], [5, 199], [5, 244], [5, 289], [5, 334], [2, 33], [2, 78], [2, 123], [2, 168], [2, 213], [2, 258], [2, 303], [2, 348], [7, 10], [7, 55], [7, 100], [7, 145], [7, 190], [7, 235], [7, 280], [7, 325], [4, 24], [4, 69], [4, 114], [4, 159], [4, 204], [4, 249], [4, 294], [4, 339], [6, 15], [6, 60], [6, 105], [6, 150], [6, 195], [6, 240], [6, 285], [6, 330], [3, 29], [3, 74], [3, 119], [3, 164], [3, 209], [3, 254], [3, 299], [3, 344], [8, 6], [8, 51], [8, 96], [8, 141], [8, 186], [8, 231], [8, 276], [8, 321], [5, 20], [5, 65], [5, 110], [5, 155], [5, 200], [5, 245], [5, 290], [5, 335], [2, 34], [2, 79], [2, 124], [2, 169], [2, 214], [2, 259], [2, 304], [2, 349], [7, 11], [7, 56], [7, 101], [7, 146], [7, 191], [7, 236], [7, 281], [7, 326], [4, 25], [4, 70], [4, 115], [4, 160], [4, 205], [4, 250], [4, 295], [4, 340], [6, 16], [6, 61], [6, 106], [6, 151], [6, 196], [6, 241], [6, 286], [6, 331], [3, 30], [3, 75], [3, 120], [3, 165], [3, 210], [3, 255], [3, 300], [3, 345], [8, 7], [8, 52], [8, 97], [8, 142], [8, 187], [8, 232], [8, 277], [8, 322], [5, 21], [5, 66], [5, 111], [5, 156], [5, 201], [5, 246], [5, 291], [5, 336], [2, 35], [2, 80], [2, 125], [2, 170], [2, 215], [2, 260], [2, 305], [2, 350], [7, 12], [7, 57], [7, 102], [7, 147], [7, 192], [7, 237], [7, 282], [7, 327], [4, 26], [4, 71], [4, 116], [4, 161], [4, 206], [4, 251], [4, 296], [4, 341], [6, 17], [6, 62], [6, 107], [6, 152], [6, 197], [6, 242], [6, 287], [6, 332], [3, 31], [3, 76], [3, 121], [3, 166], [3, 211], [3, 256], [3, 301], [3, 346], [8, 8], [8, 53], [8, 98], [8, 143], [8, 188], [8, 233], [8, 278], [8, 323], [5, 22], [5, 67], [5, 112], [5, 157], [5, 202], [5, 247], [5, 292], [5, 337], [2, 36], [2, 81], [2, 126], [2, 171], [2, 216], [2, 261], [2, 306], [2, 351], [7, 13], [7, 58], [7, 103], [7, 148], [7, 193], [7, 238], [7, 283], [7, 328], [4, 27], [4, 72], [4, 117], [4, 162], [4, 207], [4, 252], [4, 297], [4, 342], [6, 18], [6, 63], [6, 108], [6, 153], [6, 198], [6, 243], [6, 288], [6, 333], [3, 32], [3, 77], [3, 122], [3, 167], [3, 212], [3, 257], [3, 302], [3, 347], [8, 9], [8, 54], [8, 99], [8, 144], [8, 189], [8, 234], [8, 279], [8, 324], [5, 23], [5, 68], [5, 113], [5, 158], [5, 203], [5, 248], [5, 293], [5, 338], [7, 14], [7, 59], [7, 104], [7, 149], [7, 194], [7, 239], [7, 284], [7, 329], [4, 28], [4, 73], [4, 118], [4, 163], [4, 208], [4, 253], [4, 298], [4, 343], [6, 19], [6, 64], [6, 109], [6, 154], [6, 199], [6, 244], [6, 289], [6, 334], [3, 33], [3, 78], [3, 123], [3, 168], [3, 213], [3, 258], [3, 303], [3, 348], [8, 10], [8, 55], [8, 100], [8, 145], [8, 190], [8, 235], [8, 280], [8, 325], [5, 24], [5, 69], [5, 114], [5, 159], [5, 204], [5, 249], [5, 294], [5, 339], [7, 15], [7, 60], [7, 105], [7, 150], [7, 195], [7, 240], [7, 285], [7, 330], [4, 29], [4, 74], [4, 119], [4, 164], [4, 209], [4, 254], [4, 299], [4, 344], [6, 20], [6, 65], [6, 110], [6, 155], [6, 200], [6, 245], [6, 290], [6, 335], [3, 34], [3, 79], [3, 124], [3, 169], [3, 214], [3, 259], [3, 304], [3, 349], [8, 11], [8, 56], [8, 101], [8, 146], [8, 191], [8, 236], [8, 281], [8, 326], [5, 25], [5, 70], [5, 115], [5, 160], [5, 205], [5, 250], [5, 295], [5, 340], [7, 16], [7, 61], [7, 106], [7, 151], [7, 196], [7, 241], [7, 286], [7, 331], [4, 30], [4, 75], [4, 120], [4, 165], [4, 210], [4, 255], [4, 300], [4, 345], [6, 21], [6, 66], [6, 111], [6, 156], [6, 201], [6, 246], [6, 291], [6, 336], [3, 35], [3, 80], [3, 125], [3, 170], [3, 215], [3, 260], [3, 305], [3, 350], [8, 12], [8, 57], [8, 102], [8, 147], [8, 192], [8, 237], [8, 282], [8, 327], [5, 26], [5, 71], [5, 116], [5, 161], [5, 206], [5, 251], [5, 296], [5, 341], [7, 17], [7, 62], [7, 107], [7, 152], [7, 197], [7, 242], [7, 287], [7, 332], [4, 31], [4, 76], [4, 121], [4, 166], [4, 211], [4, 256], [4, 301], [4, 346], [6, 22], [6, 67], [6, 112], [6, 157], [6, 202], [6, 247], [6, 292], [6, 337], [3, 36], [3, 81], [3, 126], [3, 171], [3, 216], [3, 261], [3, 306], [3, 351], [8, 13], [8, 58], [8, 103], [8, 148], [8, 193], [8, 238], [8, 283], [8, 328], [5, 27], [5, 72], [5, 117], [5, 162], [5, 207], [5, 252], [5, 297], [5, 342], [7, 18], [7, 63], [7, 108], [7, 153], [7, 198], [7, 243], [7, 288], [7, 333], [4, 32], [4, 77], [4, 122], [4, 167], [4, 212], [4, 257], [4, 302], [4, 347], [6, 23], [6, 68], [6, 113], [6, 158], [6, 203], [6, 248], [6, 293], [6, 338], [8, 14], [8, 59], [8, 104], [8, 149], [8, 194], [8, 239], [8, 284], [8, 329], [5, 28], [5, 73], [5, 118], [5, 163], [5, 208], [5, 253], [5, 298], [5, 343], [7, 19], [7, 64], [7, 109], [7, 154], [7, 199], [7, 244], [7, 289], [7, 334], [4, 33], [4, 78], [4, 123], [4, 168], [4, 213], [4, 258], [4, 303], [4, 348], [6, 24], [6, 69], [6, 114], [6, 159], [6, 204], [6, 249], [6, 294], [6, 339], [8, 15], [8, 60], [8, 105], [8, 150], [8, 195], [8, 240], [8, 285], [8, 330], [5, 29], [5, 74], [5, 119], [5, 164], [5, 209], [5, 254], [5, 299], [5, 344], [7, 20], [7, 65], [7, 110], [7, 155], [7, 200], [7, 245], [7, 290], [7, 335], [4, 34], [4, 79], [4, 124], [4, 169], [4, 214], [4, 259], [4, 304], [4, 349], [6, 25], [6, 70], [6, 115], [6, 160], [6, 205], [6, 250], [6, 295], [6, 340], [8, 16], [8, 61], [8, 106], [8, 151], [8, 196], [8, 241], [8, 286], [8, 331], [5, 30], [5, 75], [5, 120], [5, 165], [5, 210], [5, 255], [5, 300], [5, 345], [7, 21], [7, 66], [7, 111], [7, 156], [7, 201], [7, 246], [7, 291], [7, 336], [4, 35], [4, 80], [4, 125], [4, 170], [4, 215], [4, 260], [4, 305], [4, 350], [6, 26], [6, 71], [6, 116], [6, 161], [6, 206], [6, 251], [6, 296], [6, 341], [8, 17], [8, 62], [8, 107], [8, 152], [8, 197], [8, 242], [8, 287], [8, 332], [5, 31], [5, 76], [5, 121], [5, 166], [5, 211], [5, 256], [5, 301], [5, 346], [7, 22], [7, 67], [7, 112], [7, 157], [7, 202], [7, 247], [7, 292], [7, 337], [4, 36], [4, 81], [4, 126], [4, 171], [4, 216], [4, 261], [4, 306], [4, 351], [6, 27], [6, 72], [6, 117], [6, 162], [6, 207], [6, 252], [6, 297], [6, 342], [8, 18], [8, 63], [8, 108], [8, 153], [8, 198], [8, 243], [8, 288], [8, 333], [5, 32], [5, 77], [5, 122], [5, 167], [5, 212], [5, 257], [5, 302], [5, 347], [7, 23], [7, 68], [7, 113], [7, 158], [7, 203], [7, 248], [7, 293], [7, 338], [6, 28], [6, 73], [6, 118], [6, 163], [6, 208], [6, 253], [6, 298], [6, 343], [8, 19], [8, 64], [8, 109], [8, 154], [8, 199], [8, 244], [8, 289], [8, 334], [5, 33], [5, 78], [5, 123], [5, 168], [5, 213], [5, 258], [5, 303], [5, 348], [7, 24], [7, 69], [7, 114], [7, 159], [7, 204], [7, 249], [7, 294], [7, 339], [6, 29], [6, 74], [6, 119], [6, 164], [6, 209], [6, 254], [6, 299], [6, 344], [8, 20], [8, 65], [8, 110], [8, 155], [8, 200], [8, 245], [8, 290], [8, 335], [5, 34], [5, 79], [5, 124], [5, 169], [5, 214], [5, 259], [5, 304], [5, 349], [7, 25], [7, 70], [7, 115], [7, 160], [7, 205], [7, 250], [7, 295], [7, 340], [6, 30], [6, 75], [6, 120], [6, 165], [6, 210], [6, 255], [6, 300], [6, 345], [8, 21], [8, 66], [8, 111], [8, 156], [8, 201], [8, 246], [8, 291], [8, 336], [5, 35], [5, 80], [5, 125], [5, 170], [5, 215], [5, 260], [5, 305], [5, 350], [7, 26], [7, 71], [7, 116], [7, 161], [7, 206], [7, 251], [7, 296], [7, 341], [6, 31], [6, 76], [6, 121], [6, 166], [6, 211], [6, 256], [6, 301], [6, 346], [8, 22], [8, 67], [8, 112], [8, 157], [8, 202], [8, 247], [8, 292], [8, 337], [5, 36], [5, 81], [5, 126], [5, 171], [5, 216], [5, 261], [5, 306], [5, 351], [7, 27], [7, 72], [7, 117], [7, 162], [7, 207], [7, 252], [7, 297], [7, 342], [6, 32], [6, 77], [6, 122], [6, 167], [6, 212], [6, 257], [6, 302], [6, 347], [8, 23], [8, 68], [8, 113], [8, 158], [8, 203], [8, 248], [8, 293], [8, 338], [7, 28], [7, 73], [7, 118], [7, 163], [7, 208], [7, 253], [7, 298], [7, 343], [6, 33], [6, 78], [6, 123], [6, 168], [6, 213], [6, 258], [6, 303], [6, 348], [8, 24], [8, 69], [8, 114], [8, 159], [8, 204], [8, 249], [8, 294], [8, 339], [7, 29], [7, 74], [7, 119], [7, 164], [7, 209], [7, 254], [7, 299], [7, 344], [6, 34], [6, 79], [6, 124], [6, 169], [6, 214], [6, 259], [6, 304], [6, 349], [8, 25], [8, 70], [8, 115], [8, 160], [8, 205], [8, 250], [8, 295], [8, 340], [7, 30], [7, 75], [7, 120], [7, 165], [7, 210], [7, 255], [7, 300], [7, 345], [6, 35], [6, 80], [6, 125], [6, 170], [6, 215], [6, 260], [6, 305], [6, 350], [8, 26], [8, 71], [8, 116], [8, 161], [8, 206], [8, 251], [8, 296], [8, 341], [7, 31], [7, 76], [7, 121], [7, 166], [7, 211], [7, 256], [7, 301], [7, 346], [6, 36], [6, 81], [6, 126], [6, 171], [6, 216], [6, 261], [6, 306], [6, 351], [8, 27], [8, 72], [8, 117], [8, 162], [8, 207], [8, 252], [8, 297], [8, 342], [7, 32], [7, 77], [7, 122], [7, 167], [7, 212], [7, 257], [7, 302], [7, 347], [8, 28], [8, 73], [8, 118], [8, 163], [8, 208], [8, 253], [8, 298], [8, 343], [7, 33], [7, 78], [7, 123], [7, 168], [7, 213], [7, 258], [7, 303], [7, 348], [8, 29], [8, 74], [8, 119], [8, 164], [8, 209], [8, 254], [8, 299], [8, 344], [7, 34], [7, 79], [7, 124], [7, 169], [7, 214], [7, 259], [7, 304], [7, 349], [8, 30], [8, 75], [8, 120], [8, 165], [8, 210], [8, 255], [8, 300], [8, 345], [7, 35], [7, 80], [7, 125], [7, 170], [7, 215], [7, 260], [7, 305], [7, 350], [8, 31], [8, 76], [8, 121], [8, 166], [8, 211], [8, 256], [8, 301], [8, 346], [7, 36], [7, 81], [7, 126], [7, 171], [7, 216], [7, 261], [7, 306], [7, 351], [8, 32], [8, 77], [8, 122], [8, 167], [8, 212], [8, 257], [8, 302], [8, 347], [8, 33], [8, 78], [8, 123], [8, 168], [8, 213], [8, 258], [8, 303], [8, 348], [8, 34], [8, 79], [8, 124], [8, 169], [8, 214], [8, 259], [8, 304], [8, 349], [8, 35], [8, 80], [8, 125], [8, 170], [8, 215], [8, 260], [8, 305], [8, 350], [0, 37], [0, 82], [0, 127], [0, 172], [0, 217], [0, 262], [0, 307], [0, 352], [8, 36], [8, 81], [8, 126], [8, 171], [8, 216], [8, 261], [8, 306], [8, 351], [0, 38], [0, 83], [0, 128], [0, 173], [0, 218], [0, 263], [0, 308], [0, 353], [1, 37], [1, 82], [1, 127], [1, 172], [1, 217], [1, 262], [1, 307], [1, 352], [0, 39], [0, 84], [0, 129], [0, 174], [0, 219], [0, 264], [0, 309], [0, 354], [1, 38], [1, 83], [1, 128], [1, 173], [1, 218], [1, 263], [1, 308], [1, 353], [2, 37], [2, 82], [2, 127], [2, 172], [2, 217], [2, 262], [2, 307], [2, 352], [0, 40], [0, 85], [0, 130], [0, 175], [0, 220], [0, 265], [0, 310], [0, 355], [3, 37], [3, 82], [3, 127], [3, 172], [3, 217], [3, 262], [3, 307], [3, 352], [1, 39], [1, 84], [1, 129], [1, 174], [1, 219], [1, 264], [1, 309], [1, 354], [2, 38], [2, 83], [2, 128], [2, 173], [2, 218], [2, 263], [2, 308], [2, 353], [0, 41], [0, 86], [0, 131], [0, 176], [0, 221], [0, 266], [0, 311], [0, 356], [2, 39], [2, 84], [2, 129], [2, 174], [2, 219], [2, 264], [2, 309], [2, 354], [1, 40], [1, 85], [1, 130], [1, 175], [1, 220], [1, 265], [1, 310], [1, 355], [3, 38], [3, 83], [3, 128], [3, 173], [3, 218], [3, 263], [3, 308], [3, 353], [4, 37], [4, 82], [4, 127], [4, 172], [4, 217], [4, 262], [4, 307], [4, 352], [0, 42], [0, 87], [0, 132], [0, 177], [0, 222], [0, 267], [0, 312], [0, 357], [1, 41], [1, 86], [1, 131], [1, 176], [1, 221], [1, 266], [1, 311], [1, 356], [2, 40], [2, 85], [2, 130], [2, 175], [2, 220], [2, 265], [2, 310], [2, 355], [3, 39], [3, 84], [3, 129], [3, 174], [3, 219], [3, 264], [3, 309], [3, 354], [4, 38], [4, 83], [4, 128], [4, 173], [4, 218], [4, 263], [4, 308], [4, 353], [5, 37], [5, 82], [5, 127], [5, 172], [5, 217], [5, 262], [5, 307], [5, 352], [0, 43], [0, 88], [0, 133], [0, 178], [0, 223], [0, 268], [0, 313], [0, 358], [1, 42], [1, 87], [1, 132], [1, 177], [1, 222], [1, 267], [1, 312], [1, 357], [2, 41], [2, 86], [2, 131], [2, 176], [2, 221], [2, 266], [2, 311], [2, 356], [3, 40], [3, 85], [3, 130], [3, 175], [3, 220], [3, 265], [3, 310], [3, 355], [4, 39], [4, 84], [4, 129], [4, 174], [4, 219], [4, 264], [4, 309], [4, 354], [5, 38], [5, 83], [5, 128], [5, 173], [5, 218], [5, 263], [5, 308], [5, 353], [0, 44], [0, 89], [0, 134], [0, 179], [0, 224], [0, 269], [0, 314], [0, 359], [6, 37], [6, 82], [6, 127], [6, 172], [6, 217], [6, 262], [6, 307], [6, 352], [1, 43], [1, 88], [1, 133], [1, 178], [1, 223], [1, 268], [1, 313], [1, 358], [2, 42], [2, 87], [2, 132], [2, 177], [2, 222], [2, 267], [2, 312], [2, 357], [3, 41], [3, 86], [3, 131], [3, 176], [3, 221], [3, 266], [3, 311], [3, 356], [4, 40], [4, 85], [4, 130], [4, 175], [4, 220], [4, 265], [4, 310], [4, 355], [5, 39], [5, 84], [5, 129], [5, 174], [5, 219], [5, 264], [5, 309], [5, 354], [6, 38], [6, 83], [6, 128], [6, 173], [6, 218], [6, 263], [6, 308], [6, 353], [1, 44], [1, 89], [1, 134], [1, 179], [1, 224], [1, 269], [1, 314], [1, 359], [7, 37], [7, 82], [7, 127], [7, 172], [7, 217], [7, 262], [7, 307], [7, 352], [2, 43], [2, 88], [2, 133], [2, 178], [2, 223], [2, 268], [2, 313], [2, 358], [3, 42], [3, 87], [3, 132], [3, 177], [3, 222], [3, 267], [3, 312], [3, 357], [4, 41], [4, 86], [4, 131], [4, 176], [4, 221], [4, 266], [4, 311], [4, 356], [5, 40], [5, 85], [5, 130], [5, 175], [5, 220], [5, 265], [5, 310], [5, 355], [6, 39], [6, 84], [6, 129], [6, 174], [6, 219], [6, 264], [6, 309], [6, 354], [7, 38], [7, 83], [7, 128], [7, 173], [7, 218], [7, 263], [7, 308], [7, 353], [2, 44], [2, 89], [2, 134], [2, 179], [2, 224], [2, 269], [2, 314], [2, 359], [8, 37], [8, 82], [8, 127], [8, 172], [8, 217], [8, 262], [8, 307], [8, 352], [3, 43], [3, 88], [3, 133], [3, 178], [3, 223], [3, 268], [3, 313], [3, 358], [4, 42], [4, 87], [4, 132], [4, 177], [4, 222], [4, 267], [4, 312], [4, 357], [5, 41], [5, 86], [5, 131], [5, 176], [5, 221], [5, 266], [5, 311], [5, 356], [6, 40], [6, 85], [6, 130], [6, 175], [6, 220], [6, 265], [6, 310], [6, 355], [7, 39], [7, 84], [7, 129], [7, 174], [7, 219], [7, 264], [7, 309], [7, 354], [8, 38], [8, 83], [8, 128], [8, 173], [8, 218], [8, 263], [8, 308], [8, 353], [3, 44], [3, 89], [3, 134], [3, 179], [3, 224], [3, 269], [3, 314], [3, 359], [4, 43], [4, 88], [4, 133], [4, 178], [4, 223], [4, 268], [4, 313], [4, 358], [5, 42], [5, 87], [5, 132], [5, 177], [5, 222], [5, 267], [5, 312], [5, 357], [6, 41], [6, 86], [6, 131], [6, 176], [6, 221], [6, 266], [6, 311], [6, 356], [7, 40], [7, 85], [7, 130], [7, 175], [7, 220], [7, 265], [7, 310], [7, 355], [8, 39], [8, 84], [8, 129], [8, 174], [8, 219], [8, 264], [8, 309], [8, 354], [4, 44], [4, 89], [4, 134], [4, 179], [4, 224], [4, 269], [4, 314], [4, 359], [5, 43], [5, 88], [5, 133], [5, 178], [5, 223], [5, 268], [5, 313], [5, 358], [6, 42], [6, 87], [6, 132], [6, 177], [6, 222], [6, 267], [6, 312], [6, 357], [7, 41], [7, 86], [7, 131], [7, 176], [7, 221], [7, 266], [7, 311], [7, 356], [8, 40], [8, 85], [8, 130], [8, 175], [8, 220], [8, 265], [8, 310], [8, 355], [5, 44], [5, 89], [5, 134], [5, 179], [5, 224], [5, 269], [5, 314], [5, 359], [6, 43], [6, 88], [6, 133], [6, 178], [6, 223], [6, 268], [6, 313], [6, 358], [7, 42], [7, 87], [7, 132], [7, 177], [7, 222], [7, 267], [7, 312], [7, 357], [8, 41], [8, 86], [8, 131], [8, 176], [8, 221], [8, 266], [8, 311], [8, 356], [6, 44], [6, 89], [6, 134], [6, 179], [6, 224], [6, 269], [6, 314], [6, 359], [7, 43], [7, 88], [7, 133], [7, 178], [7, 223], [7, 268], [7, 313], [7, 358], [8, 42], [8, 87], [8, 132], [8, 177], [8, 222], [8, 267], [8, 312], [8, 357], [7, 44], [7, 89], [7, 134], [7, 179], [7, 224], [7, 269], [7, 314], [7, 359], [8, 43], [8, 88], [8, 133], [8, 178], [8, 223], [8, 268], [8, 313], [8, 358], [8, 44], [8, 89], [8, 134], [8, 179], [8, 224], [8, 269], [8, 314], [8, 359]] \ No newline at end of file diff --git a/research/staged-fourth-mixture-ceiling/source4088/owner/PR4085-PROFILE.json b/research/staged-fourth-mixture-ceiling/source4088/owner/PR4085-PROFILE.json new file mode 100644 index 000000000..8f342d307 --- /dev/null +++ b/research/staged-fourth-mixture-ceiling/source4088/owner/PR4085-PROFILE.json @@ -0,0 +1,9 @@ +{ + "1": 8057880, + "2": 2310120, + "3": 748602, + "4": 330480, + "5": 66690, + "8": 25920, + "48": 138438 +} diff --git a/research/staged-fourth-mixture-ceiling/source4088/owner/TEMPLATE.json.gz b/research/staged-fourth-mixture-ceiling/source4088/owner/TEMPLATE.json.gz new file mode 100644 index 000000000..114808c32 Binary files /dev/null and b/research/staged-fourth-mixture-ceiling/source4088/owner/TEMPLATE.json.gz differ diff --git a/research/staged-fourth-mixture-ceiling/source4088/price.py b/research/staged-fourth-mixture-ceiling/source4088/price.py new file mode 100644 index 000000000..373d396a1 --- /dev/null +++ b/research/staged-fourth-mixture-ceiling/source4088/price.py @@ -0,0 +1,34 @@ +"""Rational certificate for the complete mixed profile; inherited enclosure engine. + +Cinna Davis with OpenAI Codex assistance, Apache-2.0. PR3945/4076 +logarithm and exponential interval arithmetic is imported unchanged. +""" +from fractions import Fraction as Q +import json,sys +from verify import P,read,need,pins,reject +from vendor import exact_root as E + +def main(): + pins();r=read(P/'RESULT.json');profile={int(k):n for k,n in r['profile'].items()} + lower,upper=Q(r['root_lower']),Q(r['root_upper']) + ml,mh=E.certify_bracket(profile,lower,upper) + need([list(map(str,x)) for x in [ml,mh]]==[r['lower_moment_interval'],r['upper_moment_interval']],'recorded rational signs') + predecessor={int(k):n for k,n in read(P/'owner/PR4085-PROFILE.json').items()} + pl,pu=Q(r['predecessor_lower']),Q(r['predecessor_upper']) + E.certify_bracket(predecessor,pl,pu) + claim=read(P/'inputs/PR4085-CLAIM.json')['complex_supplier'] + need(claim['profile']=={str(k):v for k,v in predecessor.items()} and Q(claim['lower'])==pl and Q(claim['upper'])==pu,'pinned PR4085 price') + need(pl==Q('.001730970419199163702738') and pu==Q('.001730970419199163702739'),'PR4085 predecessor bracket') + endpoint=lower-Q(1,10**46)-Q(1,10**70) + need(Q(r['conditional_kappa'])==endpoint and endpoint>pu,'strict conditional improvement') + need(Q(r['gain_lower_bound'])==endpoint-pu,'gain lower bound') + need(E.moment(E.signed(profile),endpoint)[1]<0,'padded endpoint') + need(sum(k*v for k,v in profile.items())==65088*360,'profile mass') + out=[] + if '--controls' in sys.argv: + bad=dict(profile);bad[1]+=1 + out.append(reject('unpaid_extra_rank1',lambda:E.certify_bracket(bad,lower,upper))) + out.append(reject('old_fill_at_new_root',lambda:E.certify_bracket(predecessor,lower,upper))) + out.append(reject('unsupported_endpoint',lambda:E.certify_bracket(profile,lower+Q(1,10**12),upper+Q(1,10**12)))) + print(json.dumps({'status':'PASS_MIXED_EXACT_ROOT','root_bracket':[r['root_lower_decimal'],r['root_upper_decimal']],'conditional_kappa':str(endpoint),'gain_lower_bound':r['gain_lower_bound'],'controls':out},sort_keys=True)) +if __name__=='__main__':main() diff --git a/research/staged-fourth-mixture-ceiling/source4088/vendor/exact_root.py b/research/staged-fourth-mixture-ceiling/source4088/vendor/exact_root.py new file mode 100644 index 000000000..96dab46ab --- /dev/null +++ b/research/staged-fourth-mixture-ceiling/source4088/vendor/exact_root.py @@ -0,0 +1,119 @@ +"""Independent rational moment certificate for the staged-entry final profile. + +Comparison: PR3945 (Dugongue), root bracket [0.001730663236534549309146, 0.001730663236534549309147]. +Rational log/exp enclosures are PR3945's checks/exact_root.py, unchanged (Dugongue, OpenAI Codex assisted). +Adaptation: Rohan Arun with Anthropic Claude assistance. Apache-2.0. +""" +from fractions import Fraction as Q +from functools import lru_cache +from decimal import Decimal as D,localcontext +from pathlib import Path +import math,json,sys + +OLD_PROFILE={1:8041680,2:2306880,3:729648,4:353160,5:69120,8:25920,48:137952} +FULL_PROFILE={1:8061120,2:2313360,3:745362,4:330480,5:66690,8:25920,48:138438} +LOCAL_DELTA={1:6,2:2,3:5,4:-7} +IDLE_DELTA={3:-486,5:-2430,48:486} +COPIES=3240 +REPLICAS=360 +LOWER=Q('0.001730809033576552081734') +UPPER=Q('0.001730809033576552081735') +OUTER_LOWER=LOWER-Q(1,10**46)-Q(1,10**70) +PREDECESSOR_LOWER=Q('0.001730663236534549309146') +PREDECESSOR_UPPER=Q('0.001730663236534549309147') +PACKAGE=Path(__file__).resolve().parent.parent + +def need(ok,why): + if not ok:raise ValueError(why) + +def outward(lo,hi,digits=60): + scale=10**digits + lower=(lo.numerator*scale)//lo.denominator + upper=-((-hi.numerator*scale)//hi.denominator) + return Q(lower,scale),Q(upper,scale) + +@lru_cache(None) +def logs(rank): + need(type(rank) is int and 1<=rank<=73,'rank range') + def small(x): + z=(x-1)/(x+1);N=120 + S=2*sum((z**(2*j+1)/Q(2*j+1) for j in range(N)),Q()) + tail=2*z**(2*N+1)/(Q(2*N+1)*(1-z*z)) + return S,S+tail + e=rank.bit_length()-1;a,b=small(Q(rank,1<=0 else u);hi+=n*(u if n>=0 else l) + return outward(lo,hi) + +def signed(profile):return {**profile,73:-896*REPLICAS} + +def certify_bracket(profile,lower=LOWER,upper=UPPER): + need(lower0 and rank<73 for rank,n in profile.items()),'positive normalized monotonicity') + return ml,mh + +def controls(): + outcomes=[] + def reject(label,fn): + try:fn() + except ValueError:outcomes.append(label);return + raise ValueError('mutation was accepted: '+label) + wrong=dict(FULL_PROFILE);wrong[1]+=1 + reject('one wrong aggregate rank1 count',lambda:certify_bracket(wrong)) + wrong=dict(FULL_PROFILE) + for r,n in IDLE_DELTA.items():wrong[r]-=n + wrong[1]+=sum(r*n for r,n in IDLE_DELTA.items()) + reject('idle change replaced by rank-1 cells',lambda:certify_bracket(wrong)) + shift=Q(1,10**12) + reject('unsupported larger endpoint',lambda:certify_bracket(FULL_PROFILE,LOWER+shift,UPPER+shift)) + reject('PR3945 profile at the new bracket',lambda:certify_bracket(OLD_PROFILE)) + return outcomes + +def main(): + owner={int(rank):n for rank,n in json.loads((PACKAGE/'owner/PROFILE.json').read_text(encoding='utf8')).items()} + need(owner==FULL_PROFILE,'owner profile and independent exact profile differ') + expected=dict(OLD_PROFILE) + for rank,n in LOCAL_DELTA.items():expected[rank]+=COPIES*n + for rank,n in IDLE_DELTA.items():expected[rank]+=n + need(expected==FULL_PROFILE,'literal aggregate profile assembly') + need(sum(r*n for r,n in LOCAL_DELTA.items())==-3 and sum(r*n for r,n in IDLE_DELTA.items())==3*COPIES,'three width units move from paid local cells to idle') + need(COPIES==9*REPLICAS,'call multiplicity') + old_lo,old_hi=moment(signed(OLD_PROFILE),PREDECESSOR_LOWER),moment(signed(OLD_PROFILE),PREDECESSOR_UPPER) + need(old_lo[1]<0PREDECESSOR_UPPER,'strict endpoint improvement after inherited padding') + ml,mh=certify_bracket(FULL_PROFILE) + padded_moment=moment(signed(FULL_PROFILE),OUTER_LOWER) + need(padded_moment[1]<0,'padded lower endpoint moment') + with localcontext() as ctx: + ctx.prec=100 + decimal_lower=format(D(LOWER.numerator)/D(LOWER.denominator),'.24f') + decimal_upper=format(D(UPPER.numerator)/D(UPPER.denominator),'.24f') + outer=format(D(OUTER_LOWER.numerator)/D(OUTER_LOWER.denominator),'.70f') + print(json.dumps({'status':'PASS_EXACT_PROFILE_ROOT','full_profile':FULL_PROFILE,'owner_profile_matches':True,'comparison_count':896*REPLICAS,'comparison_rank':73, + 'root_lower':str(LOWER),'root_upper':str(UPPER),'lower_decimal':decimal_lower,'upper_decimal':decimal_upper,'outer_lower':str(OUTER_LOWER),'outer_lower_decimal':outer, + 'pr3945_root_bracket':[str(PREDECESSOR_LOWER),str(PREDECESSOR_UPPER)],'pr3945_bracket_moments':[list(map(str,old_lo)),list(map(str,old_hi))], + 'gain_over_pr3945_upper_at_least':str(OUTER_LOWER-PREDECESSOR_UPPER),'lower_moment_interval':list(map(str,ml)),'upper_moment_interval':list(map(str,mh)), + 'rejected_controls':controls() if '--controls' in sys.argv else [], + 'scope':'Exact paid-profile comparison. Native phases, literal owner fill and inherited outer theorem hypotheses are checked by the package replay.'},sort_keys=True)) + +if __name__=='__main__':main() diff --git a/research/staged-fourth-mixture-ceiling/source_binding.py b/research/staged-fourth-mixture-ceiling/source_binding.py new file mode 100644 index 000000000..ce7d283c0 --- /dev/null +++ b/research/staged-fourth-mixture-ceiling/source_binding.py @@ -0,0 +1,146 @@ +"""Bind the pooled cost model to the exact PR4088 source subset. + +Ross Richardson with substantial OpenAI Codex assistance, Apache-2.0. +The unchanged predecessor binary-frame ledger is re-executed and credited; +this is a local cost extraction, not a native or dirty-state replay. +""" +from collections import Counter +from copy import deepcopy +import argparse +import gzip +import hashlib +import json +from pathlib import Path +import runpy + +P = Path(__file__).resolve().parent +SOURCE_HEAD = "76088d49e3ed4142a958659aa996b0ca4da5e88e" +THREE = {1: 2487, 2: 713, 3: 224, 4: 102, 5: 20, 8: 8} +DELTA = {1: 2, 3: 3, 4: -3} + + +def need(condition, message): + if not condition: + raise ValueError(message) + + +def read(path): + data = path.read_bytes() + return json.loads(gzip.decompress(data) if path.suffix == ".gz" else data) + + +def check_bytes(package=P, overrides=None): + exports = read(package / "SOURCE-EXPORT.json") + need(exports["source_head"] == SOURCE_HEAD, "wrong predecessor head") + rows = exports["files"] + need(len(rows) == 14, "source subset coverage") + need(len({row["path"] for row in rows}) == len(rows), "duplicate source path") + for row in rows: + need(row["original_head"] == SOURCE_HEAD and row["original_pr"] == 4088, + "mixed source identity") + need(row["path"].startswith("source4088/") and ".." not in Path(row["path"]).parts, + "unsafe source path") + payload = ((overrides or {}).get(row["path"]) if overrides and row["path"] in overrides + else (package / row["path"]).read_bytes()) + need(len(payload) == row["bytes"] and hashlib.sha256(payload).hexdigest() == row["sha256"], + "source bytes: " + row["path"]) + return exports + + +def order_context(order, template): + need(all(isinstance(row, list) and len(row) == 2 + and all(type(v) is int for v in row) for row in order), "call identities") + need(len(order) == len({tuple(row) for row in order}) == 3240, "call coverage") + need(set(map(tuple, order)) == {(s, r) for s in range(9) for r in range(360)}, + "current 360-replica order") + times = {tuple(row): t for t, row in enumerate(order)} + need(all(times[s, r] < times[s + 1, r] for s in range(8) for r in range(360)), + "per-replica source order") + need(template["m"] == 73, "ambient width") + child_ports = {(row["child"], row["port"]): row["rank"] + for row in template["idle_children"]} + need(len(child_ports) == len(template["idle_children"]) == 18 * 112, + "duplicate/missing child port") + need(set(child_ports) == {(c, p) for c in range(18) for p in range(112)}, + "complete child ports") + need(all(child_ports[c, p] == child_ports[c, 0] + for c in range(18) for p in range(112)), "port-dependent capacity") + bins = Counter() + # The template contains historical 37-replica material. Only its original + # child-port capacities are used; the current ORDER supplies 360 replicas. + for capacity in child_ports.values(): + bins[capacity] += 360 + need(dict(bins) == {8: 241920, 16: 161280, 32: 161280, 48: 161280}, + "current complete bin inventory") + return dict(sorted(bins.items())) + + +def bind(package=P): + exports = check_bytes(package) + source = package / "source4088" + ledger = runpy.run_path(str(source / "checks/inherited_frames.py"))["ledger"] + bills = {} + for tag in ("base", "extra"): + for variant in ("THREE", "FOUR"): + word = read(source / f"inputs/{variant}-{tag}.json.gz") + profile, inventory = ledger(word) + expected = dict(THREE) + expected_inventory = {5: 28, 6: 18, 7: 56, 8: 93, 9: 213} + if variant == "FOUR": + for rank, count in DELTA.items(): + expected[rank] += count + expected_inventory[7] += 1 + expected_inventory[8] -= 1 + need(dict(profile) == expected and dict(inventory) == expected_inventory, + "re-extracted local cost/widths") + bills[f"{variant}-{tag}"] = {"profile": dict(sorted(profile.items())), + "helper_widths": dict(sorted(inventory.items()))} + bins = order_context(read(source / "owner/ORDER.json"), + read(source / "owner/TEMPLATE.json.gz")) + need(sum(c * n for c, n in bins.items()) == 17418240, "capacity mass") + demand = {w: 3240 * n for w, n in bills["THREE-base"]["helper_widths"].items()} + need(sum(w * n for w, n in demand.items()) == 10695240, "hosted width mass") + need(sum(r * n * 3240 for r, n in THREE.items()) == 16708680, "local rank mass") + need(16708680 + 17418240 - 10695240 == 65088 * 360, "complete rank mass") + return {"status": "PASS_BOUND_SOURCE_COSTS", "source_head": SOURCE_HEAD, + "source_files": len(exports["files"]), "providers": bills, + "bins": bins, "demands_at_x0": demand, "calls": 3240, + "stock": 896 * 360, "ambient_width": 73, + "scope": "Exact source bytes and re-executed predecessor binary-frame cost ledger; " + "current order/bin extraction. Stock is the retained stipulated moment " + "normalization. No fresh native, dirty-state, owner or outer release."} + + +def controls(package=P): + rejected = [] + + def reject(name, callback): + try: + callback() + except ValueError: + rejected.append(name) + return + raise ValueError("accepted control: " + name) + + rel = "source4088/inputs/FOUR-base.json.gz" + raw = (package / rel).read_bytes() + reject("corrupted_frozen_word", lambda: check_bytes(package, {rel: bytes([raw[0] ^ 1]) + raw[1:]})) + order = read(package / "source4088/owner/ORDER.json") + template = read(package / "source4088/owner/TEMPLATE.json.gz") + reject("historical37_in_place_of_current360", lambda: order_context( + [row for row in order if row[1] < 37], template)) + bad_template = deepcopy(template) + bad_template["idle_children"][1] = bad_template["idle_children"][0] + reject("duplicate_original_child_port", lambda: order_context(order, bad_template)) + return rejected + + +if __name__ == "__main__": + parser = argparse.ArgumentParser() + parser.add_argument("--output", type=Path) + args = parser.parse_args() + result = bind() + result["rejected_controls"] = controls() + if args.output: + args.output.write_text(json.dumps(result, sort_keys=True, indent=2) + "\n") + print(json.dumps(result, sort_keys=True)) diff --git a/research/staged-fourth-mixture-ceiling/verify.py b/research/staged-fourth-mixture-ceiling/verify.py new file mode 100644 index 000000000..3a7185dbd --- /dev/null +++ b/research/staged-fourth-mixture-ceiling/verify.py @@ -0,0 +1,311 @@ +"""Exact finite pooled-pattern bound for the immutable PR4088 export. + +No optimizer is imported. Rational logarithm/exponential enclosures are loaded +unchanged from PR4088's vendor/exact_root.py (PR3945/4076 lineage). This checker +proves a relaxation, and does not claim a legal chronological/family owner fill. +Prepared with OpenAI Codex assistance. Apache-2.0. +""" +from collections import Counter +from decimal import Decimal, localcontext +from fractions import Fraction as Q +from functools import lru_cache +import argparse, gzip, hashlib, importlib.util, json, sys +from pathlib import Path + +P=Path(__file__).resolve().parent +S=P/'source4088' +W=(5,6,7,8,9) +CAPS=(8,16,32,48) +N=3240 +SOURCE_HEAD='76088d49e3ed4142a958659aa996b0ca4da5e88e' +LOWER=Q('0.001730980255989036959962') +UPPER=Q('0.001730980255989036959963') +EXPONENT_RANGE=(Q('0.00173'),Q('0.00174')) + +E=None + +def load_engine(): + global E + spec=importlib.util.spec_from_file_location('pinned_exact_root',S/'vendor/exact_root.py') + E=importlib.util.module_from_spec(spec) + old=sys.dont_write_bytecode + try: + sys.dont_write_bytecode=True + spec.loader.exec_module(E) + finally:sys.dont_write_bytecode=old + E.power_bounds=lru_cache(None)(E.power_bounds) + +def need(ok,why): + if not ok:raise ValueError(why) + +def read(rel): + raw=(S/rel).read_bytes() + return json.loads(gzip.decompress(raw) if rel.endswith('.gz') else raw) + +def rank(vectors): + pivots={} + for v in vectors: + need(type(v) is int and 0<=v<512,'binary frame vector') + while v: + p=v.bit_length()-1 + if p in pivots:v^=pivots[p] + else:pivots[p]=v;break + return len(pivots) + +def source_data(): + t=read('owner/TEMPLATE.json.gz') + counts=Counter(c['rank'] for c in t['idle_children']) + children={c['child']:c['rank'] for c in t['idle_children']} + need(counts=={8:672,16:448,32:448,48:448},'template includes all ports') + need(len(set(c['port'] for c in t['idle_children']))==112,'112 ports') + need(Counter(children.values())=={8:6,16:4,32:4,48:4},'18 child slots') + B={c:counts[c]*360 for c in CAPS} + local={};widths={} + for tag in ('base','extra'): + by_role={};origins={} + for kind in ('THREE','FOUR'): + d=read(f'inputs/{kind}-{tag}.json.gz') + origin=sorted(set(range(224,704))-set(d['removed']));origins[kind]=origin + need(len(origin)==408,'408 helper identities') + by_role[kind]={h:rank(d['helper_final'].get(str(h),[1<=0, so endpoint enclosures suffice. + """ + if not e:return Q(),Q() + if factor_a:need(sum(r*c for r,c in e.items())==0,'zero rank mass before factoring a') + low=high=Q() + for r,c in e.items(): + if factor_a: + l=(E.power_bounds(r,lo)[0]-r)/lo + h=(E.power_bounds(r,hi)[1]-r)/hi + else: + l=E.power_bounds(r,hi)[0];h=E.power_bounds(r,lo)[1] + low+=c*(l if c>0 else h);high+=c*(h if c>0 else l) + return E.outward(low,high) + +def certify_dual(which,lo,hi): + u,v=potentials(which) + zero=[];positive=[] + for cap,nn,r in patterns(): + slack=lin((1,expr(r)),(-1,u[cap]),*((-n,v[w]) for n,w in zip(nn,W))) + if not slack:zero.append((cap,list(nn),r));continue + interval=bound_expression(slack,lo,hi,True) + need(interval[0]>0,f'{which}: nonpositive pattern slack {cap,nn,r,interval}') + positive.append((interval[0],cap,list(nn),r)) + need(positive,'nontrivial feasibility') + slope=lin((1,DELTA),(1,v[7]),(-1,v[8])) + if which=='middle':need(not slope,'exact global mixture stationarity') + else: + interval=bound_expression(slope,lo,hi,True) + need(interval[1]<0 if which=='left' else interval[0]>0,'strict kink slope') + smallest=min(positive) + return {'range':list(map(str,(lo,hi))),'patterns':len(patterns()),'identically_tight':zero, + 'strict_pattern_count':len(positive),'minimum_normalized_slack_lower':str(smallest[0]), + 'minimum_normalized_slack_pattern':list(smallest[1:]), + 'capacity_dual':{str(c):{str(r):str(a) for r,a in e.items()} for c,e in u.items()}, + 'item_dual':{str(w):{str(r):str(a) for r,a in e.items()} for w,e in v.items()}, + 'slope_expression':{str(r):str(a) for r,a in slope.items()}, + 'slope_over_a_interval':list(map(str,bound_expression(slope,lo,hi,True)))} + +def primal(x): + # This is the central x=1080 integer witness, not a chronological fill. + need(x==1080,'central witness mixture') + return [(8,(0,0,0,1,0),241920), + (16,(0,0,1,0,1),161280), + (32,(0,0,0,0,3),1620), + (32,(0,0,2,0,2),10620), + (32,(0,1,0,1,2),58320), + (32,(1,0,0,0,3),90720), + (48,(0,0,0,0,0),138492), + (48,(0,0,0,0,5),22788)] + +def check_primal(rows,x,B,widths): + bins=Counter();items=Counter();idle=Counter() + for cap,nn,y in rows: + need(all(type(n) is int and n>=0 for n in nn),'whole helper pattern') + need(type(y) in (int,Q),'exact pattern multiplicity') + need(y>=0,'nonnegative pattern multiplicity') + r=cap-sum(w*n for w,n in zip(W,nn));need(r>=0,'capacity') + bins[cap]+=y + for w,n in zip(W,nn):items[w]+=y*n + if r:idle[r]+=y + need(bins==B,'bin balance') + need(items=={w:N*widths['THREE'][w]+x*((w==7)-(w==8)) for w in W},'helper balance') + return dict(sorted(idle.items())) + +def determinant(A): + A=[list(map(Q,row)) for row in A];out=Q(1) + for j in range(len(A)): + k=next((k for k in range(j,len(A)) if A[k][j]),None) + if k is None:return Q() + if k!=j:A[k],A[j]=A[j],A[k];out=-out + v=A[j][j];out*=v + for k in range(j+1,len(A)): + z=A[k][j]/v + for t in range(j+1,len(A)):A[k][t]-=z*A[j][t] + return out + +def all_mixture_witness(x): + """Affine exact relaxation witness for every real x in [0,3240].""" + x=Q(x) + need(0<=x<=N,'mixture domain') + rows=[(8,(0,0,0,1,0),Q(241920)),(16,(0,0,1,0,1),Q(161280)), + (32,(1,0,0,0,3),Q(90720))] + if x<=1080: + rows += [(32,(0,0,0,0,3),1890-x/4), + (32,(0,0,1,2,1),540-x/2), + (32,(0,0,2,0,2),9810+3*x/4), + (32,(0,1,0,1,2),Q(58320)), + (48,(0,0,0,0,0),138438+x/20), + (48,(0,0,0,0,5),22842-x/20)] + else: + rows += [(32,(0,0,0,0,3),1080+x/2), + (32,(0,0,2,0,2),10080+x/2), + (32,(0,1,0,1,2),59400-x), + (48,(0,0,0,0,0),Q(138492)), + (48,(0,0,0,0,5),23328-x/2), + (48,(0,2,0,0,4),(x-1080)/2)] + return rows + +def reject(label,fn): + try:fn() + except ValueError:return label + raise ValueError('mutation accepted: '+label) + +def controls(B,widths,rows,profile): + out=[] + out.append(reject('changed_mixture_with_unchanged_primal',lambda:check_primal(rows,1079,B,widths))) + bad=list(rows);cap,nn,y=bad[2];bad[2]=(cap,nn,y+1) + out.append(reject('one_extra_primal_pattern',lambda:check_primal(bad,1080,B,widths))) + wrong=dict(profile);wrong[1]+=1 + out.append(reject('unpaid_extra_rank1',lambda:E.certify_bracket(wrong,LOWER,UPPER))) + out.append(reject('missing_empty_pattern',lambda:need(len([v for v in patterns() if any(v[1])])==841,'empty patterns required'))) + u,v=potentials();u[8]=lin((1,u[8]),(Q(1,10),expr(1))) + slack=lin((-1,u[8]),(-1,v[8])) + out.append(reject('wrong_capacity_dual_sign',lambda:need(bound_expression(slack,UPPER,UPPER)[0]>=0,'dual feasibility'))) + return out + +def compute(): + B,local,widths=source_data();rows=primal(1080) + idle=check_primal(rows,1080,B,widths) + need(idle=={3:22788,5:1620,48:138492},'optimal idle profile') + profile=Counter(idle) + for r,n in local['THREE'].items():profile[r]+=N*n + for r,n in {1:2,3:3,4:-3}.items():profile[r]+=1080*n + profile=dict(sorted(profile.items())) + need(sum(r*n for r,n in profile.items())==65088*360,'complete paid rank mass') + ml,mh=E.certify_bracket(profile,LOWER,UPPER) + dual={} + for which in ('middle','left','right'): + dual[which]=certify_dual(which,*EXPONENT_RANGE) + # Affine identities are checked by endpoint values on each linear region; + # the written proof additionally states nonnegativity throughout the segment. + for x in map(Q,(0,1080,3240)): + check_primal(all_mixture_witness(x),x,B,widths) + u,v=potentials('left' if x<=1080 else 'right') + for cap,nn,y in all_mixture_witness(x): + r=cap-sum(w*n for w,n in zip(W,nn)) + slack=lin((1,expr(r)),(-1,u[cap]),*((-n,v[w]) for w,n in zip(W,nn))) + need(not slack,'affine witness complementary slackness') + A=[] + for c in CAPS:A.append([int(cap==c) for cap,nn,y in rows]+[0]) + for w in W:A.append([nn[W.index(w)] for cap,nn,y in rows]+[-int(w==7)+int(w==8)]) + det=determinant(A);need(det!=0,'unique active primal including x') + old=read('RESULT.json');oldlo,oldhi=Q(old['root_lower']),Q(old['root_upper']) + literal={int(r):n for r,n in old['profile'].items()} + delta=lin(*((literal.get(r,0)-profile.get(r,0),expr(r)) for r in set(literal)|set(profile))) + need(delta=={3:Q(-3),5:Q(5),16:Q(1),32:Q(2),48:Q(-2)},'literal-minus-ideal complete delta') + gap=bound_expression(delta,LOWER,UPPER,True) + need(gap[0]>0,'strict literal paid-moment gap') + sources=['owner/TEMPLATE.json.gz','inputs/THREE-base.json.gz','inputs/THREE-extra.json.gz', + 'inputs/FOUR-base.json.gz','inputs/FOUR-extra.json.gz','RESULT.json','PROOF.md','vendor/exact_root.py'] + with localcontext() as ctx: + ctx.prec=80 + decimals=[format(Decimal(q.numerator)/Decimal(q.denominator),'.24f') for q in (LOWER,UPPER)] + output={'status':'PASS_EXACT_POOLED_PATTERN_OPTIMUM','source_head':SOURCE_HEAD, + 'scope':'Optimistic pooled pattern LP; real multiplicities and x; no chronology/family constraints; no supplier or kappa claim.', + 'bin_counts':B,'calls':N,'optimum_fourth_calls':1080,'covered_exponent_range':list(map(str,EXPONENT_RANGE)), + 'primal':[{'capacity':cap,'helper_counts':dict(zip(W,nn)),'multiplicity':y, + 'residual':cap-sum(w*n for w,n in zip(W,nn))} for cap,nn,y in rows], + 'active_matrix_determinant':str(det),'idle':idle,'complete_profile':profile, + 'root_bracket':[str(LOWER),str(UPPER)],'root_decimal_bracket':decimals, + 'root_bracket_moments':[list(map(str,ml)),list(map(str,mh))], + 'dual':dual,'literal_root_bracket':[str(oldlo),str(oldhi)], + 'ideal_root_gain_over_literal_interval':[str(LOWER-oldhi),str(UPPER-oldlo)], + 'literal_minus_ideal':{r:str(c) for r,c in delta.items()}, + 'literal_minus_ideal_moment_over_a_interval':list(map(str,gap)), + 'source_sha256':{f:hashlib.sha256((S/f).read_bytes()).hexdigest() for f in sources}, + 'defect_controls':controls(B,widths,rows,profile)} + return output + +def main(): + global S + parser=argparse.ArgumentParser(description=__doc__) + parser.add_argument('--source',type=Path,default=S) + parser.add_argument('--output',type=Path,help='Write a new certificate; by default compare recomputation with RESULT.json.') + parser.add_argument('--expected',type=Path,default=P/'RESULT.json') + parser.add_argument('--controls',action='store_true',help='Accepted explicitly; defect controls always run.') + args=parser.parse_args();S=args.source.resolve();load_engine();output=compute() + if args.output:args.output.write_text(json.dumps(output,indent=2,sort_keys=True)+'\n') + else: + # JSON object keys are strings even when the exact calculation used + # integer ranks. Compare the serialized value, not Python key types. + need(json.loads(json.dumps(output))==json.loads(args.expected.read_text()), + 'recomputed exact certificate equals saved JSON value') + print(json.dumps({k:output[k] for k in ('status','covered_exponent_range','optimum_fourth_calls','idle','complete_profile', + 'active_matrix_determinant','root_bracket','ideal_root_gain_over_literal_interval')},sort_keys=True)) + +if __name__=='__main__':main()