Exact all-direction envelope for the conditional cubic-jet variance

reviews/periodic_tau_envelope_20261005/REPORT.md

@@ -0,0 +1,202 @@
+# Exact all-direction envelope for the conditional cubic jet variance
+
+Object: PERIODIC-TAU-ENVELOPE-20261005. Author: OpenAI / GPT-6 Astra Pro,
+`periodic-tau-envelope-20261005`, continuing `lean-custody-round6-20261005`.
+Dylan Roy — delegated AI work. Scientific effect: **NONE**.
+Author-side mathematical contribution; nonauthor review pending at publication.
+This is not a Lean certificate or an independent re-audit of the input packet.
+
+## 1. Input and the specific gap addressed
+
+Math-#297 computes exact-periodic covariance tensors, then samples directions.
+Its corrected source at `d8be92076dae46f9504d279b286da0432d01e088` uses the product
+spectral cumulants to compute `tau2 = Var(t_u) - c_tG Cov(G)^{-1} c_Gt`.
+The moment/sign reconstruction in #297 comment6001649072 gives
+
+    tau(u)^2 = 6 a^3 + 9 a b sum_i u_i^4 + (c - b^2/a) sum_i u_i^6,       (1)
+
+where a=kappa_2>0, b=kappa_4, c=kappa_6, and sum_i u_i^2=1.
+Here tau(u)^2 denotes a variance, not its square root. The notation `b` in this
+report is a spectral cumulant, not the research program's birth-level mark.
+
+The result below makes the all-direction extrema of this ONE invariant exact:
+only d scalar values need be considered. It does not bound the other invariants
+in #297's maximum, the coefficient quadrature, or the error in numerical cumulants.
+The separate Frobenius-trace correction PJ-A-001 is not reopened here.
+
+## 2. Algebraic extremum theorem
+
+**Theorem T1.** Let d>=1 be an integer and A,B arbitrary real numbers. On the
+closed simplex Delta_d={x_i>=0, sum_i x_i=1}, define
+
+    F(x) = A sum_i x_i^2 + B sum_i x_i^3.
+
+Then
+
+    min_Delta F = min_{1<=m<=d} (A/m + B/m^2),
+    max_Delta F = max_{1<=m<=d} (A/m + B/m^2).                         (2)
+
+Every listed value is attained: choose m coordinates equal to 1/m and the
+remaining coordinates zero. Thus (2) is an exact range endpoint formula, not
+merely a bound. There may also be nonuniform maximizers/minimizers in degenerate
+cases; the theorem does not claim to enumerate every extremizing vector.
+
+### Proof, including boundary and degenerate cases
+
+F is continuous on the compact simplex, so it has a minimum and maximum. Take
+any one of these points and restrict to the face formed by its positive
+coordinates. It is a relative-interior extremum of that face. Let m be its
+support size. For m=1 the claimed value is A+B. For m>=2, tangent first
+variations give one common number lambda with
+
+    2 A x_i + 3 B x_i^2 = lambda                                     (3)
+
+for every positive coordinate. Tangent second variations of the diagonal
+Hessian diag(2A+6Bx_i) must be nonpositive at a maximum and nonnegative at a
+minimum. Variations used below are supported on the positive coordinates and
+have sum zero, so both signs of sufficiently small displacement stay in the face.
+
+If A=B=0 the statement is immediate. If B=0 and A!=0, (3) forces all positive
+coordinates equal, hence x_i=1/m. Now suppose B!=0. Equation (3) is quadratic:
+there can be at most two distinct positive values. One value again means 1/m.
+For two distinct values s<t, subtract (3) to obtain
+
+    2A+3B(s+t)=0.
+
+The two corresponding Hessian entries are
+
+    h_s=3B(s-t),  h_t=3B(t-s)=-h_s.                                 (4)
+
+They are opposite nonzero numbers, of equal magnitude h>0.
+
+At a local MAXIMUM the group with Hessian entry +h cannot contain two
+coordinates: varying these two by +epsilon and -epsilon gives positive second
+variation 2h. Therefore that group has exactly one coordinate. If the support
+has m>=3, the other group has n=m-1>=2 coordinates, all with entry -h. Use the
+tangent vector whose single +h coordinate is -n and whose n other coordinates
+are all +1. Its second variation is
+
+    h n^2 - h n = h n(n-1) > 0,
+
+again impossible at a maximum. At a local MINIMUM the group with entry -h must
+have one coordinate; the analogous tangent vector has second variation
+-h n(n-1)<0, likewise impossible. This argument handles either sign of B.
+
+The remaining unequal two-value case is m=2. Then s+t=1, so 2A+3B=0, and on
+that entire edge
+
+    A(s^2+t^2)+B(s^3+t^3) = A+B-(2A+3B)st = A+B.
+
+Its value is also attained at a vertex and at the equal two-support point.
+Thus an extremal value is always one of the d equal-support values. Since each
+listed value actually occurs in the simplex, both equalities in (2) follow.
+No hypothesis on the signs or nonvanishing of A and B was suppressed. QED.
+
+## 3. Conditional variance corollary and its input derivation
+
+Assume the centered stationary Gaussian field's spectral law has independent,
+identically distributed symmetric coordinates with finite sixth moment. Write
+a>0 for their variance and b,c for fourth and sixth cumulants. At a fixed point,
+let G be the full gradient and t_u the third directional derivative. All
+assertions here concern this displayed covariance structure; no construction of
+a particular Gaussian field or Palm law is being supplied.
+
+For Y=sum_i u_i xi_i and a unit vector u, the even-block moment expansion gives
+
+    E[Y^6] = 15a^3 + 15ab sum_i u_i^4 + c sum_i u_i^6,
+    E[Y^3 xi_i] = 3a^2 u_i + b u_i^3.
+
+The gradient covariance is aI. The stationary derivative sign makes Cov(t_u,G_i)
+the negative of the second expression, but the sign disappears on squaring.
+Consequently the Schur subtraction is
+
+    (1/a) sum_i (3a^2 u_i + b u_i^3)^2
+      = 9a^3 + 6ab sum_i u_i^4 + (b^2/a) sum_i u_i^6.
+
+Subtracting proves (1). For jointly Gaussian derivatives this Schur complement
+is the conditional variance given G=0; it conditions on the FULL gradient,
+not just its component parallel to u.
+
+**Corollary T2.** Under these input conditions, put
+
+    v_m = 6a^3 + 9ab/m + (c-b^2/a)/m^2,     1<=m<=d.
+
+Then min over unit u of tau(u)^2 is min_m v_m, and max is max_m v_m.
+Indeed x_i=u_i^2 maps the unit sphere ONTO Delta_d, and T1 applies. Each value
+v_m occurs at a direction with m nonzero coordinates of magnitude 1/sqrt(m),
+with arbitrary signs and coordinate permutations. This is exact for the actual
+real cumulants, not a declaration that rounded input values equal those cumulants.
+
+When v_1>0, the maximum absolute relative deviation from the axis value is
+
+    max_m |v_m/v_1 - 1|.                                            (5)
+
+Thus the direction sets listed by #297 for d=2,3,4 already contain a representative
+of every needed support size for THIS invariant. No angular grid refinement is
+needed to maximize tau(u)^2 under the product-cumulant model. One must still
+control numerical parameter error before reporting a certified numerical bound.
+
+The support sequence also has the exact adjacent-difference identity, with
+A=9ab and B=c-b^2/a:
+
+    v_m-v_{m+1} = [A m(m+1)+B(2m+1)]/[m^2(m+1)^2].                  (6)
+
+Do not compare only the axis and full diagonal: with d=3, A=1, B=-1, the maximum
+is 1/4 at support m=2, larger than the axis value 0 and full-diagonal value 2/9.
+This polynomial example is a control, not an assertion of Gaussian realization.
+
+## 4. Verification and falsification controls
+
+`envelope_check.py` evaluates (2) and T2 exactly on rational inputs, rejecting
+floats rather than silently treating a binary approximation as a certified input.
+A rational or decimal string means its exact encoded value only. The arbitrary
+real theorem is proved above, not established by finite sampling.
+
+`test_envelope.py` has 14 tests, including 17,850 rational simplex-grid comparisons
+(d=2..5), equal-support attainment, all two-level stationary candidates on its
+finite coefficient grid, the flat two-coordinate edge, equal-multiplicity
+stationary degeneracy, d=1, vanishing coefficients, sign/permutation invariance,
+and invalid inputs. A distinct finite product-spectrum oracle computes
+E[Y^6]-sum E[Y^3 xi_i]^2/a by direct atom enumeration on six rational unit
+directions, independent of the cumulant formula. The test spectrum is uniform
+on {-2,-1,1,2} in each coordinate; it is not the periodic infinite spectrum.
+
+Four intentionally wrong formulas must fail named controls:
+- M1 removes intermediate support sizes from (2).
+- M2 drops the conditional-regression term b^2/a.
+- M3 substitutes 15 for 9 in the fourth-cumulant coefficient after conditioning.
+- M4 replaces 1/m^2 by 1/m in the cubic support contribution.
+
+Run from this packet directory:
+
+```sh
+python3 -B -S -m unittest test_envelope -v
+python3 -B -O -S -m unittest test_envelope -v
+python3 -B -S envelope_check.py
+python3 -B -O -S envelope_check.py
+python3 -B -S envelope_check.py --mutant M1  # expected exit 1, likewise M2--M4
+python3 -B -S envelope_check.py --mutant BAD # expected exit 2
+```
+
+Test-first observation: both initial runs failed all14 tests at the explicit
+missing-implementation assertion. After implementation, both runs passed14/14.
+The CLI baseline passes and the four named mutants reject; invalid label exits2.
+The CI of the containing repository is separate and does not automatically run
+this new standalone script. No local or hosted Lean execution of T1/T2 is claimed.
+
+## 5. Limits and source custody
+
+This is an additive authored result, not a new scientific-status register.
+It neither edits #297 nor replaces its three slice reviews. In particular it
+makes no all-direction bound for det(V), det(A|V), or the Frobenius covariance
+trace. That tau drove the sampled combined maximum does not prove that it drives
+the combined maximum over all directions. Other invariants require their own
+analysis. No numerical coefficient enclosure, positivity theorem for arbitrary
+input cumulants, lifetime theorem, persistence-pairing result, IBA1/IBA2 closure,
+or complete formal alignment is asserted.
+
+The exact input source identities and locally recomputed payload identities are
+in SOURCES.json. The #297 source hash there is from its pinned manifest, with
+native Git blob identity read back; only the stated sections were consumed.
+The new extremum proof and diagnostic have OpenAI authorship. Independent review
+must be of these new bytes, not inferred from the earlier covariance review.

reviews/periodic_tau_envelope_20261005/SOURCES.json

@@ -0,0 +1,49 @@
+{
+  "schema": 1,
+  "object": "PERIODIC-TAU-ENVELOPE-20261005",
+  "scientific_effect": "NONE",
+  "review_status": "PENDING_NONAUTHOR_REVIEW",
+  "author": {
+    "provider": "OpenAI",
+    "model": "GPT-6 Astra Pro",
+    "session": "periodic-tau-envelope-20261005",
+    "attribution": "Dylan Roy — delegated AI work"
+  },
+  "base_commit": "90790a44c01b3a2c347fa712fbfaeed7fae1024b",
+  "sources": [
+    {
+      "repository": "d6g8k5htny-coder/Math-",
+      "commit": "d8be92076dae46f9504d279b286da0432d01e088",
+      "path": "reviews/iba1_periodic_jet_claude_20261005/periodic_jet_check.py",
+      "git_blob": "a2beeeee90abfc2988cf8f491d54ea835b23a1c5",
+      "sha256": "59b53e5c2e8fdcacc9983f705b9d301fcfcf9242ac6c4d8b7bfbcf0ada7caf9f",
+      "scope": "Product-cumulant cov/Schur definition and listed direction representatives. Hash reported by pinned SOURCE_FILES.json; native blob checked; not a full new source replay."
+    },
+    {
+      "repository": "d6g8k5htny-coder/Math-",
+      "pr": 297,
+      "comment_id": 6001649072,
+      "scope": "Earlier OpenAI-derived tau polynomial identity and covariance-sign reconstruction; source of hypothesis, not independent review of new extremum theorem."
+    }
+  ],
+  "files": [
+    {
+      "path": "REPORT.md",
+      "bytes": 10021,
+      "sha256": "5534b03a332f3a3a7980a9c5a8c40c53f3b08d3c02b387d025ed31915ad825df",
+      "git_blob": "2166869f20eb4d50249920691b90415943c4b5ff"
+    },
+    {
+      "path": "envelope_check.py",
+      "bytes": 5473,
+      "sha256": "e5150f2255e6245bb2fcee56f1c9768c57c7cdc36025472a4bdbdde8658d9e8a",
+      "git_blob": "4f1e53feec8c2c178a7a779b34276ce6c119f6d5"
+    },
+    {
+      "path": "test_envelope.py",
+      "bytes": 6373,
+      "sha256": "bdd10eba112267fec170672d33a9d323957f236a134d7b46e8732cd760be9d37",
+      "git_blob": "81f7c9dabcb74277808f6825be35491af6f380fc"
+    }
+  ]
+}

reviews/periodic_tau_envelope_20261005/envelope_check.py

@@ -0,0 +1,144 @@
+"""Exact rational consequences of REPORT.md, not a Lean or interval certificate.
+
+Run with Python's standard library, normally or under -O. Exit codes:
+0 = all finite controls pass, 1 = a named mathematical control fails,
+2 = invalid arguments. M1--M4 intentionally corrupt the tested formulas.
+"""
+import argparse
+from fractions import Fraction as F
+import itertools
+import json
+from typing import Iterable
+
+
+def exact(x: int | str | F) -> F:
+    """Reject floats: a decimal string means its exact rational value only."""
+    if isinstance(x, bool) or not isinstance(x, (int, str, F)):
+        raise TypeError('use int, Fraction, or an exact rational string')
+    return F(x)
+
+
+def dimension(d: int) -> None:
+    if isinstance(d, bool) or not isinstance(d, int):
+        raise TypeError('dimension must be an integer')
+    if d < 1:
+        raise ValueError('dimension must be positive')
+
+
+def simplex(x: Iterable[int | str | F]) -> tuple[F, ...]:
+    values = tuple(exact(t) for t in x)
+    if not values or any(t < 0 for t in values) or sum(values) != 1:
+        raise ValueError('simplex coordinates must be nonnegative and sum to one')
+    return values
+
+
+def support_values(d: int, A: int | str | F, B: int | str | F,
+                   mode: str | None = None) -> tuple[F, ...]:
+    dimension(d)
+    A, B = exact(A), exact(B)
+    values = tuple(A/m + B/(m if mode == 'M4' else m*m) for m in range(1, d+1))
+    if mode == 'M1' and d > 2:
+        return values[0], values[-1]  # deliberately omits intermediate supports
+    return values
+
+
+def envelope(d: int, A: int | str | F, B: int | str | F,
+             mode: str | None = None) -> tuple[F, F]:
+    values = support_values(d, A, B, mode)
+    return min(values), max(values)
+
+
+def polynomial(x: Iterable[int | str | F], A: int | str | F,
+               B: int | str | F) -> F:
+    x, A, B = simplex(x), exact(A), exact(B)
+    return A*sum(t*t for t in x) + B*sum(t*t*t for t in x)
+
+
+def tau_coefficients(a: int | str | F, b: int | str | F,
+                     c: int | str | F, mode: str | None = None) -> tuple[F, F]:
+    a, b, c = exact(a), exact(b), exact(c)
+    if a <= 0:
+        raise ValueError('second spectral cumulant must be positive')
+    return (15 if mode == 'M3' else 9)*a*b, c if mode == 'M2' else c-b*b/a
+
+
+def tau_polynomial(x: Iterable[int | str | F], a: int | str | F,
+                   b: int | str | F, c: int | str | F,
+                   mode: str | None = None) -> F:
+    a = exact(a)
+    A, B = tau_coefficients(a, b, c, mode)
+    return 6*a**3 + polynomial(x, A, B)
+
+
+def tau_envelope(d: int, a: int | str | F, b: int | str | F,
+                 c: int | str | F) -> tuple[F, F]:
+    a = exact(a)
+    A, B = tau_coefficients(a, b, c)
+    lo, hi = envelope(d, A, B)
+    return 6*a**3+lo, 6*a**3+hi
+
+
+def test_cumulants() -> tuple[F, F, F]:
+    atoms = (-2, -1, 1, 2)
+    a, m4, m6 = (sum(F(t)**j for t in atoms)/len(atoms) for j in (2, 4, 6))
+    return a, m4-3*a*a, m6-15*m4*a+30*a**3
+
+
+def test_directions() -> tuple[tuple[F, ...], ...]:
+    return ((F(1), F(0)), (F(3, 5), F(4, 5)),
+            (F(1), F(0), F(0)), (F(1, 3), F(2, 3), F(2, 3)),
+            (F(1, 2),)*4, (F(-1, 2), F(1, 2), F(-1, 2), F(1, 2)))
+
+
+def direct_spectral_regression(u: tuple[F, ...]) -> F:
+    """Independent finite-atom E[Y^6]-sum_i E[Y^3 xi_i]^2/a oracle."""
+    if sum(t*t for t in u) != 1:
+        raise ValueError('test direction must have unit length')
+    atoms = tuple(itertools.product((-2, -1, 1, 2), repeat=len(u)))
+    sixth = F(0)
+    cross = [F(0)]*len(u)
+    for xi in atoms:
+        y = sum(t*s for t, s in zip(u, xi))
+        sixth += y**6
+        for i in range(len(u)):
+            cross[i] += y**3*xi[i]
+    sixth /= len(atoms)
+    cross = [v/len(atoms) for v in cross]
+    return sixth-sum(v*v for v in cross)/F(5, 2)
+
+
+def diagnostics(mode: str | None = None) -> dict:
+    if mode not in (None, 'M1', 'M2', 'M3', 'M4'):
+        raise ValueError('unknown mutant')
+    a, b, c = test_cumulants()
+    A, B = tau_coefficients(a, b, c, mode)
+    checks = {
+        'intermediate_support': envelope(3, 1, -1, mode) == (F(0), F(1, 4)),
+        'support_scaling': support_values(4, 2, -3, mode) == (F(-1), F(1, 4), F(1, 3), F(5, 16)),
+        'conditioning': B == c-b*b/a,
+        'fourth_cumulant_coefficient': A == 9*a*b,
+        'finite_spectral_regression': all(
+            tau_polynomial(tuple(t*t for t in u), a, b, c, mode) == direct_spectral_regression(u)
+            for u in test_directions()),
+        'flat_two_coordinate_edge': all(polynomial((F(j, 10), 1-F(j, 10)), -3, 2) == -1
+                                        for j in range(11)),
+    }
+    values = support_values(4, 9*a*b, c-b*b/a)
+    return {'object': 'PERIODIC-TAU-ENVELOPE-20261005', 'scientific_effect': 'NONE',
+            'mutant': mode, 'checks': checks, 'passed': all(checks.values()),
+            'finite_spectrum_cumulants': [str(a), str(b), str(c)],
+            'tau_support_values_d4': [str(6*a**3+v) for v in values],
+            'limits': 'Exact rational controls only; no Gaussian realization, image-sum or Lean certificate.'}
+
+
+def main() -> int:
+    parser = argparse.ArgumentParser(description=__doc__)
+    parser.add_argument('--mutant', choices=('M1', 'M2', 'M3', 'M4'))
+    args = parser.parse_args()
+    result = diagnostics(args.mutant)
+    print(json.dumps(result, indent=2, sort_keys=True))
+    return 0 if result['passed'] else 1
+
+
+if __name__ == '__main__':
+    raise SystemExit(main())