[6-1] Pair dataset schema, builder skeleton, and split logic

configs/goal6_pairs.yaml

@@ -0,0 +1,51 @@
+# configs/goal6_pairs.yaml
+# owned by 6-1
+#
+# config for the real >=50k/5k/5k pair build. NOT executable yet - it
+# needs 1-8's corpus, 4-4/4-5's rule libraries and 2-6's verifier, all
+# three still open. this file pins the intended run so the numbers in
+# the spec and the numbers we eventually report come from the same place.
+
+run:
+  run_id: goal6_pairs_v1
+  resume: true
+  reproduction_command: >
+    PYTHONPATH=src python3 -m geml.data.pairs.generate
+    --config configs/goal6_pairs.yaml
+
+corpus:
+  manifest_path: data/goal1_corpus/corpus_manifest.json   # 1-8's frozen manifest
+  splits: [train, validation, test_iid, test_ood]
+
+targets:
+  # the acceptance floor, not a quota to hit by loosening anything -
+  # if saturation doesn't reach it, we report the shortfall
+  train: 50000
+  validation: 5000
+  test: 5000
+
+positives:
+  mode: SAFE_REAL          # 4-1 rewrite mode; POSITIVE_REAL_FORMAL needs recorded assumptions
+  max_per_source: 8        # cap the fan-out so one heavily-rewritable expression
+                           # can't dominate a split
+  min_step_distance: 1
+  max_step_distance: 12    # longer traces exist; 7-0 wants them stratified, not truncated silently
+
+negatives:
+  kind: same_family
+  size_tolerance: 2        # nodes. tight on purpose - a loose window makes
+                           # "which is bigger" a winning strategy
+  ratio: 1.0               # one negative per positive
+
+verification:
+  tier_order: [egraph_proof, symbolic, numeric]   # first tier that answers wins, tier recorded on the pair
+  require_refutation_for_negatives: true
+
+output:
+  path: outputs/final/goal6/pairs/
+  shard_size: 25000        # matches 1-5
+
+smoke_test:
+  count: 25
+  command: >
+    PYTHONPATH=src python3 -m pytest tests/data/test_pairs.py -v

docs/goals/goal3/DAG_EQUIVALENCE_AUDIT.md

@@ -0,0 +1,55 @@
+# Goal 3 DAG Equivalence Audit (3-5)
+
+what this actually proves, and what it doesn't - read this before
+citing the audit results anywhere.
+
+## what's covered right now
+
+only `exp` and `ln`, plus compositions of them (`ln(exp(x))`,
+`exp(exp(x))`), plus one repeated-subexpression case. those are the
+only two eml constructions currently verified against the real paper
+(arXiv:2603.21852v2, eq 3 and 5 - see 3-3/3-4). everything runnable in
+the audit set traces back to just these two building blocks.
+
+6 cases run and match exactly across every comparison axis (signature,
+node count, edge count, depth, evaluation, purity, both directions).
+
+## what's NOT covered
+
+`add`, `mul`, `pow` - none of these have real constructors yet, since
+2-2/2-3/2-4's actual compiler formulas aren't merged. there's one
+deliberately included case (`add_family_blocked`) that exists purely
+to prove the audit harness reports this gap explicitly instead of
+silently pretending everything's covered - it shows up as `blocked`,
+not as a pass, not as a skip.
+
+**do not read "6/6 passing" as "goal 3's dag conversion is proven
+correct in general."** it's proven correct for exactly the two
+families tested. every other family is an open question until it has
+its own real constructor and its own audit case.
+
+## why this matters
+
+the whole point of 3-4 (direct construction) is a performance
+optimization over 3-3 (build-then-compress) - same math, different
+allocation strategy. this audit is the thing that actually backs that
+claim up with numbers, rather than just asserting it. if a future
+family's direct and post-hoc paths ever disagree, that's a real bug in
+one of the two implementations, and this audit is what's supposed to
+catch it before it goes further.
+
+## scale note
+
+this audit runs on hand-built tiny fixtures only, not the real 250k
+corpus - that's explicitly out of scope for 3-5 (see issue: "do not
+run the full 250k pipeline"). once the real corpus exists, a similar
+but much larger-scale audit will be needed as part of a later goal 3
+task, not this one.
+
+## how to extend this later
+
+once 2-2/2-3/2-4 land with real add/mul/pow formulas, the
+`add_family_blocked` case (and equivalents for mul/pow) should get
+replaced with real runnable cases the same way `exp`/`ln` are handled
+here - build both a direct and post-hoc version, add eval bindings,
+drop it into `STRATIFIED_AUDIT_SET` in `equivalence_audit.py`.

docs/goals/goal3/GOAL3_DAG_COMPRESSION_STUDY.md

@@ -0,0 +1,60 @@
+# Goal 3 DAG Compression Study
+
+detailed findings on exact structural sharing. structural evidence
+only - this is about tree/DAG size, not about whether an expression is
+mathematically "better" in any other sense.
+
+## the core distinction this whole study depends on
+
+"compresses well" and "becomes structurally competitive" are different
+claims, and conflating them was flagged explicitly in 3-7:
+
+- **compresses well** = eml_compression is high (the DAG is much
+  smaller than that expression's own raw, uncompressed tree)
+- **structurally competitive** = dag_alpha_vs_ast_tree is low
+  (approaching or beating 1.0 - genuinely close to what a plain AST
+  tree would've cost)
+
+an expression can do the first without the second. a raw EML tree that
+starts out 40x bigger than its AST can compress 10x and still end up
+4x bigger than the AST - it compressed well, it did not become
+competitive. 3-7's `classify_dual()` reports both booleans
+independently for exactly this reason.
+
+## what the tested cases show
+
+for the two verified families (exp, ln) and their compositions:
+- raw pure EML trees are consistently larger than the equivalent AST
+  tree, matching the α > 1.56 threshold problem identified back in the
+  original project brief
+- exact structural sharing recovers a meaningful fraction of that size
+  difference whenever an expression contains genuine duplication (like
+  `(x+1)*(x+1)`-shaped repetition) - tested directly, 7 nodes down to 4
+- expressions with NO internal duplication get no benefit from sharing
+  at all (dag_node_count == ast_tree_node_count exactly) - sharing
+  only helps when there's something to share, tested directly
+
+## what this study does not claim
+
+- no e-graph claims - discovering that two DIFFERENT expressions are
+  mathematically equivalent (like sin²x+cos²x = 1) is goal 4's job
+  entirely, not tested or claimed here
+- no motif claims - goal 5's compressed-pattern-dictionary approach is
+  a different technique, not evaluated here
+- no claim about add/mul/pow/power families - not implemented yet in
+  goal 3's DAG modules, so there's nothing to report on them
+- no claim about real-scale (10k-250k) behavior - the stability-curve
+  code is built and tested against synthetic scale points, but has no
+  real corpus data run through it yet
+
+## reproducibility
+
+every number in this study traces back to a specific test in 3-1
+through 3-7's test suites, runnable independently:
+- `pytest tests/graph/test_schema.py` - schema/signature correctness
+- `pytest tests/dag/test_ast_dag.py` - AST sharing
+- `pytest tests/dag/test_eml_dag.py` - EML sharing, verified formulas
+- `pytest tests/dag/test_direct_eml_dag.py` - direct construction matches post-hoc
+- `pytest tests/experiments/test_goal3_audit.py` - the direct-vs-post-hoc audit
+- `pytest tests/experiments/test_goal3_smoke.py` - pipeline + resume guarantee
+- `pytest tests/analysis/test_goal3_analysis.py` - stratification + the dual-claim distinction

docs/goals/goal3/GOAL3_SUMMARY.md

@@ -0,0 +1,62 @@
+# Goal 3 Summary
+
+what actually got built, what's actually proven, and what isn't yet.
+structural evidence only - no claims here about math correctness
+beyond what's been directly tested, no e-graph or motif claims.
+
+## what goal 3 covers
+
+a generic graph/DAG schema (3-1) neutral across ast/eml/macro/motif
+representations, exact structural sharing for both AST trees (3-2) and
+pure EML trees (3-3), a direct/memoized construction path that skips
+allocating the full uncompressed tree (3-4), an audit proving the
+direct and post-hoc paths produce identical results (3-5), a metrics
+pipeline with checkpoint/resume built for the real 250k corpus (3-6),
+stratified analysis of that pipeline's output (3-7), and this - the
+frozen cost interface goal 4 actually consumes (3-8).
+
+## what's genuinely verified
+
+- exp(x) = eml(x, 1) and ln(z) = eml(1, eml(eml(1,z), 1)) - both
+  pulled directly from the real paper (arXiv:2603.21852v2, eq 3 and
+  5), checked numerically against math.exp/math.log, and checked
+  composed together (ln(exp(x)) = x).
+- (x+1)*(x+1)-shaped duplication collapses from 7 nodes to 4, for both
+  AST and EML DAGs, tested directly.
+- direct construction and post-hoc construction produce byte-identical
+  canonical signatures for every case both paths can currently build.
+- the resume/checkpoint guarantee: running interrupted-then-resumed
+  produces identical final success/failure counts to running straight
+  through, tested with an actual simulated interruption, not just
+  assumed.
+
+## what's NOT yet covered
+
+- add, multiply, divide, power - the real formulas exist now (found on
+  the goal2 branch, in compiler_arithmetic.py/compiler_core.py) but
+  aren't wired into goal 3's DAG modules yet. everything built so far
+  is honestly scoped to exp/ln and compositions of them.
+- the real 250k corpus run. the corpus itself was genuinely generated
+  and QA-passed (confirmed via goal1's CORPUS_QA.md - exact 250,000
+  rows, correct split counts, all checksums valid), but the actual
+  data files aren't committed to git, so goal 3's pipeline hasn't
+  actually processed them yet.
+- trig/hyperbolic functions - out of scope for this stage entirely.
+
+## denominator and scaling caveats
+
+every aggregate stat reported anywhere in goal 3's analysis (3-7)
+distinguishes all_processed_count from valid_count - an average is
+never silently computed over failed rows, and a reader always knows
+which denominator a given number is really over. the 10k/50k/100k/250k
+stability-curve machinery is built and tested, but has no real data
+points yet since the real corpus hasn't been run through the pipeline.
+
+## the frozen interface (this issue)
+
+`compute_eml_dag_cost()` / `compute_eml_dag_cost_from_tree()` in
+`src/geml/interfaces/eml_dag_cost.py` are the only things goal 4 should
+ever call for a dag cost number. this module deliberately never
+imports from `geml.experiments.*` or `geml.analysis.*` - only from the
+already-frozen `geml.graph.*`/`geml.dag.*` modules - so goal 4 never
+has to pull in goal 3's internal research code just to get a cost.

docs/specs/PAIR_DATASET_SPEC.md

@@ -0,0 +1,114 @@
+# Equivalence-pair dataset (frozen by 6-1)
+
+The dataset Goals 6, 7 and 8 all sit on. A pair is two expression ids, a
+label, and enough provenance that anyone can replay how we decided the
+label. 6-2 tensorizes these records, 7-0 replays the traces into steps,
+8-x uses the step distance as a value target - so the shapes below are a
+contract, not an implementation detail.
+
+**Status: partial start.** Schema, builder control flow, negative
+matching and split bookkeeping are implemented and tested against fakes
+(`tests/data/test_pairs.py`). The production build waits on 1-8 (final
+corpus), 4-4/4-5 (rule libraries) and 2-6 (verifier). Those come in
+through the two protocols below - this module imports none of them.
+
+## Records (`src/geml/data/pairs/generate.py`)
+
+`PairRecord` - one row of the dataset.
+
+| Field | Notes |
+|---|---|
+| `pair_id` | `left~right` for positives, `left!right` for negatives |
+| `left_expression_id` / `right_expression_id` | 1-2 corpus ids |
+| `label` | `"equivalent"` / `"not_equivalent"` |
+| `split` | one of 1-2's four splits; both sides must agree, see below |
+| `group_id` | the leakage unit - e-class id when 4-2 gives us one, expression id until then |
+| `family`, `max_depth`, `left_size`, `right_size` | stratification and OOD slicing |
+| `verification` | tier + status, on every pair including negatives |
+| `left_signature` | 3-1 signature of the state the trace starts from - 7-0 replays step 0 against it |
+| `rule_sequence` | positives only: the ordered `RuleApplication` trace |
+| `step_distance` | `len(rule_sequence)`; None for negatives |
+| `negative_kind` | negatives only |
+| `eval_tags` | `depth_ood` / `family_ood`, assigned by `tag_ood` |
+
+`RuleApplication` - one rewrite step. `rule_id`, `rule_name`, 4-1 `tier`
+and `mode`, the `site_id` it fired on, the `result_signature` after the
+step, and any `assumptions` the mode required. **7-0 replays against
+`result_signature`**, so a step without one is not replayable and the
+pair carrying it is not usable. Chained with `left_signature` this gives
+the full state sequence: state 0 is `left_signature`, state *k* is step
+*k-1*'s `result_signature`.
+
+`Verification` - `tier` (`egraph_proof` | `symbolic` | `numeric`) and
+`status` (`verified` | `refuted` | `unsupported`). Recorded on every
+pair. `unsupported` is a real outcome we keep, not a silent skip.
+
+`PairError` - retained failure row: expression id, stage, error type,
+message. Same fields 1-2's `ErrorRow` wants, without importing it while
+that branch is unmerged.
+
+## Injected interfaces
+
+Two protocols, both satisfied by objects the owning issues already
+describe:
+
+- `SaturationEngine.equivalents(source) -> Iterable[Equivalent]` - 4-2
+  through 4-5. Each `Equivalent` carries the id it reached, its size and
+  depth, and the full rule sequence that got there.
+- `Verifier.verify(left, right, rule_sequence) -> Verification` - 2-6.
+
+Passing them in is what lets the builder be finished and tested before
+either exists. It also means the fixture tests and the production run
+exercise the same code path.
+
+## What gets rejected
+
+A positive survives only if it has a non-empty trace **and** verification
+returns `verified`. Everything else lands in `errors`:
+
+| Case | Why it isn't a pair |
+|---|---|
+| engine raised | saturation hit a limit or blew up; recorded with the exception type |
+| empty rule sequence | nothing for 7-0 to replay |
+| `refuted` / `unsupported` | we don't have the proof, so we don't claim the label |
+| negative that verifies as equal | a near-miss edit that preserved meaning - real, and reported, but not a negative |
+| no size-matched candidate | reported rather than fixed by widening the tolerance |
+
+`BuildResult.counts` reports `attempted = pairs + errors`. Attempted is
+the denominator, per 4-1's reporting policy.
+
+## Hard negatives
+
+Same family, same split, node count within tolerance (default 2, see
+`configs/goal6_pairs.yaml`), nearest match wins, ties broken by
+expression id so the draw is reproducible. Non-equivalence has to be
+positively refuted by the verifier - "we couldn't prove them equal" is
+not a negative label.
+
+The tolerance is the difficulty knob. Widen it and "which side is
+bigger" starts being a winning strategy, which is exactly the shortcut
+this dataset exists to close off.
+
+## Splits and leakage
+
+Both sides of a pair come from the same corpus split - `pair_split`
+raises `CrossSplitPair` otherwise. Group splits work on `group_id`, so
+an expression and its e-class relatives can never straddle a split.
+`find_leaks(pairs)` returns every group that appears in more than one
+split; the acceptance criterion is that it returns `{}` on the real
+build.
+
+Until 4-2 merges, `group_id` falls back to the expression id. That
+fallback cannot see that two ids are e-class relatives, so the
+production build must run with `eclass_id` populated - a clean
+`find_leaks` under the fallback is weaker evidence than it looks.
+
+`tag_ood` measures OOD against what train actually contained: deeper
+than any train pair, or a family train never saw. Measured, not
+declared, so the tags can't drift away from the data as the corpus
+changes.
+
+## Not in here
+
+No tensorization (6-2), no step extraction (7-0), no training. This spec
+covers the records and how they're built, nothing downstream.