Evidence and certificate integration for simultaneous Pell bounds

[roed-math]

Goal

Give the proved simultaneous-Pell results their final, machine-checkable evidence: adopt the certificate schema established by #55's #72 (kind="certificate", certified=True) and record the complete bound chain — seed orbits, initial analytic bound, every reduction round, certified precision, final index rectangle, exhaustive-search completion — inside SolutionSet.evidence, with an exact JSON contract in as_dict().

Boundary of the reuse, stated exactly: the certificate record shape is shared infrastructure with #55; the mathematics is not. The S-unit/de Weger pipeline (#55) and the simultaneous-Pell Baker–Davenport reduction are separate mathematical reductions; nothing in this issue or its docstrings may describe them as the same pipeline. The shared parts are the #72 certified-arithmetic primitives and the certificate record conventions, nothing else.

Target base

• Repository state: branch review-architecture @ 85f8e0a (the composed
  tree on the roed-math fork: wave-1 code = PRs Packaging, CI, design notes, and the annotated bibliography #2–Family: waring — Waring-type diagonal representation #48, plus the wave-2 and
  architecture-review series, which are not yet opened as PRs).
• Required merged PRs: Packaging, CI, design notes, and the annotated bibliography #2–Family: waring — Waring-type diagonal representation #48 (wave 1); the wave-2/architecture-review series
  must land after them before this issue's work can merge to main.
  Implementation happens on the composed tree, not on a split branch.

Dependencies

• Parent: Rigorous completion of simultaneous Pell searches #58.
• Blocked by: Certified Baker–Davenport reduction for the unit right-hand-side case #81 (which carries the Certified logarithmic-bound and LLL-reduction primitives #72 schema dependency transitively).
• Unblocks: Simultaneous-Pell solver integration and partial fallback boundaries #84. (Extension to supported nonunit right-hand sides #83 extends the payload with per-pair records; the extension rules are written there.)

Supported inputs

The proved results produced by the #81 pipeline (and later #83's). The fallback path is untouched: its plain-string evidence ("orbit search along the first Pell equation",) stays exactly as it is today (#84 freezes it verbatim).

Output and API contract

The certificate record

One evidence.Evidence record joining SolutionSet.evidence alongside #81's two theorem records:

Evidence(
    <one-line human summary of the certified reduction>,
    kind="certificate",
    certified=True,
    software="sage",
    version=software_version("sage"),
    certificate={
        "pipeline": "simultaneous-pell-baker-davenport",
        "seed_orbits": [<equation 1's #80 certificate>, <equation 2's>],
        "initial_bound": {"theorem": "Matveev (BMS Thm 9.4)", "value": <exact bound>},
        "rounds": [
            {"dimension": 2, "scaling_C": <exact>, "precision_bits": <exact>,
             "b1_norm_lower": <exact>, "new_bound": <exact>},
            ...
        ],
        "final_box": {"j": [<min>, <max>], "k": [<min>, <max>]},
        "search_completion": {"method": "orbit-walk", "range": <exact stop height>},
    },
)

Field contract:

• "pipeline" — the literal string "simultaneous-pell-baker-davenport"; this is the discriminator against Rigorous de Weger completion of the exponential searches #55's pipelines (separate reduction, shared schema only).
• "seed_orbits" — the two Complete seed-orbit enumeration for generalized Pell equations #80 enumeration certificates, one per equation, embedded as their exact payloads ({"seeds": ..., "fundamental": ..., "crosscheck": "nagell-bound-exhaustive"}).
• "initial_bound" — the theorem name literal "Matveev (BMS Thm 9.4)" and the exact integer bound B_0 actually derived; recording this value is what locks the pinned instantiation of the theorem's constants (Certified Baker–Davenport reduction for the unit right-hand-side case #81).
• "rounds" — one entry per Dujella–Pethő round in execution order, with exactly the five keys of Certified logarithmic-bound and LLL-reduction primitives #72's shared round-record schema: the lattice dimension (2), the round's scaling constant scaling_C, the working precision_bits, the certified exact lower bound b1_norm_lower for the round's lattice norm/distance quantity (the reduced-basis quantity the round's criterion consumed), and the new_bound it produced. new_bound values are strictly decreasing (the termination rule in Certified Baker–Davenport reduction for the unit right-hand-side case #81 discards the non-improving final attempt).
• "final_box" — the final index rectangle for (j, k) after the last improving round.
• "search_completion" — method is the literal "orbit-walk"; range is the exact integer stop height used by the finishing walk over _pell_solutions_stream(D1, N1).
• Exactness rule: every numeric leaf is an exact ZZ/QQ value — where a quantity was computed as a real ball, the recorded value is the exact rational enclosure endpoint actually consumed by the certified computation (upper endpoint for quantities used as upper bounds, lower for lower). Values are never pre-stringified in memory; floats never appear; Evidence.to_dict() encodes all of it recursively through serialize.encode_exact. SCHEMA_VERSION stays 3 — the certificate rides inside the existing Evidence encoding.

One complete exact JSON example

The following is the to_dict() image of the certificate record. It is schematic only in its "<decimal>" placeholders, which stand for literal decimal strings; everything else — key names, nesting, tag names — is the exact contract:

{
  "kind": "certificate",
  "statement": "Baker-Davenport reduction over the seed orbits certifies the full finite solution list",
  "software": "sage",
  "version": "SageMath version 10.7, Release Date: 2025-08-09",
  "certified": true,
  "certificate": {
    "pipeline": "simultaneous-pell-baker-davenport",
    "seed_orbits": [
      {
        "seeds": [[{"type": "integer", "value": "1"}, {"type": "integer", "value": "0"}]],
        "fundamental": [{"type": "integer", "value": "2"}, {"type": "integer", "value": "1"}],
        "crosscheck": "nagell-bound-exhaustive"
      },
      {
        "seeds": [[{"type": "integer", "value": "1"}, {"type": "integer", "value": "0"}]],
        "fundamental": [{"type": "integer", "value": "3"}, {"type": "integer", "value": "1"}],
        "crosscheck": "nagell-bound-exhaustive"
      }
    ],
    "initial_bound": {
      "theorem": "Matveev (BMS Thm 9.4)",
      "value": {"type": "integer", "value": "<decimal>"}
    },
    "rounds": [
      {
        "dimension": {"type": "integer", "value": "2"},
        "scaling_C": {"type": "rational", "numerator": "<decimal>", "denominator": "<decimal>"},
        "precision_bits": {"type": "integer", "value": "<decimal>"},
        "b1_norm_lower": {"type": "integer", "value": "<decimal>"},
        "new_bound": {"type": "integer", "value": "<decimal>"}
      }
    ],
    "final_box": {
      "j": [{"type": "integer", "value": "<decimal>"}, {"type": "integer", "value": "<decimal>"}],
      "k": [{"type": "integer", "value": "<decimal>"}, {"type": "integer", "value": "<decimal>"}]
    },
    "search_completion": {
      "method": "orbit-walk",
      "range": {"type": "integer", "value": "<decimal>"}
    }
  }
}

(The two seed_orbits entries shown are the real D = 3, N = 1 and D = 8, N = 1 payloads for the classical fixture — fundamental (2, 1) and (3, 1) respectively, seed (1, 0) each; verified against Sage 10.7 / PARI 2.17.2. The scaling_C entry is shown with the rational tag to display the QQ leaf encoding — #72's schema admits ZZ or QQ there, and an integer scaling serializes with the integer tag instead.)

Algorithm and conventions

• Build the certificate inside the Certified Baker–Davenport reduction for the unit right-hand-side case #81 pipeline from the values it already computes; this issue adds no mathematics — it fixes the record's shape, exactness and serialization.
• The certificate record replaces Certified Baker–Davenport reduction for the unit right-hand-side case #81's provisional computation-record payload; the two theorem records (Certified Baker–Davenport reduction for the unit right-hand-side case #81) stay alongside it in SolutionSet.evidence.
• The exact values recorded for the classical fixture are committed from the first verified run and asserted literally thereafter — they lock the Matveev instantiation and the reduction schedule against regression.
• Sage-convention docstrings with doctests on every new function (INPUT/OUTPUT/EXAMPLES, passing sage -t); docstring coverage stays 100%.

Failure and fallback semantics

• The certificate is attached only to proved pipeline results. The fallback path's SolutionSet keeps its current plain-string evidence unchanged; the proved-empty first-equation branch keeps its current form (kind="empty", no certificate — SEMANTICS permits proved-empty without evidence).
• A certificate that cannot be completed (any field unavailable) is an internal error of the pipeline, not a degraded record: the pipeline either produces the full certificate or declines to claim proved (Simultaneous-Pell solver integration and partial fallback boundaries #84 fallback). Partial certificates never ship.

Acceptance criteria

1. For the classical fixture solve("x^2 - 3*z^2 = 1; y^2 - 8*z^2 = 1"): SolutionSet.evidence contains exactly one kind="certificate" record with certified is True; its payload has exactly the six keys {"pipeline", "seed_orbits", "initial_bound", "rounds", "final_box", "search_completion"}; pipeline == "simultaneous-pell-baker-davenport"; initial_bound["theorem"] == "Matveev (BMS Thm 9.4)"; rounds is nonempty with strictly decreasing new_bound values and each entry carrying exactly the five keys {"dimension", "scaling_C", "precision_bits", "b1_norm_lower", "new_bound"}; final_box is a finite rectangle containing the index pairs realized by the found solutions; search_completion["method"] == "orbit-walk"; the two seed_orbits payloads are exactly the Complete seed-orbit enumeration for generalized Pell equations #80 certificates for (3, 1) and (8, 1).
2. The exact numeric certificate values for the fixture are committed from the first verified run and asserted literally.
3. Round-trip: json.dumps(S.as_dict()) followed by json.loads reproduces the dictionary exactly; reconstructing the tagged leaves yields the original ZZ/QQ values; no float appears anywhere in the dump.
4. The solver-contract suite's constraints hold and are asserted for these results: proved implies complete + evidence + scope; evidence kinds from EVIDENCE_KINDS; every reference key resolves in data/references.bib.
5. No docstring, description or doc introduced by this issue describes Rigorous de Weger completion of the exponential searches #55 and Rigorous completion of simultaneous Pell searches #58 as the same pipeline; the discriminator string is asserted in a test.
6. make test, make doctest, make coverage (docstring coverage stays 100%), make registry-docs clean.

Out of scope

• Any change to the mathematical pipeline (Certified Baker–Davenport reduction for the unit right-hand-side case #81) or its regimes (Extension to supported nonunit right-hand sides #83).
• The fallback path's evidence (stays the plain string; Simultaneous-Pell solver integration and partial fallback boundaries #84).
• Per-pair payload extension for multi-seed systems (Extension to supported nonunit right-hand sides #83 specifies it).
• Rigorous de Weger completion of the exponential searches #55's own certificates and pipelines.

References

BugeaudMignotteSiksek2006 and DujellaPetho1998 are cited by the theorem records this certificate accompanies (#81); no new bibliography entries are needed by this child.