diff --git a/research/t37-support-interval/METHODS.md b/research/t37-support-interval/METHODS.md new file mode 100644 index 0000000000..d4d29a6db9 --- /dev/null +++ b/research/t37-support-interval/METHODS.md @@ -0,0 +1,125 @@ +# Finite certificate methods + +These arguments justify the finite premises of the theorem in `README.md`. +They do not replace its continuum proof or establish physical feasibility. + +## Complete bin coverage + +The primary checker uses one Cartesian product for each capacity `c`. +A helper of width `w` has a count between zero and `floor(c/w)`. +Every feasible count vector lies in this product. +The total-width filter removes exactly the infeasible vectors. +Maximizing the signed price within each residual class therefore computes `u(r)` exactly. +The receipt retains a maximizing pattern for each class. + +The independent checker instead computes the largest price `D(m)` of an ordered helper sequence with total width `m`. +It starts with `D(0)=0` and marks other masses as unreachable. +Its recurrence is + +```text +D(m) = max_(w <= m, m-w reachable) [price(w)+D(m-w)]. +``` + +Every nonempty sequence has a final helper. +Removing it gives a sequence at a smaller mass. +Conversely, appending that helper constructs a sequence of mass `m`. +Induction therefore proves the recurrence for every mass through 48. + +Ordering does not change a multiset's mass or price, and every multiset has an ordering. +Thus the recurrence and Cartesian enumeration cover the same bin patterns through different states. +For each capacity, the independent checker adds its bonus to `D(c-r)` and then maximizes over capacities. +It compares all table entries and their complete rank domains with the primary receipt. + +## Integer radical enclosure + +For positive rational `x=a/d` and `b=p/q`, put `S=2^128` and + +```text +N = a^p*S^q, +D = d^p, +h = floor_root_q(floor(N/D)). +``` + +Integer bisection finds `h`. +The checker then verifies the exact inequalities + +```text +h^q*D <= N < (h+1)^q*D. +``` + +Taking positive `q`th roots proves + +```text +h/S <= x^b < (h+1)/S. +``` + +No floating operations enter this enclosure. +Signed interval arithmetic then encloses every `F_r(b)`, including negative credits. +Strictly positive lower bounds and strictly negative upper bounds determine the required signs. + +## Independent logarithm and exponential enclosure + +The independent checker uses scale `S=2^160`. +Dyadic range reduction writes each rational base as `2^k*y`, where `1<=y<2`. +It also computes an enclosure of `log(2)`. + +For `1<=y<=2`, set `z=(y-1)/(y+1)`, so `0<=z<=1/3`. +The atanh expansion gives + +```text +log(y) = 2*sum_(j>=0) z^(2*j+1)/(2*j+1). +``` + +The first 80 terms give a lower bound. +Every remaining denominator is at least 161. +A geometric sum therefore bounds the tail by + +```text +2*z^161 / (161*(1-z^2)). +``` + +All series terms and the tail are exact rational numbers. +Multiplication by `k` and addition enclose `log(x)`. +Rounding the lower endpoint down and the upper endpoint up preserves the enclosure at integer scale. +The same outward rounding encloses `b*log(x)`. + +All evaluated exponential arguments lie in `[0,4]`; an explicit guard checks this domain. +For the Taylor sum through term 90, let `L_j` and `U_j` enclose the scaled term `S*x^j/j!`. +The integer updates are + +```text +L_j = floor(L_(j-1)*lo/(S*j)), +U_j = ceil(U_(j-1)*hi/(S*j)). +``` + +Nonnegativity proves these enclosures by induction. +Starting at the constant term, summing the lower and upper terms encloses the partial sum. +The next term has upper bound `ceil(U_90*hi/(91*S))`. +Every later term ratio is at most `4/92`. +Multiplying that next-term bound by `92/88`, rounded upward, bounds the full remaining tail. + +For `00`, the denominator `48^b-1` is positive. +The checker requires a strictly positive lower endpoint before division. +It divides the numerator's lower bound by the denominator's upper bound, and conversely for the upper bound. +This encloses the normalized support expression + +```text +925*r*((48/r)^b-1)/(48^b-1) - v(r). +``` + +Its sign equals that of `F_r(b)`. +This calculation shares neither the radical enclosure nor the primary enumeration. +The separate monotone-ratio proof in `README.md` checks the step from these finite signs to the full continuum. + +## Exact premises and limits + +The primary certificate checks every noncritical attainable rank at `b=2/3`. +Both implementations independently check rank 32 at `16/25` and `13/20`. +These are sufficient premises for the analytic proof; they are not a numerical grid search. +The two implementations also check the countermodel equations. + +The proof uses the fixed inventory and inherited signed prices recorded in `README.md`. +`SOURCES.json` binds the predecessor documents and construction records consumed for those inputs. +No claim extends to changed helper widths, bin capacities, call counts, or source interfaces. +An alternative signed-price inequality could remove the relaxed countermodel from a stronger relaxation. +Thus the sharp boundary here does not establish a physical ceiling beyond the interval. diff --git a/research/t37-support-interval/README.md b/research/t37-support-interval/README.md new file mode 100644 index 0000000000..add3cd1134 --- /dev/null +++ b/research/t37-support-interval/README.md @@ -0,0 +1,247 @@ +# Sharp uniform range for the T37 owner relaxation + +**Status: mathematical research note. No new kappa.** + +PR942 certifies the T37 supporting inequality at one saving endpoint. +Concurrent PR995 extends it through `b=1/3` and exhibits failure at `b=1`. +This note determines the exact first failure and proves the sharp uniform range. +The result applies to every positive replica count and any unchanged contribution per replica from a local supplier. +It does not assume the U8 paid profile or infer physical feasibility from a relaxed profile. + +Let `b_star` be the unique positive solution of + +```text +37*(3/2)^b - 48^b - 36 = 0. +``` + +We prove `16/25 < b_star < 13/20` with exact arithmetic. +Thus `0.64 < b_star < 0.65`. +An exploratory floating calculation suggests `b_star ≈ 0.64186556`; that decimal is not a certified root enclosure. + +For every `0 < b <= b_star`, the normalized T37 remainder profile minimizes the signed-dual relaxation over all positive replica counts. +For every `b > b_star`, an explicit relaxed T16 profile has a strictly smaller normalized moment. +This latter statement is not a physical packing counterexample. +The selected saving endpoint near `0.001665` lies far inside the proved interval. + +## Fixed inventory and precise relaxation + +Retain the whole-helper widths, call count, and idle capacities of PR795/PR890/PR942. +Every replica has nine calls, with this helper inventory per call: + +```text +width: 4 5 7 8 9 +multiplicity:80 32 54 122 216 +``` + +The bin inventory per replica is: + +```text +capacity: 8 16 32 48 +multiplicity: 672 448 448 448 +``` + +A bin may contain only whole helpers, with total width at most its capacity. +The residual rank is the unused capacity. +Let `u(r)` be the largest capacity bonus plus helper price of any bin pattern with residual rank `r`. +Use the inherited integer prices and bonuses: + +```text +helper prices at widths (4,5,7,8,9): (-1,-20,-8,-2,4) +capacity bonuses at (8,16,32,48): (2,4,8,-13) +``` + +The complete enumeration contains 1,163 legal count vectors and 45 attainable residual ranks. +It gives `u(0)=0`, `u(1)=19`, `u(32)=8`, and `u(48)=-13`. +Define `v(r)=48*u(r)+13*r`, so `v(1)=925` and `v(32)=800`. + +For each positive integer `T`, define `R_T` by nonnegative integer counts `n_r` on attainable ranks satisfying: + +```text +sum n_r = 2016*T, +sum r*n_r = 14382*T, +sum v(r)*n_r >= 150*T. +``` + +Every whole-helper packing of the fixed inventory gives a point in `R_T`. +Indeed, total residual mass is `14382*T` and total actual signed price is `-3892*T`. +Since each actual bin price is at most `u(r)`, summing gives the stated credit inequality. + +The underlying totals are `48384-9*3778=14382` for residual mass and `896+9*(-532)=-3892` for signed price. +The relation `48*(-3892)+13*14382=150` verifies its direction. +The relaxation omits capacity assignments, helper multiplicities within residual classes, chronology, charts, and physical execution. +We assume no sufficiency of these constraints. + +Define + +```text +phi_b(r) = r*(73/r)^b for r>0; phi_b(0)=0, +I_b(n) = sum phi_b(r)*n_r, +L_b = (6*phi_b(1)+11086*phi_b(48))/37. +``` + +**Theorem.** For every `T>=1`, `n in R_T`, and `0= L_b`. +For `00`. +Thus `G_r` is strictly concave. +If `F_r(B)>0`, its chord from `x=1` to `x=48^B` proves `F_r(b)>0` for every `00` for every attainable `r` except `0,1,32,48`. +This covers every noncritical rank throughout `00` and `F_32(13/20)<0`. +Strict concavity in `x` and `G_32(1)=0` give exactly one further zero for `x>1`. +For completeness, the secant slope `G_32(x)/(x-1)` strictly decreases for `x>1`. +Its signs at the two certified points therefore give uniqueness and the signs on each side. +Consequently `F_32(b)>0` for `00` give + +```text +sum_(r<48) c_b(r)*n_r >= (c_b(1)/925)*sum_(r<48) v(r)*n_r + >= (150*T/925)*c_b(1). +``` + +Negative credits cause no sign reversal: the first inequality holds rank by rank, and its final multiplier is positive. +Using the fixed mass gives + +```text +I_b(n)/T = (14382/48)*phi_b(48) + sum c_b(r)*n_r/(48*T) + >= (14382/48)*phi_b(48) + (6/37)*c_b(1)/48 + = L_b. +``` + +Below `b_star`, equality forces all positive non-48 ranks to be one and forces credit equality. +The mass equation then gives the stated profile and divisibility by 37. +It belongs to `R_37`, with `n_0=63500`, `n_1=6`, and `n_48=11086`. +At the boundary, equality allows only ranks `1,32,48`, with `37*n_1+32*n_32=6*T` and the mass equation. + +Now take the relaxed T16 profile + +```text +n_0=27461, n_32=3, n_48=4792; all other n_r=0. +``` + +Its count is `32256=2016*16`, mass is `230112=14382*16`, and signed price is `-62272=-3892*16`. +It therefore lies in `R_16` and has exact credit equality. +Its difference from `L_b` has the sign of + +```text +(3/16)*c_b(32) - (6/37)*c_b(1) + = (3/16)*(c_b(32)-(800/925)*c_b(1)). +``` + +This sign is exactly the sign of `F_32(b)`. +It proves equality at the boundary and strict failure of the relaxed T37 optimum for every `b>b_star`. +We do not claim that this residual profile admits the required whole-helper packing or physical schedule. + +## Independent validation + +The primary checker enumerates Cartesian count vectors and bounds rational powers with integer roots. +It checks the root bracket, every noncritical inequality, mass, credit, and the relaxed countermodel. +Each root enclosure carries the integer inequality that proves its lower and upper bounds. + +The independent checker imports neither the primary checker nor the repository's moment engines. +It derives the bin table by a maximum-score fill recurrence. +It bounds logarithms with a rational atanh series and exponentials with outward-rounded integer arithmetic and an explicit tail bound. +It verifies the normalized ratio inequalities rather than the primary radical expressions. +Both traversals cover their complete finite domains. +[Arithmetic and coverage arguments](METHODS.md) justify their enumeration and interval bounds. + +A second analytic argument checks the continuum step. +For `00`. +Write it as the ratio of the integrals of `exp(b*t)` on `[0,A]` and `[0,L]`. +Its logarithmic derivative is the first interval's weighted mean of `t` minus the second interval's weighted mean. + +The latter mean is strictly larger because the added interval `(A,L]` lies above every point of `[0,A]`. +Apply this with `A=log(48/r)` and `L=log(48)`. +The exact endpoint checks then certify the same uniform interval and unique critical crossing. + +Re-running a receipt does not supply independent proof. +The distinct enumerations, arithmetic bounds, analytic arguments, and semantic controls address that requirement separately. +This package has no external human review or Lean proof. + +## Reproduce and scope + +```sh +python3 -B research/t37-support-interval/reproduce.py --out /absolute/new/output +``` + +Expected final line: `PASS_T37_SUPPORT_INTERVAL_REPRODUCTION`. +The command needs only the Python standard library. +Checks remain active under `-O`; the command preserves existing outputs. +The command does not run the native supplier, global controller, full invoice, or multiplication theorem. + +The contribution locates the first failure left open by PR995 and supplies an explicit relaxed competitor on the entire remaining exponent range. +It completes the parameter-domain characterization of the inherited supporting line, independently of the fixed local paid profile. +The new equality case explains the boundary's mechanism: rank 32 joins ranks one and 48. +The practical owner-search exclusion near the selected endpoint already follows from PR995; we claim no additional improvement there. +We claim no kappa improvement, new physical construction, or altered selected frontier. + +## Credit and provenance + +Chafik Boukhalfa supplies the signed prices and capacity model in PR795/PR890. +Jonathan Capalbo supplies the all-positive-replica rank-one supporting argument and T37 construction in PR942. +Hao Yan supplies the T16 owner-lift lineage. +Jeremy Kothe supplies the PR799 and U8 lineage; the retained sources also credit NewBArch and ColdWitness/icekylinx. +Joel Pulikkan's concurrent PR962 supplies a separate T37 construction and endpoint cross-check. + +Charles Bethin's PR850 proves a separate continuum theorem for the fixed T8 inventory. +It does not imply this all-replica theorem. + +Concurrent [PR995](https://github.com/CrocSwap/integer-mult-bounds/pull/995) by woklerx publishes the uniform `00,'rank32 defeats extended support')) + reject('extend strict support to b=1',lambda:first.need(first.support_bounds(32,800,Q(1))[0]>0,'rank32 defeats extended support')) + def tamper(field,value): + c=copy.deepcopy(certificate);c[field]=value + return second.check(c) + bad=copy.deepcopy(certificate['upper']);bad.pop('32') + reject('omit critical rank from primary table',lambda:tamper('upper',bad)) + bad_credit=copy.deepcopy(certificate['credits']);bad_credit['32']=799 + reject('understate critical credit',lambda:tamper('credits',bad_credit)) + reject('replace exact root bracket',lambda:tamper('root_bracket',['2/3','1'])) + bad_model=copy.deepcopy(certificate['countermodel']);bad_model['idle']['32']=2 + reject('corrupt relaxed competitor',lambda:tamper('countermodel',bad_model)) + # Nontrivial positives: both equality candidates belong to the relaxation. + first.relaxed_member({0:63500,1:6,48:11086},37,upper) + first.relaxed_member({0:27461,32:3,48:4792},16,upper) + first.need(first.support_bounds(32,800,Q(16,25))[0]>0,'lower-side support') + first.need(first.support_bounds(32,800,Q(13,20))[1]<0,'upper-side failure') + return dict(status='PASS_T37_SUPPORT_SEMANTIC_CONTROLS',rejected=rejected, + positive=['T37 belongs to relaxation','T16 competitor belongs to relaxation','critical rank supports at 16/25','critical rank defeats support at 13/20']) diff --git a/research/t37-support-interval/data/CERTIFICATE.json b/research/t37-support-interval/data/CERTIFICATE.json new file mode 100644 index 0000000000..d179a5f7ed --- /dev/null +++ b/research/t37-support-interval/data/CERTIFICATE.json @@ -0,0 +1,670 @@ +{ + "status": "PASS_SHARP_T37_SUPPORT_INTERVAL", + "bin_vectors": 1163, + "attainable_ranks": [ + 0, + 1, + 2, + 3, + 4, + 5, + 6, + 7, + 8, + 9, + 10, + 11, + 12, + 13, + 14, + 15, + 16, + 17, + 18, + 19, + 20, + 21, + 22, + 23, + 24, + 25, + 26, + 27, + 28, + 29, + 30, + 31, + 32, + 33, + 34, + 35, + 36, + 37, + 38, + 39, + 40, + 41, + 43, + 44, + 48 + ], + "upper": { + "8": 2, + "0": 0, + "1": 19, + "3": 7, + "4": 1, + "16": 4, + "7": 8, + "9": -4, + "2": 13, + "11": 9, + "6": 14, + "12": 3, + "5": 20, + "32": 8, + "23": 12, + "14": 16, + "24": 6, + "15": 10, + "25": 0, + "17": -2, + "18": -8, + "10": 15, + "27": -12, + "19": 11, + "20": 5, + "13": -3, + "22": -7, + "28": 7, + "21": -1, + "48": -13, + "39": -9, + "30": -5, + "40": -15, + "31": -11, + "41": -21, + "33": -23, + "34": -29, + "26": -6, + "43": -33, + "35": -10, + "36": -16, + "29": -24, + "38": -53, + "44": -14, + "37": -22 + }, + "credits": { + "8": 200, + "0": 0, + "1": 925, + "3": 375, + "4": 100, + "16": 400, + "7": 475, + "9": -75, + "2": 650, + "11": 575, + "6": 750, + "12": 300, + "5": 1025, + "32": 800, + "23": 875, + "14": 950, + "24": 600, + "15": 675, + "25": 325, + "17": 125, + "18": -150, + "10": 850, + "27": -225, + "19": 775, + "20": 500, + "13": 25, + "22": -50, + "28": 700, + "21": 225, + "48": 0, + "39": 75, + "30": 150, + "40": -200, + "31": -125, + "41": -475, + "33": -675, + "34": -950, + "26": 50, + "43": -1025, + "35": -25, + "36": -300, + "29": -775, + "38": -2050, + "44": -100, + "37": -575 + }, + "mass_per_replica": 14382, + "signed_price_per_replica": -3892, + "critical_equation": "37*(3/2)^b - 48^b - 36 = 0; unique positive root", + "root_bracket": [ + "16/25", + "13/20" + ], + "critical_lower_margin": "425760879763489673961756878867690335075/10633823966279326983230456482242756608", + "critical_upper_margin": "-958221815587879250222867513653641570875/5316911983139663491615228241121378304", + "noncritical_at_two_thirds": { + "2": "119260663386757216690336227474804844504325/21267647932558653966460912964485513216", + "3": "3493767808011283111060307454023243332848675/340282366920938463463374607431768211456", + "4": "1231202464517499395532427358334959283277225/85070591730234615865843651857942052864", + "5": "638556555897606433039012002990811038172775/170141183460469231731687303715884105728", + "6": "1275075162730255242520681816860402864708825/170141183460469231731687303715884105728", + "7": "3776068759723524424370390859372437685175875/340282366920938463463374607431768211456", + "8": "620705655986205547168835350599197925916475/42535295865117307932921825928971026432", + "9": "95721612500512261491376341716695951517625/5316911983139663491615228241121378304", + "10": "569501486953280077812270588596744190127925/85070591730234615865843651857942052864", + "11": "3394732788004843971278321701232891236293925/340282366920938463463374607431768211456", + "12": "1123606812721248194641687828625893625503725/85070591730234615865843651857942052864", + "13": "43589030083569744975302429217644488839075/2658455991569831745807614120560689152", + "14": "833300438952795588701085037989971945776325/170141183460469231731687303715884105728", + "15": "681826498492433993771677061618616032171775/85070591730234615865843651857942052864", + "16": "236116766005096994224743089545180616660175/21267647932558653966460912964485513216", + "17": "1204830966317705815807649152420294517289275/85070591730234615865843651857942052864", + "18": "2926274685732015045934036999776340506987975/170141183460469231731687303715884105728", + "19": "1893411924847646751024465241000553516578625/340282366920938463463374607431768211456", + "20": "364040057731747227858708076534803150940625/42535295865117307932921825928971026432", + "21": "3924953975574987116327691047771081903680125/340282366920938463463374607431768211456", + "22": "616475379383695656933969656130608606424075/42535295865117307932921825928971026432", + "23": "237104462223256322796336278735270394041575/85070591730234615865843651857942052864", + "24": "60779513235736368493131012822224154475275/10633823966279326983230456482242756608", + "25": "2936841610785442202491706303313393514045525/340282366920938463463374607431768211456", + "26": "490551765149629201127475842607199693917775/42535295865117307932921825928971026432", + "27": "2453967894723812918804189017543642835478075/170141183460469231731687303715884105728", + "28": "225692996310626779592708215098689054056625/85070591730234615865843651857942052864", + "29": "107246746018763419035648756216387632289225/5316911983139663491615228241121378304", + "30": "1425835804489177221665800447133200440849525/170141183460469231731687303715884105728", + "31": "3821242358207349018914985579252524194162675/340282366920938463463374607431768211456", + "33": "5751476417495795992427460363934706489264025/340282366920938463463374607431768211456", + "34": "3356219401168875709822669764442854977015425/170141183460469231731687303715884105728", + "35": "1342964813878298099182466278298725794231775/170141183460469231731687303715884105728", + "36": "455229319139665145997564118181662418730825/42535295865117307932921825928971026432", + "37": "574423133078639759669823793138649750612775/42535295865117307932921825928971026432", + "38": "1316446003370047920029793456239185524619275/42535295865117307932921825928971026432", + "39": "1510954319056308637322590470489107427636075/340282366920938463463374607431768211456", + "40": "307255474106716020739859174473260157341675/42535295865117307932921825928971026432", + "41": "3403158131922061801013176713893418427723525/340282366920938463463374607431768211456", + "43": "5287775013487786899449622817917989119794575/340282366920938463463374607431768211456", + "44": "310635125814455172548955579758129655672525/85070591730234615865843651857942052864" + }, + "normalized_optimum": { + "1": "6/37", + "48": "11086/37" + }, + "strict_equality_replicas": "positive multiples of 37 for 0 < b < b_star", + "countermodel": { + "replicas": 16, + "idle": { + "32": 3, + "48": 4792 + }, + "physical_feasibility": "not asserted" + }, + "scope": "Sharp parameter range of the inherited signed-dual relaxation. The continuum proof, hypotheses, and equality cases are in README.md. No new kappa, physical optimum beyond the interval, or multiplication theorem.", + "source_sha256": { + "research/complex-t37-owners/ALL-T-PROOF.md": "4c0c71ccd0afb850538af1b467e5208b7eb3edd0260fded84e02a8c01dfc868b", + "research/complex-t37-owners/PROOF.md": "09b39ad0d5f1f59f54dcff15c16640f7a7acf27e6597660acaf957b95c7e8510", + "research/complex-t37-owners/independent/all_t_bound.py": "3f8637a90baaa11ef18eab9e739d17b32fcff18fbc50c355f9ef32727a92e4f6", + "research/complex-t21-owner-bound/PROOF.md": "2aa0aa6ec1d87402138564c38749b5ca0f058c16817efdf58a2685d2d90cb417", + "research/complex-t21-owners/data/CLAIM.json": "433d7bc4a371aaffeee35c12a1db6ea974722a85b799233626e1a57dcfdcb121" + }, + "maximizing_patterns": { + "0": { + "capacity": 8, + "counts": [ + 0, + 0, + 0, + 1, + 0 + ] + }, + "1": { + "capacity": 32, + "counts": [ + 1, + 0, + 0, + 0, + 3 + ] + }, + "2": { + "capacity": 32, + "counts": [ + 1, + 0, + 0, + 1, + 2 + ] + }, + "3": { + "capacity": 16, + "counts": [ + 1, + 0, + 0, + 0, + 1 + ] + }, + "4": { + "capacity": 8, + "counts": [ + 1, + 0, + 0, + 0, + 0 + ] + }, + "5": { + "capacity": 32, + "counts": [ + 0, + 0, + 0, + 0, + 3 + ] + }, + "6": { + "capacity": 32, + "counts": [ + 0, + 0, + 0, + 1, + 2 + ] + }, + "7": { + "capacity": 16, + "counts": [ + 0, + 0, + 0, + 0, + 1 + ] + }, + "8": { + "capacity": 8, + "counts": [ + 0, + 0, + 0, + 0, + 0 + ] + }, + "9": { + "capacity": 16, + "counts": [ + 0, + 0, + 1, + 0, + 0 + ] + }, + "10": { + "capacity": 32, + "counts": [ + 1, + 0, + 0, + 0, + 2 + ] + }, + "11": { + "capacity": 32, + "counts": [ + 1, + 0, + 0, + 1, + 1 + ] + }, + "12": { + "capacity": 16, + "counts": [ + 1, + 0, + 0, + 0, + 0 + ] + }, + "13": { + "capacity": 32, + "counts": [ + 1, + 0, + 1, + 1, + 0 + ] + }, + "14": { + "capacity": 32, + "counts": [ + 0, + 0, + 0, + 0, + 2 + ] + }, + "15": { + "capacity": 32, + "counts": [ + 0, + 0, + 0, + 1, + 1 + ] + }, + "16": { + "capacity": 16, + "counts": [ + 0, + 0, + 0, + 0, + 0 + ] + }, + "17": { + "capacity": 32, + "counts": [ + 0, + 0, + 1, + 1, + 0 + ] + }, + "18": { + "capacity": 32, + "counts": [ + 0, + 0, + 2, + 0, + 0 + ] + }, + "19": { + "capacity": 32, + "counts": [ + 1, + 0, + 0, + 0, + 1 + ] + }, + "20": { + "capacity": 32, + "counts": [ + 1, + 0, + 0, + 1, + 0 + ] + }, + "21": { + "capacity": 32, + "counts": [ + 1, + 0, + 1, + 0, + 0 + ] + }, + "22": { + "capacity": 48, + "counts": [ + 0, + 0, + 0, + 1, + 2 + ] + }, + "23": { + "capacity": 32, + "counts": [ + 0, + 0, + 0, + 0, + 1 + ] + }, + "24": { + "capacity": 32, + "counts": [ + 0, + 0, + 0, + 1, + 0 + ] + }, + "25": { + "capacity": 32, + "counts": [ + 0, + 0, + 1, + 0, + 0 + ] + }, + "26": { + "capacity": 48, + "counts": [ + 1, + 0, + 0, + 0, + 2 + ] + }, + "27": { + "capacity": 32, + "counts": [ + 0, + 1, + 0, + 0, + 0 + ] + }, + "28": { + "capacity": 32, + "counts": [ + 1, + 0, + 0, + 0, + 0 + ] + }, + "29": { + "capacity": 48, + "counts": [ + 1, + 0, + 1, + 1, + 0 + ] + }, + "30": { + "capacity": 48, + "counts": [ + 0, + 0, + 0, + 0, + 2 + ] + }, + "31": { + "capacity": 48, + "counts": [ + 0, + 0, + 0, + 1, + 1 + ] + }, + "32": { + "capacity": 32, + "counts": [ + 0, + 0, + 0, + 0, + 0 + ] + }, + "33": { + "capacity": 48, + "counts": [ + 0, + 0, + 1, + 1, + 0 + ] + }, + "34": { + "capacity": 48, + "counts": [ + 0, + 0, + 2, + 0, + 0 + ] + }, + "35": { + "capacity": 48, + "counts": [ + 1, + 0, + 0, + 0, + 1 + ] + }, + "36": { + "capacity": 48, + "counts": [ + 1, + 0, + 0, + 1, + 0 + ] + }, + "37": { + "capacity": 48, + "counts": [ + 1, + 0, + 1, + 0, + 0 + ] + }, + "38": { + "capacity": 48, + "counts": [ + 0, + 2, + 0, + 0, + 0 + ] + }, + "39": { + "capacity": 48, + "counts": [ + 0, + 0, + 0, + 0, + 1 + ] + }, + "40": { + "capacity": 48, + "counts": [ + 0, + 0, + 0, + 1, + 0 + ] + }, + "41": { + "capacity": 48, + "counts": [ + 0, + 0, + 1, + 0, + 0 + ] + }, + "43": { + "capacity": 48, + "counts": [ + 0, + 1, + 0, + 0, + 0 + ] + }, + "44": { + "capacity": 48, + "counts": [ + 1, + 0, + 0, + 0, + 0 + ] + }, + "48": { + "capacity": 48, + "counts": [ + 0, + 0, + 0, + 0, + 0 + ] + } + } +} diff --git a/research/t37-support-interval/data/CONTROLS.json b/research/t37-support-interval/data/CONTROLS.json new file mode 100644 index 0000000000..5da9c65aed --- /dev/null +++ b/research/t37-support-interval/data/CONTROLS.json @@ -0,0 +1,63 @@ +{ + "status": "PASS_T37_SUPPORT_SEMANTIC_CONTROLS", + "rejected": [ + { + "name": "omit legal bin pattern count", + "reason": "complete count-vector inventory" + }, + { + "name": "inflate critical signed price", + "reason": "support anchors" + }, + { + "name": "change full-width helper price", + "reason": "support anchors" + }, + { + "name": "all rank48 countermodel omits necessary credit", + "reason": "relaxed credit" + }, + { + "name": "countermodel violates mass", + "reason": "relaxed mass" + }, + { + "name": "countermodel violates bin count", + "reason": "relaxed bin count" + }, + { + "name": "countermodel uses a fractional count", + "reason": "relaxed count domain" + }, + { + "name": "extend rank-one support to two thirds", + "reason": "rank32 defeats extended support" + }, + { + "name": "extend strict support to b=1", + "reason": "rank32 defeats extended support" + }, + { + "name": "omit critical rank from primary table", + "reason": "independent bin table" + }, + { + "name": "understate critical credit", + "reason": "credit table" + }, + { + "name": "replace exact root bracket", + "reason": "claimed bracket" + }, + { + "name": "corrupt relaxed competitor", + "reason": "countermodel coordinates" + } + ], + "positive": [ + "T37 belongs to relaxation", + "T16 competitor belongs to relaxation", + "critical rank supports at 16/25", + "critical rank defeats support at 13/20" + ] +} diff --git a/research/t37-support-interval/data/INDEPENDENT.json b/research/t37-support-interval/data/INDEPENDENT.json new file mode 100644 index 0000000000..cf4436ac26 --- /dev/null +++ b/research/t37-support-interval/data/INDEPENDENT.json @@ -0,0 +1,51 @@ +{ + "status": "PASS_INDEPENDENT_T37_SUPPORT_INTERVAL", + "method": "mass recurrence; atanh logarithm bounds; rounded exponential series; monotone ratio proof", + "attainable_residual_ranks": 45, + "noncritical_ratio_margins": { + "2": "910614487014021058092407922219206170895612174845800/1982398520566353320796088659355782055503994071353", + "3": "5001872825075355920333718799578284579480039651639300/5947195561699059962388265978067346166511982214059", + "4": "7050632426476347098015392015392430846892846082332500/5947195561699059962388265978067346166511982214059", + "5": "5485159048453231109163540889993975194950612874734450/17841586685097179887164797934202038499535946642177", + "6": "1216979138637405408079750446008287044735479650974200/1982398520566353320796088659355782055503994071353", + "7": "16218091830459819404528054131741954941640010335402750/17841586685097179887164797934202038499535946642177", + "8": "21327283943223835617791465769857992765143886345755200/17841586685097179887164797934202038499535946642177", + "9": "2923528499271715174061948968542788330268574779786675/1982398520566353320796088659355782055503994071353", + "10": "1087106782883426050725349958011416368302520603981450/1982398520566353320796088659355782055503994071353", + "11": "14580266303139705946223155020562350739429193703952325/17841586685097179887164797934202038499535946642177", + "12": "6434472685600743680380122216252620987089673969392100/5947195561699059962388265978067346166511982214059", + "13": "23963322710181401805309985433489657051973536615944700/17841586685097179887164797934202038499535946642177", + "14": "7157996266089403082488454715763694166147621841549550/17841586685097179887164797934202038499535946642177", + "15": "1301521116698309914083564742544592303538303202321225/1982398520566353320796088659355782055503994071353", + "16": "16225820608466818552050759097576804207522519897954000/17841586685097179887164797934202038499535946642177", + "17": "6899612796723498699523803915049712264601206341957700/5947195561699059962388265978067346166511982214059", + "18": "2792945349851484987214805930509631509353731026613200/1982398520566353320796088659355782055503994071353", + "19": "8132142295077052578210732705986135671630095782604775/17841586685097179887164797934202038499535946642177", + "20": "12508321139134450276734490380224356312719589486487000/17841586685097179887164797934202038499535946642177", + "21": "5619182987799917486749593556456256823634021560303625/5947195561699059962388265978067346166511982214059", + "22": "7060644248645774619063027478766212984473259584366650/5947195561699059962388265978067346166511982214059", + "23": "4073423643938213428141934343145306336590307281695275/17841586685097179887164797934202038499535946642177", + "24": "928163632406353212998408891430433441615483673931600/1982398520566353320796088659355782055503994071353", + "25": "4204546223951811710866696094656027193872214087438950/5947195561699059962388265978067346166511982214059", + "26": "16855230306501839722952920568223728476188477014971700/17841586685097179887164797934202038499535946642177", + "27": "2342158189616166097485843390700514718027348607980000/1982398520566353320796088659355782055503994071353", + "28": "3877376152361562702449927935677611598596032115217800/17841586685097179887164797934202038499535946642177", + "29": "29479761072192453575632337029917541116306662641542425/17841586685097179887164797934202038499535946642177", + "30": "4082612099831244102001837041399515232843770811356650/5947195561699059962388265978067346166511982214059", + "31": "16412110958590481223097548467201207539485780872915000/17841586685097179887164797934202038499535946642177", + "33": "8234134372286562001654601971811940750250541389089250/5947195561699059962388265978067346166511982214059", + "34": "28829705132442050693554305195380171574362699639431400/17841586685097179887164797934202038499535946642177", + "35": "3845326636857344840085104667943907869799806313507350/5947195561699059962388265978067346166511982214059", + "36": "1737951144786852140844980607336283622543411132796300/1982398520566353320796088659355782055503994071353", + "37": "19737028565108908511577543596905358979885874268480075/17841586685097179887164797934202038499535946642177", + "38": "45232740251394092819846289921456871855443787749249650/17841586685097179887164797934202038499535946642177", + "39": "2163166462032265059927617024250656508650947410526325/5947195561699059962388265978067346166511982214059", + "40": "10557217702442560984295623024065683218404977626533400/17841586685097179887164797934202038499535946642177", + "41": "356498850724919733079084235396121487238088557696950/435160650856028777735726778882976548769169430297", + "43": "7570273583845334542851123467497708693220613337896425/5947195561699059962388265978067346166511982214059", + "44": "5336670825447721320623204696071545844977079902379400/17841586685097179887164797934202038499535946642177" + }, + "critical_left_margin": "11703225948802408732796470716414486426510107065440/3189658999800995403753942496584877374963062868643", + "critical_right_margin": "-131697003528437900598534933839463168597792234845200/8317739266800098128729171411773908826997406460543", + "continuum": "The monotone-ratio argument is proved separately in README.md; no sampling substitutes for it." +} diff --git a/research/t37-support-interval/independent.py b/research/t37-support-interval/independent.py new file mode 100644 index 0000000000..c907222b5f --- /dev/null +++ b/research/t37-support-interval/independent.py @@ -0,0 +1,123 @@ +#!/usr/bin/env python3 +# SPDX-License-Identifier: Apache-2.0 +# Charles Bethin, with substantial OpenAI Codex assistance. +"""Independent fill recurrence and logarithm/exp interval certificate. + +No imports from verify.py or the repository's moment engines. The analytic +cross-check uses monotonicity of an exponential ratio, rather than the primary +proof's concavity after reparameterization. See README.md. +""" +from fractions import Fraction as Q +from functools import lru_cache +from pathlib import Path +import argparse +import json + +S=1 << 160 + +def need(ok,message): + if not ok:raise ValueError(message) + +def down(x):return x.numerator//x.denominator + +def up(x):return -((-x.numerator)//x.denominator) + +def ceil_div(a,b):return -(-a//b) + + +def bin_scores(): + # Build ordered fills, collapsing each mass by maximum attainable score. + # This visits masses, not the primary checker's Cartesian count vectors. + scores=[None]*49;scores[0]=0 + for mass in range(1,49): + choices=[] + for width,price in ((9,4),(8,-2),(7,-8),(5,-20),(4,-1)): + if mass>=width and scores[mass-width] is not None: + choices.append(scores[mass-width]+price) + if choices:scores[mass]=max(choices) + table={} + for capacity,bonus in ((48,-13),(32,8),(16,4),(8,2)): + for mass,score in enumerate(scores[:capacity+1]): + if score is not None: + rank=capacity-mass + table[rank]=max(table.get(rank,-10**9),score+bonus) + return table + + +def atanh_log(x): + need(Q(1)<=x<=Q(2),'reduced logarithm domain') + z=(x-1)/(x+1);power=z;total=Q(0) + for j in range(80): + total+=2*power/(2*j+1) + power*=z*z + tail=2*power/(161*(1-z*z)) + return total,total+tail + + +@lru_cache(None) +def log_interval(x): + x=Q(x);need(x>=1,'log domain');k=0 + while x>=2:x/=2;k+=1 + lo,hi=atanh_log(x);two_lo,two_hi=atanh_log(Q(2)) + return down(S*(lo+k*two_lo)),up(S*(hi+k*two_hi)) + + +def exp_interval(lo,hi): + need(0<=lo<=hi<=4*S,'exponential domain') + tl=tu=sl=su=S + for j in range(1,91): + tl=tl*lo//(S*j) + tu=ceil_div(tu*hi,S*j) + sl+=tl;su+=tu + # The remaining term ratios are at most 4/92. + nxt=ceil_div(tu*hi,91*S) + tail=ceil_div(nxt*92,88) + return sl,su+tail + + +def power_interval(x,b): + lo,hi=log_interval(Q(x));b=Q(b) + return exp_interval(down(b*lo),up(b*hi)) + + +def ratio_interval(rank,credit,b): + al,au=power_interval(Q(48,rank),b) + bl,bu=power_interval(Q(48),b) + need(bl>S,'positive ratio denominator') + return (925*rank*Q(al-S,bu-S)-credit, + 925*rank*Q(au-S,bl-S)-credit) + + +def check(certificate): + table=bin_scores() + need(table=={int(r):v for r,v in certificate['upper'].items()},'independent bin table') + need(set(table)==set(certificate['attainable_ranks']),'rank support') + credit={r:48*table[r]+13*r for r in table} + need(credit=={int(r):v for r,v in certificate['credits'].items()},'credit table') + margins={} + for r in sorted(table): + if r in (0,1,32,48):continue + lo,hi=ratio_interval(r,credit[r],Q(2,3)) + need(lo>0,'noncritical ratio: '+str(r)) + margins[r]=str(lo) + left=ratio_interval(32,credit[32],Q(16,25)) + right=ratio_interval(32,credit[32],Q(13,20)) + need(left[0]>0 and right[1]<0,'independent critical bracket') + need(certificate['root_bracket']==['16/25','13/20'],'claimed bracket') + need(certificate['countermodel']['replicas']==16 and certificate['countermodel']['idle']=={'32':3,'48':4792},'countermodel coordinates') + need(3*32+4792*48==14382*16 and 3*8-4792*13==-3892*16,'independent countermodel equations') + need(Q(150,925)==Q(6,37) and Q(14382,48)-Q(6,37*48)==Q(11086,37),'normalized optimum equations') + return dict(status='PASS_INDEPENDENT_T37_SUPPORT_INTERVAL',method='mass recurrence; atanh logarithm bounds; rounded exponential series; monotone ratio proof', + attainable_residual_ranks=len(table),noncritical_ratio_margins=margins, + critical_left_margin=str(left[0]),critical_right_margin=str(right[1]), + continuum='The monotone-ratio argument is proved separately in README.md; no sampling substitutes for it.') + + +def main(): + p=argparse.ArgumentParser();p.add_argument('--certificate',type=Path,required=True);p.add_argument('--out',type=Path,required=True);a=p.parse_args() + need(not a.out.exists(),'output preservation') + result=check(json.loads(a.certificate.read_text())) + a.out.write_text(json.dumps(result,indent=2)+'\n') + print(result['status']) + +if __name__=='__main__':main() diff --git a/research/t37-support-interval/reproduce.py b/research/t37-support-interval/reproduce.py new file mode 100644 index 0000000000..9660c5370e --- /dev/null +++ b/research/t37-support-interval/reproduce.py @@ -0,0 +1,28 @@ +#!/usr/bin/env python3 +# SPDX-License-Identifier: Apache-2.0 +# Charles Bethin; substantial OpenAI Codex assistance. +"""One command for the proof premises, independent model, and controls.""" +import argparse +import json +from pathlib import Path +import subprocess +import sys +import controls + +p=argparse.ArgumentParser();p.add_argument('--out',type=Path,required=True);a=p.parse_args() +a.out.mkdir(parents=True,exist_ok=False) +here=Path(__file__).resolve().parent +flags=['-O'] if sys.flags.optimize else [] +for name,args in [('verify.py',['--out',str(a.out/'CERTIFICATE.json')]), + ('independent.py',['--certificate',str(a.out/'CERTIFICATE.json'),'--out',str(a.out/'INDEPENDENT.json')])]: + subprocess.run([sys.executable,*flags,'-B',str(here/name),*args],check=True) +result=controls.run(json.loads((a.out/'CERTIFICATE.json').read_text())) +(a.out/'CONTROLS.json').write_text(json.dumps(result,indent=2)+'\n') +print(result['status'],f'negative={len(result["rejected"])} positive={len(result["positive"])}') +for name in ('CERTIFICATE.json','INDEPENDENT.json','CONTROLS.json'): + frozen=here/'data'/name + if frozen.exists(): + actual=json.dumps(json.loads((a.out/name).read_text()),sort_keys=True) + expected=json.dumps(json.loads(frozen.read_text()),sort_keys=True) + if actual!=expected:raise ValueError('committed receipt differs: '+name) +print('PASS_T37_SUPPORT_INTERVAL_REPRODUCTION') diff --git a/research/t37-support-interval/verify.py b/research/t37-support-interval/verify.py new file mode 100644 index 0000000000..28996987a7 --- /dev/null +++ b/research/t37-support-interval/verify.py @@ -0,0 +1,127 @@ +#!/usr/bin/env python3 +# SPDX-License-Identifier: Apache-2.0 +# Charles Bethin, with substantial OpenAI Codex assistance. +"""Exact finite certificates for the sharp T37 rank-one support interval. + +The continuum argument is in README.md. This program enumerates every bin +count vector and proves its finite premises with integer radical bounds. +No moment engine or producer enumeration is imported. +""" +from fractions import Fraction as Q +from itertools import product +import argparse +import hashlib +import json +from pathlib import Path + +WIDTHS=(4,5,7,8,9) +PRICES=(-1,-20,-8,-2,4) +HELPERS=(80,32,54,122,216) +CAPS=(8,16,32,48) +BINS=(672,448,448,448) +BONUSES=(2,4,8,-13) +SCALE=1 << 128 +HERE=Path(__file__).resolve().parent +ROOT=HERE.parents[1] + + +def need(ok,message): + if not ok: + raise ValueError(message) + + +def nth_root_floor(n,k): + need(n>=0 and k>=1,'root domain') + lo,hi=0,1 << ((n.bit_length()+k-1)//k) + while lo+10 and b>0,'power domain') + n=x.numerator**b.numerator*SCALE**b.denominator + d=x.denominator**b.numerator + q=nth_root_floor(n//d,b.denominator) + need(q**b.denominator*d<=n<(q+1)**b.denominator*d,'root enclosure') + return Q(q,SCALE),Q(q+1,SCALE) + + +def support_bounds(r,v,b): + # F_r(b)=925*r*((48/r)^b-1)-v*(48^b-1). + al,au=power_bounds(Q(48,r),b) + bl,bu=power_bounds(Q(48),b) + return (925*r*(al-1)-v*((bu if v>=0 else bl)-1), + 925*r*(au-1)-v*((bl if v>=0 else bu)-1)) + + +def enumerate_bins(prices=PRICES): + upper={};witness={};count=0 + for cap,bonus in zip(CAPS,BONUSES): + for vector in product(*(range(cap//w+1) for w in WIDTHS)): + fill=sum(w*n for w,n in zip(WIDTHS,vector)) + if fill>cap:continue + count+=1 + r=cap-fill + score=bonus+sum(p*n for p,n in zip(prices,vector)) + if r not in upper or score>upper[r]: + upper[r]=score;witness[r]=(cap,vector) + return upper,witness,count + + +def relaxed_member(profile,replicas,upper): + need(type(replicas) is int and replicas>0,'positive replica count') + need(all(r in upper and type(n) is int and n>=0 for r,n in profile.items()),'relaxed count domain') + need(sum(profile.values())==2016*replicas,'relaxed bin count') + need(sum(r*n for r,n in profile.items())==14382*replicas,'relaxed mass') + need(sum((48*upper[r]+13*r)*n for r,n in profile.items())>=150*replicas,'relaxed credit') + return True + + +def certify(upper,count): + need(count==1163,'complete count-vector inventory') + mass=sum(c*n for c,n in zip(CAPS,BINS))-9*sum(w*n for w,n in zip(WIDTHS,HELPERS)) + price=sum(n*p for n,p in zip(BINS,BONUSES))+9*sum(n*p for n,p in zip(HELPERS,PRICES)) + need((mass,price)==(14382,-3892),'fixed family totals') + need((upper[0],upper[1],upper[32],upper[48])==(0,19,8,-13),'support anchors') + credits={r:48*u+13*r for r,u in upper.items()} + need(48*price+13*mass==150,'credit demand') + # At b=2/3 every non-anchor rank except 32 remains strictly above support. + margins={r:support_bounds(r,credits[r],Q(2,3)) for r in upper if 00 for lo,hi in margins.values()),'noncritical rank at two thirds') + left=support_bounds(32,800,Q(16,25)) + right=support_bounds(32,800,Q(13,20)) + need(left[0]>0 and right[1]<0,'sharp root bracket') + # A relaxed countermodel, not a packing or physical construction. + alternative={32:3,48:4792} + need(sum(r*n for r,n in alternative.items())==16*mass,'alternative mass') + need(sum(upper[r]*n for r,n in alternative.items())==16*price,'alternative signed equality') + need(sum(credits[r]*n for r,n in alternative.items() if r<48)==16*150,'alternative credit equality') + need(relaxed_member({**alternative,0:27461},16,upper),'alternative zero-bin completion') + need(relaxed_member({0:63500,1:6,48:11086},37,upper),'T37 realization of relaxation') + return dict(status='PASS_SHARP_T37_SUPPORT_INTERVAL',bin_vectors=count,attainable_ranks=sorted(upper), + upper=upper,credits=credits,mass_per_replica=mass,signed_price_per_replica=price, + critical_equation='37*(3/2)^b - 48^b - 36 = 0; unique positive root', + root_bracket=['16/25','13/20'],critical_lower_margin=str(left[0]),critical_upper_margin=str(right[1]), + noncritical_at_two_thirds={r:str(x[0]) for r,x in sorted(margins.items())}, + normalized_optimum={'1':'6/37','48':'11086/37'}, + strict_equality_replicas='positive multiples of 37 for 0 < b < b_star', + countermodel=dict(replicas=16,idle=alternative,physical_feasibility='not asserted'), + scope='Sharp parameter range of the inherited signed-dual relaxation. The continuum proof, hypotheses, and equality cases are in README.md. No new kappa, physical optimum beyond the interval, or multiplication theorem.') + + +def main(): + p=argparse.ArgumentParser();p.add_argument('--out',type=Path,required=True);a=p.parse_args() + need(not a.out.exists(),'output preservation') + pins=json.loads((HERE/'SOURCES.json').read_text()) + for name,digest in pins.items():need(hashlib.sha256((ROOT/name).read_bytes()).hexdigest()==digest,'source drift: '+name) + u,w,n=enumerate_bins();result=certify(u,n) + result['source_sha256']=pins + result['maximizing_patterns']={r:dict(capacity=c,counts=v) for r,(c,v) in sorted(w.items())} + a.out.write_text(json.dumps(result,indent=2)+'\n') + print(result['status'],'bins=1163','critical_rank=32','16/25 < b_star < 13/20') + +if __name__=='__main__':main()