# Certificate Map

This document maps the numerical assertions in the manuscript to the code and
machine-readable certificate in this directory.

It is intentionally different from the paper's audit appendix.  The appendix
records how external analytic estimates from DMR/MR10/IK and related sources
are translated into explicit internal lemmas.  This file records which printed
numerical inequalities are checked mechanically by the code, where the results
are stored in JSON, and which script regenerates them.

## Quick Verification

From this `code/` directory:

```sh
.venv/bin/python run_all.py
```

This runs:

| Step | Script | What it checks |
|---|---|---|
| Theorem certificate | `certify_theorem.py --no-write` | The theorem-level rounded numerical inequalities, threshold conversion, and seed certificates without rewriting JSON. |
| Seed certificates | `verify_q0.py` | Proth form, Proth witness, digit-sum chains, and threshold comparison for the seed primes. |
| Stored-M regression | `test_m_value.py` | The stored rigorous and empirical threshold literals still match fresh computations. |

To regenerate the JSON certificate:

```sh
.venv/bin/python certify_theorem.py
```

The default output is:

```text
certificates/theorem_certificate.json
```

## Certificate Scope

The certificate checks numerical consequences of the printed proof:

- exact or outward-rounded interval checks for the rigorous theorem-level
  constants;
- finite threshold comparisons used in the maximum defining `Y_*`;
- integer conversion from `Y_* <= 9.10e31` to the displayed value of `M`;
- deterministic Proth certificates and digit-sum chains for the seed primes;
- empirical bisection diagnostics, explicitly marked as not used in the proof.

The certificate does not formalize the analytic reductions from
Drmota--Mauduit--Rivat, Mauduit--Rivat 2010, or Iwaniec--Kowalski.  Those
reductions are proved in the manuscript and source-localized in the paper's
import audit appendix and in `../external-refs/`.

## JSON Schema

The top-level JSON object has these keys:

| Key | Meaning |
|---|---|
| `certificate_format_version` | Schema version for the JSON certificate. |
| `script` | Generator script, currently `certify_theorem.py`. |
| `proof_relevant_constants` | Rounded constants used in the proof of the main theorem. |
| `threshold_components` | Rigorous upper bounds and empirical diagnostics for all `Y_*` components. |
| `numeric_certificate` | Method metadata, interval endpoints, and named theorem-level checks. |
| `seed_certificates` | Proth-prime and digit-chain certificate records for the application seeds. |
| `empirical_diagnostics_not_used_in_proof` | Sharper floating-point/bisection values reported only as diagnostics. |
| `ok` | Global pass/fail flag; true iff all theorem-level and seed checks pass. |

The certificate is designed so a referee can check the manuscript constants in
two ways:

1. Read `proof_relevant_constants` and `threshold_components.rigorous_upper_bounds_used_in_proof`
   as the constants that feed the theorem.
2. Read `numeric_certificate.checks` and `seed_certificates.records[*].checks`
   as the individual boolean checks supporting those constants.

## Proof-Relevant Constants

These keys are used directly in the rigorous theorem-level statement.

| Manuscript assertion | JSON key | Value |
|---|---|---:|
| `Y_{43}^* <= 9.10 x 10^31` | `proof_relevant_constants.Y43_star_upper` | `9.10e31` |
| `Y_maj <= 7.90 x 10^31` | `proof_relevant_constants.Y_major_upper` | `7.90e31` |
| `Y_min <= 8.00 x 10^31` | `proof_relevant_constants.Y_minor_upper` | `8.00e31` |
| `Y_41 < 43` | `proof_relevant_constants.Y41_upper` | `43` |
| `Y_42 < 2.4 x 10^4` | `proof_relevant_constants.Y42_upper` | `2.4e4` |
| `Y_45 < 3.6 x 10^9` | `proof_relevant_constants.Y45_upper` | `3.6e9` |
| `Y_47 < 3.7 x 10^31` | `proof_relevant_constants.Y47_upper` | `3.7e31` |
| `log x_AP < 9` | `proof_relevant_constants.Y_AP_upper` | `9` |
| `Y_* <= 9.10 x 10^31` | `proof_relevant_constants.Y_star_upper` | `9.10e31` |
| `M <= 177843590339381623423137292296355` | `proof_relevant_constants.M_rigorous_certified` | `177843590339381623423137292296355` |
| `M < 1.78 x 10^32` | `proof_relevant_constants.M_headline_bound` and `M_headline_integer` | `1.78e32`, `178000000000000000000000000000000` |

The same threshold components are repeated under
`threshold_components.rigorous_upper_bounds_used_in_proof` to make the maximum
defining `Y_*` easy to audit.

## Assertion-to-Certificate Map

| Manuscript assertion | Certificate entries | Generator | Proof location |
|---|---|---|---|
| `Y_{43}^* <= 9.10 x 10^31` | `proof_relevant_constants.Y43_star_upper`; checks `e^72.75 < 3.94e31`, `(3.94e31 + 1) * log(10) < 9.10e31`, and `C9`--`C13b` | `certify_theorem.py` | Corollary `Lstar-upper-bound` and the characteristic-function replacement threshold. |
| `Y_maj <= 7.90 x 10^31` | `proof_relevant_constants.Y_major_upper`; check `Y_maj closed-form upper < 7.90e31` | `certify_theorem.py` | Major-arc threshold subsection. |
| `Y_min <= 8.00 x 10^31` | `proof_relevant_constants.Y_minor_upper`; checks `73.459 < log(8.00e31) < 73.460`, `(8.00e31)^0.109 > 3002.0`, `0.122009 * 3002.0 > 366.27`, `minor RHS with C_min=4e12 < 364.43`, and `0.00790 < 9R < 0.00791` | `certify_theorem.py` | Minor-arc threshold subsection using `C_min = 4e12`. |
| Insensitivity for `K_10` up to `10^9` | Check `insensitivity RHS with C_min=4.1e12 < 364.46` | `certify_theorem.py` | Insensitivity lemma for the minor-arc structural constant. |
| Dominated thresholds in the `Y_*` maximum | Checks `dominated threshold Y41 < 43`, `Y42 < 2.4E+4`, `Y45 < 3.6E+9`, `Y47 < 3.7E+31`, `Y_AP < 9` | `certify_theorem.py` | Threshold derivation section. |
| `Y_* <= 9.10 x 10^31` | `threshold_components.rigorous_upper_bounds_used_in_proof.Y_star`; all dominant and dominated threshold checks above | `certify_theorem.py` | Final maximum defining `Y_*`. |
| `M <= 177843590339381623423137292296355` | `proof_relevant_constants.M_rigorous_certified`; check `M from Y_* <= 9.10e31` | `certify_theorem.py` | Conversion from `Y_*` to digit-sum threshold `M`. |
| `M < 1.78 x 10^32` | `proof_relevant_constants.M_headline_bound`; check `headline M < 1.78e32` | `certify_theorem.py` | Main theorem numerical statement. |
| Proth seed for terminal `7` used in the A070027 theorem | `seed_certificates.records` entry with `terminal = "7"` | `certify_theorem.py`, `verify_q0.py` | A070027 theorem. |
| Backup terminal-`7` seed and terminal-stratification seeds for `2` and `5` | `seed_certificates.records` entries with `terminal = "7'"`, `"2"`, and `"5"` | `certify_theorem.py`, `verify_q0.py` | Seed robustness remark and terminal-stratification application. |
| Empirical/bisected threshold diagnostics | `threshold_components.computed_threshold_diagnostics_not_used_in_proof`; `empirical_diagnostics_not_used_in_proof` | `prime_digit_sums_constraint_checker_with_search.py` called by `certify_theorem.py` | Numerical diagnostics only; not used in theorem proof. |

## Numeric Check Ledger

The following table lists every named item in `numeric_certificate.checks`.

| Check name | Certifies | Method |
|---|---|---|
| `M from Y_* <= 9.10e31` | The exact integer ceiling for the rigorous threshold conversion. | Rational interval lower bound for `log(10)` and integer arithmetic. |
| `headline M < 1.78e32` | The certified integer `M` is below the headline decimal bound. | Exact integer comparison. |
| `e^72.75 < 3.94e31` | First closed-form part of the `Y_{43}^*` upper bound. | Rational logarithm interval. |
| `(3.94e31 + 1) * log(10) < 9.10e31` | Converts the `L_*` bound into `Y_{43}^* <= 9.10e31`. | Rational upper interval for `log(10)`. |
| `C9 at log L=72.75: L0 and D bounds` | The finite conditions labelled `C9` at the permanence threshold. | Exact rational comparisons with logarithm intervals. |
| `C10 at log L=72.75: ratio > 2` | The `C10` ratio condition at the permanence threshold. | Exact rational comparison using the printed lower bound. |
| `C11 at log L=72.75: coefficient margin` | The `C11` coefficient inequality. | Exact rational comparison and lower interval for `log(10)`. |
| `C12 at log L=72.75: coefficient margin` | The `C12` coefficient inequality. | Exact rational comparison and lower interval for `c_4 = log(10)/6`. |
| `C13a at log L=72.75: main-term absorption` | Main-term absorption part of `C13`. | Exact comparison against an upper interval for `log(7)`. |
| `C13b at log L=72.75: fixed-point margin` | Fixed-point inequality part of `C13`. | Exact rational comparison. |
| `Y_maj closed-form upper < 7.90e31` | Major-arc threshold is dominated by `7.90e31`. | Logarithmic interval comparison. |
| `73.459 < log(8.00e31) < 73.460` | Minor-arc threshold log bracket used in the printed proof. | Rational logarithm interval. |
| `(8.00e31)^0.109 > 3002.0` | Lower bound for the minor-arc exponential-decay side. | Logarithmic interval comparison. |
| `0.122009 * 3002.0 > 366.27` | Numeric lower bound for the minor-arc left-hand side. | Exact rational arithmetic. |
| `minor RHS with C_min=4e12 < 364.43` | Minor-arc right-hand side with the printed `C_min`. | Logarithmic interval comparison. |
| `insensitivity RHS with C_min=4.1e12 < 364.46` | Minor-arc right-hand side under the wider `K_10 <= 10^9` envelope. | Logarithmic interval comparison. |
| `0.00790 < 9R < 0.00791` | Bracket for the normalizing constant `9R`. | `log(10)` and `pi` intervals plus directed Decimal square roots/division. |
| `dominated threshold Y41 < 43` | `Y_41` does not contribute to the final maximum. | High-precision diagnostic value compared with safe upper bound. |
| `dominated threshold Y42 < 2.4E+4` | `Y_42` does not contribute to the final maximum. | High-precision diagnostic value compared with safe upper bound. |
| `dominated threshold Y45 < 3.6E+9` | `Y_45` does not contribute to the final maximum. | High-precision diagnostic value compared with safe upper bound. |
| `dominated threshold Y47 < 3.7E+31` | `Y_47` does not contribute to the final maximum. | High-precision diagnostic value compared with safe upper bound. |
| `dominated threshold Y_AP < 9` | AP lower-bound threshold does not contribute to the final maximum. | High-precision diagnostic value compared with safe upper bound. |

All of these checks must have `"ok": true` for `numeric_certificate` to pass.

## Threshold Components

`threshold_components.rigorous_upper_bounds_used_in_proof` contains only values
used in the printed proof:

| Component | Rigorous upper bound | Role |
|---|---:|---|
| `Y41` | `43` | Auxiliary major-arc proposition threshold. |
| `Y42` | `2.4e4` | Auxiliary major-arc proposition threshold. |
| `Y43_star` | `9.10e31` | Characteristic-function replacement threshold. |
| `Y45` | `3.6e9` | Moment-comparison threshold. |
| `Y47` | `3.7e31` | Absorption threshold. |
| `Y_major` | `7.90e31` | Major-arc positivity threshold. |
| `Y_minor` | `8.00e31` | Minor-arc threshold. |
| `Y_AP` | `9` | Arithmetic-progression prime lower-bound threshold, `log(4050)`. |
| `Y_star` | `9.10e31` | Maximum of all proof-relevant thresholds. |

`threshold_components.computed_threshold_diagnostics_not_used_in_proof` stores
the sharper empirical values produced by the constraint checker.  These values
are useful for sanity checks and parameter exploration, but the theorem uses
only the rigorous upper bounds above.

## Seed Certificate Records

Each `seed_certificates.records` item has the following fields:

| Field | Meaning |
|---|---|
| `terminal` | Terminal one-digit prime in the digit-sum chain; `"7'"` denotes the backup terminal-7 seed. |
| `k`, `n` | Proth representation `q = k * 2^n + 1`. |
| `q` | The decimal integer seed. |
| `digits` | Number of decimal digits of `q`. |
| `chain` | Iterated digit-sum chain from `q` to the terminal one-digit prime. |
| `witness_base` | Proth witness base, currently `7`. |
| `witness_mod_q` | Value of `7^((q-1)/2) mod q`; it must equal `q-1`. |
| `checks` | Boolean subchecks described below. |
| `ok` | True iff every seed subcheck required for that record passes. |

The seed subchecks are:

| Subcheck | Meaning |
|---|---|
| `proth_k_odd` | `k` is odd. |
| `proth_size_condition` | `2^n > k`, so the number has Proth form. |
| `proth_witness_base_7` | `7^((q-1)/2) == -1 mod q`, proving primality by Proth's theorem. |
| `chain_terminal_matches` | The iterated digit-sum chain ends at the stated terminal. |
| `chain_intermediates_prime` | All intermediate values in the digit-sum chain are prime. |
| `above_theorem_headline_threshold` | The seed is above the theorem's headline threshold. |
| `displayed_decimal_checked` | Whether the manuscript displays this seed's full decimal expansion. |
| `displayed_decimal_matches` | If a full decimal expansion is displayed, whether it matches the computed seed. |

The current seed records are:

| Terminal | Proth form | Digits | Chain | Manuscript use |
|---|---|---:|---|---|
| `2` | `3557 * 2^431 + 1` | `134` | `q_2 -> 641 -> 11 -> 2` | Terminal-stratification seed. |
| `5` | `4027 * 2^426 + 1` | `132` | `q_5 -> 599 -> 23 -> 5` | Terminal-stratification seed. |
| `7` | `43917 * 2^430 + 1` | `135` | `q_7 -> 601 -> 7` | A070027 theorem seed. |
| `7'` | `44853 * 2^450 + 1` | `141` | `q_7' -> 601 -> 7` | Backup terminal-7 seed. |

## Interval Methods

`numeric_certificate.method` records the interval arithmetic used by
`certify_theorem.py`:

| Quantity | Method |
|---|---|
| Logarithms | Exact rational `atanh`-series intervals with geometric tail bounds. |
| `pi` | Machin formula `pi/4 = 4 atan(1/5) - atan(1/239)` with alternating-series intervals. |
| Square roots and divisions | Python `Decimal` with directed rounding. |

The generated JSON also stores interval endpoints for `log(10)` and `pi` under
`numeric_certificate.intervals`.

## Empirical Diagnostics

The following JSON locations are diagnostic only:

- `threshold_components.computed_threshold_diagnostics_not_used_in_proof`
- `empirical_diagnostics_not_used_in_proof`

These values are generated by `prime_digit_sums_constraint_checker_with_search.py`
through `certify_theorem.py`.  They reproduce the sharper bisection values
reported in the manuscript, such as the empirical `Y_required` and empirical
`M`, but they are not used to prove the headline bound.

## Maintenance Checklist

When changing theorem-level constants or threshold definitions:

1. Update the manuscript statement/proof.
2. Update `certify_theorem.py` so the relevant assertion has a named check.
3. Regenerate `certificates/theorem_certificate.json` with:

   ```sh
   .venv/bin/python certify_theorem.py
   ```

4. Run:

   ```sh
   .venv/bin/python run_all.py
   ```

5. Update this file if a JSON key, check name, or manuscript assertion changed.
