OPT v1.4.0 — Exact Pair Streams, Modular Filtering and Mathematical Evidence

OPT v1.4.0 adds OPT-STREAM-001 — Bounded replayable pair streams, extending the catalog to 22 optimization records. This release covers exact integer enumeration, complete equal-sum joins, modular filtering, and reproducible measurements of their memory–latency tradeoffs.

Exact pair streams and bounded replay

• Adds PairSums, which enumerates indexed pair sums through a heap instead of materializing the entire Cartesian product.
• Adds an exact equal-sum join with bounded tie buffering and suffix replay.
• Preserves duplicate occurrences, original indices and deterministic ordering.
• Supports immutable input snapshots and independent replay clones.
• Treats interrupted enumeration as an incomplete prefix.

The mechanism is independently adapted from the inspected OpenAI math manuscripts, retaining attribution to the classical Schroeppel–Shamir pair-sum method.

Modular pair filtering

Adds a separate FilteredPairSums API that generates only pairs satisfying a declared residue condition.

• Preserves actual-sum and original-index ordering.
• Supports positive composite moduli and modulus one.
• Normalizes signed residues.
• Allocates no table proportional to the modulus.
• Preserves duplicate identities and replay independence.

Congruence remains distinct from exact equality. The existing unfiltered pair stream and exact join retain their established behavior.

Reproducible performance evidence

Three benchmark procedures retain raw samples, environment details, source identities, counts and ordered output digests.

• Pair enumeration: the local 128×128 fixture reduces median traced allocation from 1,871,552 bytes to 23,641 bytes, approximately 79× lower.
• Full joins: 350 verified samples characterize seven fixture shapes and four buffer capacities. Small buffers save memory but can increase replay latency; larger buffers trade additional storage for lower replay cost.
• Modular filtering: 180 verified samples characterize nine fixtures. Sparse balanced fixtures run approximately 24–28× faster locally, while temporary bucket construction raises traced allocation peaks to approximately 2.2× baseline. Dense fixtures show no established latency advantage.

Full-join and modular benchmarks measure timing separately from allocation tracing. These synthetic observations establish neither portable defaults nor target-application speedups.

Mathematical evidence scope

Adds EVIDENCE-SCOPE.md and expands the record template and donor assessment to distinguish:

• file integrity;
• numerical certificate replay;
• manuscript arguments;
• selected formal theorem coverage;
• independent implementation tests;
• target performance measurements.

The OpenAI math assessment is pinned to commit fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb. No donor proofs are imported or reported as independently replayed.

Validation

• 91 tests passing, including exhaustive and adversarial oracle comparisons.
• Catalog integrity verified: 22 records, including five frozen v1 records.
• PR CI passes for tests/archive inventory, catalog integrity, and Lean formalization.
• Lean trust audit verifies 354 declarations.
• Frozen formal model files and the pinned toolchain remain unchanged.

Included pull requests

• #5 — Add bounded pair streams and scoped mathematical evidence
• #6 — Characterize full equal-sum join memory and latency tradeoffs
• #7 — Add exact modular pair filtering with scoped performance evidence

Full changelog: v1.3.0...v1.4.0

Upgrade

No migration is required. The new references are optional additions, and the frozen v1 formalization retains its existing scope.