diff --git a/reviews/d2_sharp_scalar_floor_20261006/NOTE.md b/reviews/d2_sharp_scalar_floor_20261006/NOTE.md new file mode 100644 index 000000000..8741b0c80 --- /dev/null +++ b/reviews/d2_sharp_scalar_floor_20261006/NOTE.md @@ -0,0 +1,156 @@ +# D2: a sharper scalar lower floor without moment upper inputs + +Object: D2-SHARP-SCALAR-PARTB-PUBLICATION-20261006-R5. +Scientific effect: NONE. Publication source review: PENDING. + +Dylan Roy — delegated AI work. Publication and regression author: OpenAI / +GPT-6 Astra Pro, `canonical-r5-partb-source-publication-20261006`; +pickup Math-#328/6016272882. The original mathematical observation is by +OpenAI / GPT-6 Astra Pro, `round17-continuation-audit-20261005`, Part B of +[comment 6008747995](https://github.com/d6g8k5htny-coder/Math-/pull/328#issuecomment-6008747995), +created/updated 2026-10-06T03:29:55Z. This is its separate source publication, +not a new independent discovery or an amendment to either original packet. + +The comment received a separate [PASS_SCOPED review 6016072968](https://github.com/d6g8k5htny-coder/Math-/pull/328#issuecomment-6016072968) +from OpenAI / GPT-6 Astra Pro, `canonical-r4-partb-scalar-review-20261006`, +on 2026-10-06T12:18:58Z. That review covers the exact comment argument, +not this new publication or regression file. The same conversation now +assembles this packet; no self-review or organizational independence is +claimed. A separate source-bound publication review is required. + +## 1. Sources and non-duplication + +Source A is #328's NOTE.md at commit +`31f7a6b5a36045be7795a6461da067a8ada96343`, path +`reviews/d2_two_atom_floors_20261006/NOTE.md`, blob +`cedbb44a237d1a158111dca81c30983f7efd37f1`, specifically section 5, +formula (5.1), its positive lower-input interface, and section 6's example. + +Source B is `formal/ResearchFormalCoreR1/D2Schur.lean` at commit +`2f8b6f372be383d752e9dd30d38234faa977243c`, blob +`b95460c0d263a32ea274b347079cca6aaab3d2e9`. Its scalar definitions, +`d2_schur_ratio`, and `d2_det_interpolation` provide the correspondence. +All formulas used below are stated explicitly; no running import, pending +PR merge, or older CI outcome is a proof premise. + +#326 remains the primary source for the common three moment floors under +its broader squared-radius mass premise. #328 is the individual-atom +companion with its original conservative upper-moment-free Schur bound. +The common moment floors and determinant/tau consequences are not counted +again. Neither source is replaced, edited, or globally superseded here. +The canonical crosswalk remains [6009510800](https://github.com/d6g8k5htny-coder/Math-/pull/328#issuecomment-6009510800). + +## 2. Exact scalar proposition + +Let x >= x0 > 0, g >= g0 > 0 and 0 <= t <= 1/4. Define + + D0 = x(g+x), D1 = g(g+4x)/4, + N = xg(g+2x), D(t) = (1-4t)D0 + 4tD1, + S(t) = N/D(t). + +Then D(t)>0 and + + S(t) >= H(x0,g0) + := min{g0(g0+2x0)/(g0+x0), 4x0(g0+2x0)/(g0+4x0)} + >= min{g0, 2x0}. (1) + +For the original moment application use x=s^2 and x0=s0^2, with +s>=s0>0. In source B the substitution is m2=s, m4=g+s^2 and q=t. +Thus its numerator equals N and its determinant equals D(t); its Schur +ratio identity applies because the determinant has just been proved +positive. No moment upper bounds or probabilistic independence are used. +This proposition takes lower inputs as premises; it does not re-prove +or broaden the atom-integral argument supplying those inputs. + +## 3. Proof with denominator and monotonicity directions explicit + +Both D0 and D1 are positive. The interpolation weights are nonnegative +and sum to one, including at t=0 and t=1/4. Consequently + + 0 < D(t) <= max(D0,D1), + S(t) >= N/max(D0,D1) = min{F0(x,g),F1(x,g)}, + F0(x,g) = g(g+2x)/(g+x), + F1(x,g) = 4x(g+2x)/(g+4x). + +For X>=x>0 and G>=g>0, clearing the positive denominators gives + + F0(X,g)-F0(x,g) = g^2(X-x)/((g+X)(g+x)), + F0(x,G)-F0(x,g) = (G-g)+x^2(G-g)/((G+x)(g+x)), + F1(X,g)-F1(x,g) = 2(X-x)+2g^2(X-x)/((g+4X)(g+4x)), + F1(x,G)-F1(x,g) = 8x^2(G-g)/((G+4x)(g+4x)). (2) + +Every denominator is positive and each increment is nonnegative. +Apply (2) one coordinate at a time to obtain Fi(x,g)>=Fi(x0,g0) +for i=0,1. Taking the minimum proves the first inequality in (1). +Finally, + + F0(x0,g0)-g0 = g0*x0/(g0+x0) > 0, + F1(x0,g0)-2x0 = 2*x0*g0/(g0+4*x0) > 0, + +which proves the last inequality in (1). At no point is an uncontrolled +quotient denominator replaced by a lower bound. This proof requires +neither joint attainment of the moment floors nor a new normalizer. + +## 4. Example and scope limits + +Source A's example gives s0=5/4, x0=25/16 and g0=9/8. Direct calculation +produces F0(x0,g0)=153/86 and F1(x0,g0)=425/118. Hence H=153/86, +with H/(9/8)=68/43. The example's actual g is 43/16, not g0. The +comparison uses lower inputs; the original conservative floor 9/8 +remains correct. + +The direction interval is essential. For (x,g,t)=(1,1,-1) or (1,4,1), +D(t)>0 but the asserted endpoint lower floor fails. Such directions are +outside the proposition. Strict positivity of x0,g0 is also retained. +No extension to singular inputs through total division is asserted. + +The endpoint reduction is exact for fixed positive x,g. This packet +does NOT claim global sharpness over the original constrained moment +laws, a concrete periodic/Gaussian/Palm identification, a numerical field +certificate, an elder/capture/persistence consequence, or a family-uniform +positive floor without uniform caller inputs. It adds no Lean declaration, +kernel execution, independent statement alignment, or scientific acceptance. + +## 5. Reproduction and source-review boundary + +From the repository root: + +```sh +python -B -S reviews/d2_sharp_scalar_floor_20261006/check_partb.py +python -B -O -S reviews/d2_sharp_scalar_floor_20261006/check_partb.py +python -B -S -m unittest discover -s tests -p test_d2_sharp_scalar_floor.py -v +python -B -O -S -m unittest discover -s tests -p test_d2_sharp_scalar_floor.py -v +``` + +The checker is byte-identical to the previous reviewer control script, +SHA256 `64047e54a8525cd890fcc0f400cd529a357537a901a5de792b49afb71cd669da`. +Here "independent" means no import from either original packet helper; +it does not mean an independent organization or a new review of this code. +Its ten exact polynomial coefficient identities and finite rational cases +supplement the continuum proof in section 3, not replace it. + +The new five-method regression authenticates the note, checker and itself +against SOURCES.json; requires exact successful baseline bytes; checks all +six named wrong-formula reports, exact exit codes and empty stderr; and +separately checks invalid CLI calls. Invalid-argument tests check the usage +prefix and one of two exact error suffix spellings (plain or quoted choices), +not every intermediate usage-layout byte. +The six variants are explicit checker formula variants, not source edits +to either original packet. A hash establishes identity, not trust by itself. + +Tests were first executed before the publication files existed and failed +with ten intended missing-checker/manifest assertions, zero test errors. +One initial assembled test falsely expected quoted argparse choices; actual +3.13.5 printed plain choices. Only the test presentation contract was corrected +to those two explicit spellings; the original failure is retained. +After assembly, local results and exact hosted outcomes are recorded on +the PR; this static source does not claim a future green run. Direct local +GitHub access failed DNS, so local checks use an authenticated file subset, +not a complete repository checkout or a local Lean build. Existing CI must +supply its own current-candidate results; no older receipt is rebound. + +Any publication amendment, implementation, consolidation or changed +hypothesis must expose its exact source delta and applicable review. +The comment-level PASS is not automatically a PASS of these four files. +SOURCES.json preserves the original pending publication-review annotation; +subsequent reviews belong in source-bound PR records, not silent flag edits. diff --git a/reviews/d2_sharp_scalar_floor_20261006/SOURCES.json b/reviews/d2_sharp_scalar_floor_20261006/SOURCES.json new file mode 100644 index 000000000..591a23cd3 --- /dev/null +++ b/reviews/d2_sharp_scalar_floor_20261006/SOURCES.json @@ -0,0 +1,61 @@ +{ + "schema_version": 1, + "scientific_effect": "NONE", + "publication_review_status": "PENDING_SOURCE_BOUND_REVIEW", + "object": "D2-SHARP-SCALAR-PARTB-PUBLICATION-20261006-R5", + "publication_author": "OpenAI / GPT-6 Astra Pro; canonical-r5-partb-source-publication-20261006", + "mathematical_origin": { + "repository": "d6g8k5htny-coder/Math-", + "pr": 328, + "comment_id": 6008747995, + "section": "B", + "created_at": "2026-10-06T03:29:55Z", + "updated_at": "2026-10-06T03:29:55Z" + }, + "comment_mathematical_review": { + "comment_id": 6016072968, + "verdict": "PASS_SCOPED", + "scope": "comment Part B only; not this publication code", + "performer": "OpenAI / GPT-6 Astra Pro; canonical-r4-partb-scalar-review-20261006", + "organizational_independence": 0 + }, + "sources": [ + { + "path": "reviews/d2_two_atom_floors_20261006/NOTE.md", + "commit": "31f7a6b5a36045be7795a6461da067a8ada96343", + "git_blob": "cedbb44a237d1a158111dca81c30983f7efd37f1", + "role": "sections 5 and 6; explicit scalar formulas and example, not a runtime file dependency" + }, + { + "path": "formal/ResearchFormalCoreR1/D2Schur.lean", + "commit": "2f8b6f372be383d752e9dd30d38234faa977243c", + "git_blob": "b95460c0d263a32ea274b347079cca6aaab3d2e9", + "role": "scalar formula correspondence, not new kernel evidence" + } + ], + "checker_origin": { + "delivery_sha256": "b438b906965087f2f19de7502dd925d01315768375f114dc9605bdd0c4ad0ebb", + "member": "part_b/check_partb.py", + "sha256": "64047e54a8525cd890fcc0f400cd529a357537a901a5de792b49afb71cd669da" + }, + "files": [ + { + "path": "reviews/d2_sharp_scalar_floor_20261006/NOTE.md", + "bytes": 7864, + "git_blob": "8741b0c801fb5a75e7b13a169872769a30d16015", + "sha256": "38d1c6576955e0ce1c04c6a4a3f4703430538ba039a1e21ebef249b74644f637" + }, + { + "path": "reviews/d2_sharp_scalar_floor_20261006/check_partb.py", + "bytes": 6688, + "git_blob": "cc88ad90a80279a8c3ec2d3392ccd973266e58d0", + "sha256": "64047e54a8525cd890fcc0f400cd529a357537a901a5de792b49afb71cd669da" + }, + { + "path": "tests/test_d2_sharp_scalar_floor.py", + "bytes": 5892, + "git_blob": "9e1a784930cfc1bec8ce8cf00c368a037b62d1fd", + "sha256": "30badc12c14a1360388c956b1167cd74f574e0b0c2d5f5d2c7f72cae83ddc79b" + } + ] +} diff --git a/reviews/d2_sharp_scalar_floor_20261006/check_partb.py b/reviews/d2_sharp_scalar_floor_20261006/check_partb.py new file mode 100644 index 000000000..cc88ad90a --- /dev/null +++ b/reviews/d2_sharp_scalar_floor_20261006/check_partb.py @@ -0,0 +1,143 @@ +#!/usr/bin/env python3 +"""Independent exact controls for comment6008747995 Part B (not a Lean proof). + +Standard-library polynomial coefficient identities and rational test inputs. +No import from either mathematical packet. --mutant is a deliberately wrong +review-control formula, not a modification of a repository source. +""" +from __future__ import annotations +import argparse +from fractions import Fraction as Q +import itertools +import json +import sys + +NVAR = 5 # x, g, X, G, t +class P: + def __init__(self, value=0): + self.c = ({e: Q(a) for e, a in value.items() if a} + if isinstance(value, dict) else ({(0,)*NVAR: Q(value)} if value else {})) + @staticmethod + def var(index): + e = [0]*NVAR; e[index] = 1 + return P({tuple(e): 1}) + def __add__(self, other): + other = other if isinstance(other, P) else P(other) + c = dict(self.c) + for e, a in other.c.items(): c[e] = c.get(e, Q(0)) + a + return P(c) + __radd__ = __add__ + def __neg__(self): return P({e: -a for e, a in self.c.items()}) + def __sub__(self, other): return self + -(other if isinstance(other, P) else P(other)) + def __rsub__(self, other): return P(other) + -self + def __mul__(self, other): + other = other if isinstance(other, P) else P(other) + c = {} + for e, a in self.c.items(): + for f, b in other.c.items(): + ef = tuple(i+j for i,j in zip(e,f)) + c[ef] = c.get(ef, Q(0)) + a*b + return P(c) + __rmul__ = __mul__ + def __pow__(self, n): + if type(n) is not int or n < 0: raise ValueError('nonnegative exponent required') + out = P(1) + for _ in range(n): out *= self + return out + +def f0(x,g): return g*(g+2*x)/(g+x) +def f1(x,g): return 4*x*(g+2*x)/(g+4*x) +def endpoints(x,g): return x*(g+x), g*(g+4*x)/4 +def schur(x,g,t): + d0,d1 = endpoints(x,g) + return x*g*(g+2*x)/((1-4*t)*d0+4*t*d1) +def original_schur(x,g,t): + a = g+x-2*(g-2*x)*t + c = x+2*(g-2*x)*t + d = x*(g+x)+(g-2*x)*(g+2*x)*t + return a-(c**3+(2*c+a)*(g-2*x)**2*t*(1-4*t))/d + +def run(mutant=None): + failures=[]; counts={} + def expect(ok,group): + if not ok and group not in failures: failures.append(group) + x,g,X,G,t = [P.var(i) for i in range(NVAR)] + d0 = x*(g+x); d1 = Q(1,4)*g*(g+4*x); n=x*g*(g+2*x) + d = x*(g+x)+(g-2*x)*(g+2*x)*t + a = g+x-2*(g-2*x)*t; c=x+2*(g-2*x)*t + sign = -1 if mutant=='flip_difference_sign' else 1 + factor = 2 if mutant=='omit_F1_factor_four' else 4 + identities = { + 'F0_x_difference':g*(g+2*X)*(g+x)-g*(g+2*x)*(g+X)-sign*g**2*(X-x), + 'F0_g_difference':G*(G+2*x)*(g+x)-g*(g+2*x)*(G+x)-(G-g)*(G+x)*(g+x)-x**2*(G-g), + 'F1_x_difference':4*X*(g+2*X)*(g+4*x)-4*x*(g+2*x)*(g+4*X)-2*(X-x)*(g+4*X)*(g+4*x)-2*g**2*(X-x), + 'F1_g_difference':4*x*(G+2*x)*(g+4*x)-4*x*(g+2*x)*(G+4*x)-8*x**2*(G-g), + 'determinant_interpolation':d-(1-4*t)*d0-4*t*d1, + 'original_schur_cancellation':a*d-c**3-(2*c+a)*(g-2*x)**2*t*(1-4*t)-n, + 'endpoint0':n*(g+x)-g*(g+2*x)*d0, + 'endpoint1':n*(g+4*x)-factor*x*(g+2*x)*d1, + 'dominance0':g*(g+2*x)-g*(g+x)-g*x, + 'dominance1':4*x*(g+2*x)-2*x*(g+4*x)-2*x*g, + } + for name, residual in identities.items(): expect(not residual.c,'symbolic:'+name) + counts['polynomial_identities']=len(identities) + values=[Q(1,64),Q(1,4),Q(1),Q(2),Q(9),Q(64)] + inc=[Q(0),Q(1,7),Q(2),Q(19)] + exact_count=0 + for x,g,dx,dg in itertools.product(values,values,inc,inc): + X,G=x+dx,g+dg + claims=[ + (f0(X,g)-f0(x,g),g*g*dx/((g+X)*(g+x))), + (f0(x,G)-f0(x,g),dg+x*x*dg/((G+x)*(g+x))), + (f1(X,g)-f1(x,g),2*dx+2*g*g*dx/((g+4*X)*(g+4*x))), + (f1(x,G)-f1(x,g),8*x*x*dg/((G+4*x)*(g+4*x))), + ] + for left,right in claims: + expect(left==right,'rational_differences'); exact_count+=1 + expect(left<=0 if mutant=='reverse_monotone_direction' else left>=0,'monotonicity') + counts['rational_difference_equalities']=exact_count + dirs=0; dominance=0; endpoint_min=0; original_equalities=0 + for s0,g0,dx,dg in itertools.product( + [Q(1,8),Q(1,2),Q(1),Q(5,4),Q(3),Q(8)], + [Q(1,16),Q(1,4),Q(9,8),Q(2),Q(7),Q(64)], + [Q(0),Q(1,7),Q(3)],[Q(0),Q(1,5),Q(5)]): + x0=s0*s0; x=x0+dx; g=g0+dg + supplied_x=s0 if mutant=='square_input_missing' else x0 + choice=max if mutant=='max_for_min' else min + h=choice(f0(supplied_x,g0),f1(supplied_x,g0)) + expect(h>=min(g0,2*x0),'dominance'); dominance+=1 + expect(min(schur(x,g,Q(0)),schur(x,g,Q(1,4)))==min(f0(x,g),f1(x,g)),'endpoint_min'); endpoint_min+=1 + for k in range(17): + t=Q(k,64) + d0,d1=endpoints(x,g) + expect((1-4*t)*d0+4*t*d1>0,'denominator_positivity') + expect(schur(x,g,t)>=h,'direction_floor'); dirs+=1 + expect(original_schur(x,g,t)==schur(x,g,t),'native_formula_correspondence'); original_equalities+=1 + counts.update(direction_inequalities=dirs,dominance_checks=dominance, + endpoint_minimum_checks=endpoint_min,native_formula_equalities=original_equalities) + x0,g0=Q(25,16),Q(9,8) + ex=min(f0(x0,g0),f1(x0,g0)) + target=Q(153,85 if mutant=='example_wrong_denominator' else 86) + expect(ex==target and ex/Q(9,8)==Q(68,43),'example') + # Deliberate excluded-direction inputs: denominator stays positive but claimed bound fails. + outside=[(Q(1),Q(1),Q(-1)),(Q(1),Q(4),Q(1))] + for x,g,t in outside: + d0,d1=endpoints(x,g) + expect((1-4*t)*d0+4*t*d1>0 and schur(x,g,t)