[
  {
    "local_id": "C1",
    "type": "empirical",
    "core": true,
    "statement": "Adding 1000000 doubles drawn uniformly from [0, 1) from left to right lands a mean of 196.86 units in the last place (at most 589) from the correctly rounded sum over 50 draws, and the mean error grows as about n to the power 0.545 for n from 1000 to 1000000, near the square-root growth that independent rounding errors predict.",
    "evidence": [
      {"result": "R1.positive.by_n.1000000.recursive.mean_ulps", "produced_by": "code/summation.py", "tolerance": 0.001},
      {"result": "R1.positive.by_n.1000000.recursive.max_ulps", "produced_by": "code/summation.py"},
      {"result": "R1.positive.growth_exponent.recursive", "produced_by": "code/summation.py", "tolerance": 0.002}
    ],
    "depends_on": [],
    "falsified_if": "Re-running the same draws gives a different mean or largest error at n = 1000000, or a fitted exponent outside 0.543 to 0.547.",
    "confidence": 0.97
  },
  {
    "local_id": "C2",
    "type": "empirical",
    "core": true,
    "statement": "Pairwise summation of the same positive draws stays within 2 units in the last place of the correctly rounded sum in all 200 draws for n from 1000 to 1000000, with a mean error of 0.4 units at n = 1000000.",
    "evidence": [
      {"result": "R1.positive.max_ulps.pairwise", "produced_by": "code/summation.py"},
      {"result": "R1.positive.by_n.1000000.pairwise.mean_ulps", "produced_by": "code/summation.py", "tolerance": 0.001}
    ],
    "depends_on": [],
    "falsified_if": "Re-running the same draws finds a pairwise error above 2 units in the last place, or a mean at n = 1000000 other than 0.4.",
    "confidence": 0.97
  },
  {
    "local_id": "C3",
    "type": "empirical",
    "core": true,
    "statement": "Kahan's and Neumaier's compensated sums equal the correctly rounded sum in all 400 draws, positive and mixed-sign, including mixed-sign sums of 1000000 values whose median condition number is 991.",
    "evidence": [
      {"result": "R1.exact_trials.kahan", "produced_by": "code/summation.py"},
      {"result": "R1.exact_trials.neumaier", "produced_by": "code/summation.py"},
      {"result": "R1.trials_total", "produced_by": "code/summation.py"},
      {"result": "R1.mixed.by_n.1000000.median_condition_number", "produced_by": "code/summation.py", "tolerance": 0.001}
    ],
    "depends_on": [],
    "falsified_if": "Re-running the same draws finds a compensated sum that differs from math.fsum's correctly rounded sum.",
    "confidence": 0.96
  },
  {
    "local_id": "C4",
    "type": "empirical",
    "core": false,
    "statement": "For 1000000 values drawn uniformly from [-1, 1), measured in units in the last place of the sum of the values' magnitudes, left-to-right summation errs by a mean of 0.278047 and pairwise summation by 0.001872 over 50 draws.",
    "evidence": [
      {"result": "R1.mixed.by_n.1000000.recursive.mean_ulps_of_magnitudes", "produced_by": "code/summation.py", "tolerance": 0.000001},
      {"result": "R1.mixed.by_n.1000000.pairwise.mean_ulps_of_magnitudes", "produced_by": "code/summation.py", "tolerance": 0.000001}
    ],
    "depends_on": [],
    "falsified_if": "Re-running the same draws gives either mean more than 0.000001 away from the stated value.",
    "confidence": 0.96
  }
]