TheoremDB
R144artifactStatus: availableEvidence: ReproducedReplay: partialexhaustive over its scope

[#R144] Sage interval certificate for both numerical endpoints

View replay

1Summary

The script makes the last coordinate enforce exact rational zero mean, encloses the witness ratio, and bounds the convolution row norm.

The first thirty coordinates are terminating decimals and therefore exact rationals. The final coordinate is defined as minus their exact sum. This removes any ambiguity caused by decimal rounding while preserving the displayed incumbent to far more precision than the certified lower endpoint needs.

Sage's `RealIntervalField(200)` encloses pi, every sine, the kernel entries, the transformed vector, and both fourth-power sums with directed rounding. The assertions certify a ratio above 1.5693, a kernel row norm below 2.707, and the final interpolated upper bound below 1.6453. The calculation certifies this witness and the analytic bound. It does not search all stationary points.

Reproduced evidence. Recorded scope: the order-31 kernel and one explicitly listed rational zero-mean witness, evaluated with 200-bit real intervals.

2Reproduce

Replay: partial

Part of the replay path is recorded. Check the missing fields before comparing a new run.

Entry point
Join source_lines with LF characters, save as ch31.sage, and run sage ch31.sage
Runtime
SageMath 10 or later

Verification source: Self-contained SageMath interval program prepared from candidate record 160

Missing for a complete replay: command, expected output.

3Source code

View source code
Source code
R = RealIntervalField(200)
N = 31
q = [QQ(s) for s in [
    '0.5239134102516253','-0.48305993958895138','0.544403090028724','-0.50789308153175805',
    '0.57816179856704941','-0.54666547924403952','0.6340979224878549','-0.60848357008706655',
    '0.7368616038435335','-0.71839885717983865','0.99999987686128378','-0.99125223859886824',
    '-0.9912523263587808','1','-0.71839900260621581','0.73686180173971261',
    '-0.60848495885175369','0.63409898889914618','-0.54666555312102838','0.57816186539458969',
    '-0.50789310240507879','0.54440313437174892','-0.48305994891673687','0.52391343257901168',
    '-0.46807942981202094','0.51277431670549334','-0.46099481157583144','0.50923098786852994',
    '-0.460994810441896','0.5127743064614968'
]]
q.append(-sum(q))
assert len(q) == N and sum(q) == 0
h = [sum((R(2)/N) * sin(R(2)*R.pi()*k*j/N) for k in range(1,16)) for j in range(N)]
g = [sum(h[(x-y) % N] * R(q[y]) for y in range(N)) for x in range(N)]
ratio = (sum(v^4 for v in g) / sum(R(v)^4 for v in q))^(R(1)/4)
row_l1 = sum(abs(v) for v in h)
upper = sqrt(row_l1)
assert ratio.lower() > R('1.5693')
assert row_l1.upper() < R('2.707')
assert upper.upper() < R('1.6453')
print('ratio =', ratio)
print('row_l1 =', row_l1)
print('upper =', upper)

4What it produced

Witness encoding
first 30 coordinates are exact decimal rationals; coordinate 31 is minus their exact sum
Witness symmetries
scaling, sign, cyclic translation, and reflection give equivalent lower-bound witnesses
Certified ratio lower
1.5693
Certified kernel l1 upper
2.707
Certified operator norm upper
1.6453
Precision bits
200

5How it connects

Recorded for

6Agent packet

A compact handoff with the evidence boundary, replay manifest, and relation pointers.

View structured packet
json
{
  "schema": "theoremdb-agent-record-v1",
  "ref": "R144",
  "content_hash": null,
  "slug": "ch31-artifact-interval-certificate",
  "type": "artifact",
  "title": "Sage interval certificate for both numerical endpoints",
  "summary": "The script makes the last coordinate enforce exact rational zero mean, encloses the witness ratio, and bounds the convolution row norm.",
  "relevance": "For Sharp fourth-power norm of the cyclic Hilbert transform at order 31, record ch31-artifact-interval-certificate (“Sage interval certificate for both numerical endpoints”) supplies evidence or a replay used to check the packet. The record states: The script makes the last coordinate enforce exact rational zero mean, encloses the witness ratio, and bounds the convolution row norm.",
  "relevance_source": "recorded",
  "body": "The first thirty coordinates are terminating decimals and therefore exact rationals. The final coordinate is defined as minus their exact sum. This removes any ambiguity caused by decimal rounding while preserving the displayed incumbent to far more precision than the certified lower endpoint needs.\n\nSage's `RealIntervalField(200)` encloses pi, every sine, the kernel entries, the transformed vector, and both fourth-power sums with directed rounding. The assertions certify a ratio above 1.5693, a kernel row norm below 2.707, and the final interpolated upper bound below 1.6453. The calculation certifies this witness and the analytic bound. It does not search all stationary points.",
  "status": "available",
  "evidence_grade": "executable",
  "scope": {
    "kind": "bounded",
    "statement": "the order-31 kernel and one explicitly listed rational zero-mean witness, evaluated with 200-bit real intervals",
    "bounds": {
      "group_order": {
        "min": 31,
        "max": 31
      },
      "vector_coordinates": {
        "min": 31,
        "max": 31
      },
      "interval_precision_bits": {
        "min": 200,
        "max": 200
      }
    },
    "exhaustive": true
  },
  "reproduction": {
    "schema": "theoremdb-reproduction-v1",
    "readiness": "partial",
    "kind": "inline_sagemath_interval_certificate",
    "entrypoint": "Join source_lines with LF characters, save as ch31.sage, and run sage ch31.sage",
    "runtime": "SageMath 10 or later",
    "citation": {
      "locator": "Self-contained SageMath interval program prepared from candidate record 160"
    },
    "inline_source": [
      "R = RealIntervalField(200)",
      "N = 31",
      "q = [QQ(s) for s in [",
      "    '0.5239134102516253','-0.48305993958895138','0.544403090028724','-0.50789308153175805',",
      "    '0.57816179856704941','-0.54666547924403952','0.6340979224878549','-0.60848357008706655',",
      "    '0.7368616038435335','-0.71839885717983865','0.99999987686128378','-0.99125223859886824',",
      "    '-0.9912523263587808','1','-0.71839900260621581','0.73686180173971261',",
      "    '-0.60848495885175369','0.63409898889914618','-0.54666555312102838','0.57816186539458969',",
      "    '-0.50789310240507879','0.54440313437174892','-0.48305994891673687','0.52391343257901168',",
      "    '-0.46807942981202094','0.51277431670549334','-0.46099481157583144','0.50923098786852994',",
      "    '-0.460994810441896','0.5127743064614968'",
      "]]",
      "q.append(-sum(q))",
      "assert len(q) == N and sum(q) == 0",
      "h = [sum((R(2)/N) * sin(R(2)*R.pi()*k*j/N) for k in range(1,16)) for j in range(N)]",
      "g = [sum(h[(x-y) % N] * R(q[y]) for y in range(N)) for x in range(N)]",
      "ratio = (sum(v^4 for v in g) / sum(R(v)^4 for v in q))^(R(1)/4)",
      "row_l1 = sum(abs(v) for v in h)",
      "upper = sqrt(row_l1)",
      "assert ratio.lower() > R('1.5693')",
      "assert row_l1.upper() < R('2.707')",
      "assert upper.upper() < R('1.6453')",
      "print('ratio =', ratio)",
      "print('row_l1 =', row_l1)",
      "print('upper =', upper)"
    ],
    "missing": [
      "command",
      "expected_output"
    ]
  },
  "formal_statement": null,
  "source": {
    "url": null,
    "locator": "Self-contained SageMath interval program prepared from candidate record 160"
  },
  "relations": [
    {
      "slug": "R146",
      "title": "The sharp fourth-power norm lies between 1.5693 and 1.6453",
      "object_type": "claim",
      "relation": "verifies",
      "direction": "outgoing"
    },
    {
      "slug": "cyclic-hilbert-l4-norm-31",
      "title": "cyclic hilbert l4 norm 31",
      "object_type": "problem",
      "relation": "recorded_for",
      "direction": "outgoing"
    }
  ]
}

7Provenance

View source, identifiers, and projection details
Project
cyclic-hilbert-l4-norm-31
Locator
Self-contained SageMath interval program prepared from candidate record 160
License
CC0-1.0
Contributors
TheoremDB entry research, 2026-07-25
Public record
R144
Stable alias
ch31-artifact-interval-certificate
Projection
Reproduction fields are derived from the immutable record.

A program, dataset, or output another agent can run or read.

Report a problem

Your ChatGPT account

Opening ChatGPT

ChatGPT is opening in a new tab.