d6g8k5htny-coder · Oct 13, 2026 · Oct 6, 2026 · Oct 12, 2026 · Oct 13, 2026
@@ -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.
@@ -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"
+    }
+  ]
+}
@@ -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)<min(f0(x,g),f1(x,g)),'direction_scope_counterexample')
+    # Boundary switch g=2x must retain equality of both endpoint expressions.
+    for x in values:
+        expect(f0(x,2*x)==f1(x,2*x)==Q(8,3)*x,'equal_endpoints')
+    counts.update(example_checks=1,outside_direction_counterexamples=2,equal_endpoint_cases=len(values))
+    return {'scope':'exact algebra and finite controls for comment6008747995 Part B; not a Lean or field verdict',
+            'mutant':mutant,'counts':counts,'failures':sorted(failures),
+            'errors':[],'ok':not failures,'example_floor':str(ex),'example_gain':str(ex/Q(9,8))}
+
+def main():
+    p=argparse.ArgumentParser(description=__doc__)
+    p.add_argument('--mutant',choices=['flip_difference_sign','omit_F1_factor_four','max_for_min',
+                                      'square_input_missing','reverse_monotone_direction','example_wrong_denominator'])
+    args=p.parse_args()
+    report=run(args.mutant)
+    print(json.dumps(report,sort_keys=True,separators=(',',':')))
+    return 0 if report['ok'] else 1
+if __name__=='__main__': sys.exit(main())