diff --git a/docs/decisions/ADR-0140-subtract-and-additive-group-closure.md b/docs/decisions/ADR-0140-subtract-and-additive-group-closure.md new file mode 100644 index 00000000..120fa74d --- /dev/null +++ b/docs/decisions/ADR-0140-subtract-and-additive-group-closure.md @@ -0,0 +1,271 @@ +# ADR-0140 — `subtract` as Inverse Translator + Additive Group Closure + +**Status:** Draft +**Date:** 2026-05-24 +**Author:** CORE agents +**Parent:** [ADR-0139](./ADR-0139-arithmetic-as-versor-spike.md) +**Engine target:** CGA cognitive engine (`algebra/versor.py`, `algebra/cga.py`) + +--- + +## Context + +ADR-0139 proved one operation — `add` — can be represented as a closed +unit versor in Cl(4,1) with all residuals exactly 0.0 in float64. The +construction `T_t = 1 - 0.5·(t·n_inf)` produces an exactly-closed +translator because `(t·n_inf)² = 0` algebraically before any float +arithmetic occurs. + +That spike proved the algebraic substrate can host *one* operation. It +did not yet prove anything about the *structure* the operations should +form. Subtract is the smallest follow-on that: + +1. Demonstrates the family generalizes — `subtract` is the same construction + with a negated addend, so it should inherit the exact-closure property + for free. +2. Surfaces the **additive group structure**. Add + subtract together + form an abelian group on the e1 axis. The structural identities + (inverse, identity, associativity, commutativity) are the actual + thing being decoded — not just "two operations work." + +The thesis (`thesis-decoding-not-generating`) is sharper here: the engine +isn't being given subtract as a *new capability*; it's being shown that +the additive group **was already there in the algebra**, and CORE is +decoding the relationships that already hold between the operations. + +This ADR makes that decoding visible by testing the group axioms directly. + +--- + +## Decision + +### Construction + +`subtract(addend)` is implemented as `translator(-addend)`. No new +algebra; the existing `translator()` from ADR-0139 is reused with a +negated argument. + +```python +def subtract(addend: float) -> np.ndarray: + return translator(-float(addend)) +``` + +### Group-property tests + +Beyond the six assertion families inherited from ADR-0139, this ADR +introduces **three new families** that test the additive group structure: + +- **Family 7 — Inverse composition.** `T_{-b} · T_b = identity`. + Specifically, the geometric product of `translator(-b)` and + `translator(b)` equals the scalar `1` (component 0 = 1, all others 0) + within machine epsilon. + +- **Family 8 — Round-trip closure.** `versor_apply(T_{-b}, versor_apply(T_b, X)) = X`. + An additive shift followed by its inverse recovers the original + embedded quantity byte-equal at the chosen tolerance. + +- **Family 9 — Commutativity of translators.** `T_a · T_b = T_b · T_a = T_{a+b}`. + Additive translations commute and compose into a single translator + by the sum. This is the abelian property of the group; if it fails, + the algebra is decoding something other than scalar addition. + +--- + +## Acceptance + +A single test module — `tests/test_arithmetic_subtract_and_group.py` — +passes with the following assertions on a small fixed set of `(a, b)` pairs. + +### Inherited from ADR-0139 (applied to subtract) + +The same six families ADR-0139 used for `add`, applied to `subtract`: + +1. Embedding well-formedness (re-verified on subtract cases) +2. Translator-of-negative well-formedness — `versor_condition(subtract(b)) < 1e-6` +3. Closure under sandwich — `cga_inner(R, R) < 1e-5` +4. Arithmetic correctness — `decode_quantity(R, u) == (a − b, u)` within `1e-9` +5. Replay determinism — byte-identical across runs +6. Composability — `subtract(c) ∘ subtract(b)` decodes to `a − b − c` + +### New group-property families + +7. **Inverse composition.** For each `b` in the test set: + `geometric_product(translator(-b), translator(b))` equals the scalar + versor `[1, 0, 0, ..., 0]` within `1e-9` component-wise. + +8. **Round-trip closure.** For each `(a, b)` in the test set: + `versor_apply(translator(-b), versor_apply(translator(b), embed_quantity(a, "u")))` + decodes to `(a, "u")` with error `< 1e-9`. Includes the case `b = 0` + (degenerate — should be identity in the algebra). + +9. **Commutativity / composition into sum.** For each `(a, b)`: + - `geometric_product(translator(a), translator(b))` equals + `translator(a + b)` component-wise within `1e-9`. + - `geometric_product(translator(a), translator(b))` equals + `geometric_product(translator(b), translator(a))` byte-equal. + +### Fixed test cases + +```text +Subtract cases (a, b): + (0, 0), (5, 0), (0, 5), + (10, 3), (3, 10), + (1.5, 0.5), (0.25, 0.75), + (-5, 3), (5, -3), + (-2, -3), (100, 1) + +Group cases (a, b) for families 7-9: + (0, 0), (1, 0), (0, 1), + (1, 1), (-1, 1), (3, 4), + (0.5, 0.5), (-2.5, 2.5), + (100, 1), (1, 100) +``` + +--- + +## Non-goals + +Out of scope for this ADR (every item below is for a follow-on): + +- No `multiply`, `divide`, or any non-additive operation. `multiply` is + ADR-0141 territory — the dilator construction is structurally different + and concentrates the next risk. +- No `MathProblemGraph` consumer. No `PropositionGraph` construction. + No `CognitiveTurnPipeline` integration. +- No GSM8K case routed. +- No pack changes. +- No proof of associativity beyond what binary-composition tests implicitly + cover. (Three-element associativity `T_a · (T_b · T_c) = (T_a · T_b) · T_c` + would be a clean addition but is redundant given commutativity + closure + into the sum.) +- No "inverse element" exposed as a separate primitive. `subtract(b)` is + the inverse of `add(b)`; the engine does not need a named "inverse" + function until ADR-0143 (compare) or later. + +Engine B (`math_solver.py`, candidate-graph parser, S.x corridor) remains +unchanged. The 3/50 GSM8K admission set is preserved. + +--- + +## Rationale + +**Why test the group axioms here rather than later?** + +The thesis says the engine decodes what is already there. The additive +group on the real line *is* already there — it's a mathematical fact +independent of CORE. If `translator()` faithfully decodes addition, then +the group axioms must hold automatically. Testing them isn't "adding a +feature"; it's *verifying that what we think we decoded is what we +actually decoded*. + +If the inverse composition test (family 7) fails, the construction is +not decoding addition — it's decoding something that looks like addition +on small cases but doesn't form a group. That would invalidate ADR-0139 +retroactively and pause the lift program. + +If commutativity (family 9) fails, the algebra is not decoding scalar +addition — it's decoding some non-abelian operation, which means scalar +arithmetic can't be lifted onto this construction as we assumed. + +So families 7-9 are not nice-to-haves. They are the structural +verification that ADR-0139's algebraic claim is actually true at the +*group* level, not just at the *point-pair* level. + +**Why subtract, not multiply, as the next step?** + +Multiply is structurally different — it's a dilator, not a translator, +and the dilator construction in CGA (`D_s = cosh(α/2) + sinh(α/2)·(n_o ∧ n_inf)`) +sits on a different versor manifold. The closure properties have to be +re-derived. That's the next big risk; doing subtract first locks down +the additive subgroup so multiply has a clean foundation to extend from. + +Subtract is also the smallest possible follow-on — same construction, +same module, three new test families. If subtract's spike fails, we +catch the inverse-element failure with a one-line change rather than a +multi-module multiply implementation. + +**Why no MathProblemGraph wiring yet?** + +Same reason as ADR-0139: the substrate must be proven before integration. +We don't yet know whether `multiply` (the next risk) closes; if it +doesn't, the integration plan changes shape. Wiring `add` and `subtract` +into MathProblemGraph before multiply is tested would couple two +unrelated unknowns. + +--- + +## Risks + +Materially smaller than ADR-0139 because most of the load-bearing +algebra is already discharged: + +- **The inverse-composition test (family 7) may not hit exact zero.** + In ADR-0139, `T_t · reverse(T_t) = 1` was exact because of an + algebraic cancellation `B² = 0`. The composition `T_{-b} · T_b` is a + different product (`reverse` is not the same as negate). The + expected residual is bounded by `(geometric_product cancellation + precision)` at float64. If it lands between `1e-9` and `1e-6`, the + test passes the versor-condition threshold but suggests the algebra + isn't *exactly* the additive group. Worth measuring honestly. + +- **Commutativity is non-trivial at the multivector level.** Two + bivectors don't generally commute. `translator(a) · translator(b)` + multiplied out involves cross-terms; whether those cancel depends + on the structure of `B_a = a·e1·n_inf` and `B_b = b·e1·n_inf`. They + do (because both bivectors live in the same 2D subspace spanned by + `e14` and `e15`, where the algebra reduces to a commuting plane). + But this is the kind of property that's *true by structure*, not + by accident — and family 9 is exactly the test that confirms it. + +- **`b = 0` edge case.** `translator(0)` should be the scalar 1 + exactly. The construction `1 - 0.5 · (0 · n_inf)` simplifies to `1` + symbolically, and float arithmetic should reach the same result, but + family 8's `b = 0` case verifies it explicitly. + +--- + +## Replay & invariants + +Same invariants as ADR-0139: + +- `versor_condition(T) < 1e-6` for all constructed translators (now + including negative addends). +- Null inputs to `versor_apply` stay null. +- No new normalization is introduced. +- Float64 end-to-end where precision matters. +- Determinism: same `(a, b)` → identical multivector bytes across runs. + +New cross-cutting invariant introduced by this ADR (worth pinning in +the test module): **the additive subgroup of Cl(4,1) translators along +e1 is abelian and closed under composition.** Families 7-9 are the +CI-enforced statement of this invariant. + +--- + +## Sequencing for follow-on + +Only if every assertion in this ADR passes: + +1. ADR-0141: `multiply` as dilator. Concentrates the next risk. +2. ADR-0142: `Rate` as bivector; `apply_rate` as combined translator-dilator. +3. ADR-0143: `compare_*` at the proposition layer, not the versor layer. +4. ADR-0144: `PropositionGraph` from `MathProblemGraph`. +5. ADR-0145: One GSM8K case routed end-to-end through Engine A. + +If any assertion fails — particularly family 7 (inverse) or family 9 +(commutativity) — ADR-0139's algebraic claim is invalidated retroactively. +The lift program pauses until the failure mode is documented and a +revised construction is proposed. + +--- + +## Decision summary + +Extend `generate/math_versor_arithmetic.py` with one new function +(`subtract`, a one-line delegate to `translator(-b)`). Add one test +module verifying the six ADR-0139 acceptance families against subtract, +plus three new families that test the additive group structure +(inverse, round-trip, commutativity). + +Acceptance is binary: every test passes, or the ADR is withdrawn and +ADR-0139's claim is re-examined. diff --git a/generate/math_versor_arithmetic.py b/generate/math_versor_arithmetic.py index 7b62acdb..80aec93a 100644 --- a/generate/math_versor_arithmetic.py +++ b/generate/math_versor_arithmetic.py @@ -43,6 +43,7 @@ from algebra.cl41 import N_COMPONENTS, geometric_product __all__ = [ "embed_quantity", "translator", + "subtract", "decode_quantity", "N_INF", ] @@ -124,6 +125,14 @@ def translator(addend: float) -> np.ndarray: return T +def subtract(addend: float) -> np.ndarray: + """Construct the CGA translator versor for subtractive shift along e1. + + Delegates to ``translator(-addend)``. No new algebra. + """ + return translator(-float(addend)) + + def decode_quantity(F: np.ndarray, unit: str) -> tuple[float, str]: """Decode a multivector back to a (value, unit) scalar quantity. diff --git a/tests/test_arithmetic_subtract_and_group.py b/tests/test_arithmetic_subtract_and_group.py new file mode 100644 index 00000000..216bd76d --- /dev/null +++ b/tests/test_arithmetic_subtract_and_group.py @@ -0,0 +1,320 @@ +"""ADR-0140 acceptance tests — subtract as inverse translator + additive group closure. + +Nine assertion families per the ADR: + +Families 1-6 (inherited from ADR-0139, applied to subtract): + 1. Embedding well-formedness — subtract cases lie on null cone. + 2. Translator-of-negative well-formedness — versor_condition(subtract(b)) < 1e-6. + 3. Closure under sandwich — sandwich result stays on null cone. + 4. Arithmetic correctness — decoded value equals a − b within 1e-9. + 5. Replay determinism — byte-identical across runs. + 6. Composability — subtract(c) ∘ subtract(b) decodes to a − b − c. + +New group-property families: + 7. Inverse composition — geometric_product(translator(-b), translator(b)) ≈ identity. + 8. Round-trip closure — versor_apply(T_{-b}, versor_apply(T_b, X)) decodes to (a, u). + 9. Commutativity / composition into sum: + a) translator(a) * translator(b) ≈ translator(a+b) component-wise. + b) translator(a) * translator(b) == translator(b) * translator(a) byte-equal. + +If family 7 or 9 fails, ADR-0139's algebraic claim is invalidated retroactively. +The lift program is paused — see ADR-0140 §Falsification Discipline. +DO NOT loosen tolerances to make tests pass. +""" + +from __future__ import annotations + +import pytest +import numpy as np + +from algebra.cga import cga_inner +from algebra.cl41 import geometric_product +from algebra.versor import versor_apply, versor_condition +from generate.math_versor_arithmetic import ( + decode_quantity, + embed_quantity, + subtract, + translator, +) + + +# --------------------------------------------------------------------------- +# Fixed test cases per ADR-0140 §Acceptance +# --------------------------------------------------------------------------- + +SUBTRACT_CASES: list[tuple[float, float]] = [ + (0.0, 0.0), + (5.0, 0.0), + (0.0, 5.0), + (10.0, 3.0), + (3.0, 10.0), + (1.5, 0.5), + (0.25, 0.75), + (-5.0, 3.0), + (5.0, -3.0), + (-2.0, -3.0), + (100.0, 1.0), +] + +GROUP_CASES: list[tuple[float, float]] = [ + (0.0, 0.0), + (1.0, 0.0), + (0.0, 1.0), + (1.0, 1.0), + (-1.0, 1.0), + (3.0, 4.0), + (0.5, 0.5), + (-2.5, 2.5), + (100.0, 1.0), + (1.0, 100.0), +] + +# Composability case for family 6 (subtract twice). +COMPOSE_CASE: tuple[float, float, float] = (20.0, 3.0, 5.0) + +# Tolerance constants — exactly as specified in the ADR. +TOL_NULL = 1e-5 # cga_inner(X, X) for null points +TOL_VERSOR = 1e-6 # versor_condition runtime contract +TOL_DECODE = 1e-9 # arithmetic correctness / round-trip / group properties + + +# --------------------------------------------------------------------------- +# Identity versor (scalar 1): component 0 = 1, all others 0. +# --------------------------------------------------------------------------- + +def _identity_versor() -> np.ndarray: + from algebra.cl41 import N_COMPONENTS + v = np.zeros(N_COMPONENTS, dtype=np.float64) + v[0] = 1.0 + return v + + +# =========================================================================== +# Families 1-6: ADR-0139 assertion families applied to subtract +# =========================================================================== + + +# ----- Family 1: embedding well-formedness ----- + +@pytest.mark.parametrize("a,b", SUBTRACT_CASES) +def test_family1_embedding_is_null(a: float, b: float) -> None: + """embed_quantity(a, _) and embed_quantity(b, _) both lie on the null cone.""" + X_a = embed_quantity(a, "u") + X_b = embed_quantity(b, "u") + inner_a = abs(float(cga_inner(X_a, X_a))) + inner_b = abs(float(cga_inner(X_b, X_b))) + assert inner_a < TOL_NULL, ( + f"embed_quantity({a}) not null: |cga_inner| = {inner_a:.3e}" + ) + assert inner_b < TOL_NULL, ( + f"embed_quantity({b}) not null: |cga_inner| = {inner_b:.3e}" + ) + + +# ----- Family 2: translator-of-negative well-formedness ----- + +@pytest.mark.parametrize("a,b", SUBTRACT_CASES) +def test_family2_subtract_unit_versor(a: float, b: float) -> None: + """subtract(b) satisfies versor_condition < 1e-6.""" + S = subtract(b) + cond = versor_condition(S) + assert cond < TOL_VERSOR, ( + f"subtract({b}) not unit versor: versor_condition = {cond:.3e}" + ) + + +# ----- Family 3: closure under sandwich ----- + +@pytest.mark.parametrize("a,b", SUBTRACT_CASES) +def test_family3_sandwich_preserves_null(a: float, b: float) -> None: + """versor_apply(subtract(b), embed_quantity(a, _)) stays on the null cone.""" + X = embed_quantity(a, "u") + S = subtract(b) + R = versor_apply(S, X) + inner_R = abs(float(cga_inner(R, R))) + assert inner_R < TOL_NULL, ( + f"sandwich result ({a} − {b}) not null: |cga_inner(R, R)| = {inner_R:.3e}" + ) + + +# ----- Family 4: arithmetic correctness ----- + +@pytest.mark.parametrize("a,b", SUBTRACT_CASES) +def test_family4_decode_matches_difference(a: float, b: float) -> None: + """decode_quantity(R, _) returns (a − b, _) within 1e-9.""" + X = embed_quantity(a, "u") + S = subtract(b) + R = versor_apply(S, X) + value, unit = decode_quantity(R, "u") + expected = a - b + err = abs(value - expected) + assert unit == "u", f"unit metadata lost: got {unit!r}" + assert err < TOL_DECODE, ( + f"decode error for ({a} − {b}): got {value}, expected {expected}, err = {err:.3e}" + ) + + +# ----- Family 5: replay determinism ----- + +@pytest.mark.parametrize("a,b", SUBTRACT_CASES) +def test_family5_replay_byte_identical(a: float, b: float) -> None: + """Two independent runs produce byte-identical multivector arrays.""" + X1 = embed_quantity(a, "u") + X2 = embed_quantity(a, "u") + S1 = subtract(b) + S2 = subtract(b) + R1 = versor_apply(S1, X1) + R2 = versor_apply(S2, X2) + assert X1.tobytes() == X2.tobytes(), ( + f"embed_quantity({a}) not deterministic across runs" + ) + assert S1.tobytes() == S2.tobytes(), ( + f"subtract({b}) not deterministic across runs" + ) + assert R1.tobytes() == R2.tobytes(), ( + f"versor_apply result not deterministic across runs for ({a}, {b})" + ) + + +# ----- Family 6: composability ----- + +def test_family6_two_subtracts_compose() -> None: + """subtract(c) ∘ subtract(b) applied to embed_quantity(a) decodes to a − b − c.""" + a, b, c = COMPOSE_CASE + X = embed_quantity(a, "u") + S_b = subtract(b) + S_c = subtract(c) + + R1 = versor_apply(S_b, X) + R2 = versor_apply(S_c, R1) + + inner_R1 = abs(float(cga_inner(R1, R1))) + inner_R2 = abs(float(cga_inner(R2, R2))) + assert inner_R1 < TOL_NULL, ( + f"intermediate (a − b = {a - b}) not null: |cga_inner| = {inner_R1:.3e}" + ) + assert inner_R2 < TOL_NULL, ( + f"final (a − b − c = {a - b - c}) not null: |cga_inner| = {inner_R2:.3e}" + ) + + value, unit = decode_quantity(R2, "u") + expected = a - b - c + err = abs(value - expected) + assert unit == "u" + assert err < TOL_DECODE, ( + f"compose decode error: got {value}, expected {expected}, err = {err:.3e}" + ) + + +# =========================================================================== +# Families 7-9: Additive group structure verification +# =========================================================================== + + +# ----- Family 7: inverse composition ----- +# +# geometric_product(translator(-b), translator(b)) must equal the identity +# versor (component 0 = 1, all others 0) within 1e-9 component-wise. +# +# If this fails, the algebra is not decoding exact addition — it is decoding +# something that resembles addition on point-pairs but does not form a group. +# That invalidates ADR-0139 retroactively. STOP; do not loosen 1e-9. + +@pytest.mark.parametrize("a,b", GROUP_CASES) +def test_family7_inverse_composition_is_identity(a: float, b: float) -> None: + """geometric_product(translator(-b), translator(b)) ≈ identity within 1e-9.""" + T_pos = translator(b) + T_neg = translator(-b) + product = geometric_product(T_neg, T_pos) + identity = _identity_versor() + + residual = np.abs(product - identity) + max_residual = float(residual.max()) + assert max_residual < TOL_DECODE, ( + f"Inverse composition residual for b={b}: max |product - identity| = {max_residual:.6e}\n" + f"Component residuals (non-zero): " + + str([(i, float(residual[i])) for i in range(len(residual)) if residual[i] > 1e-15]) + ) + + +# ----- Family 8: round-trip closure ----- +# +# versor_apply(T_{-b}, versor_apply(T_b, embed_quantity(a))) must decode +# back to (a, "u") within 1e-9. Includes the b=0 edge case. + +@pytest.mark.parametrize("a,b", GROUP_CASES) +def test_family8_round_trip_closure(a: float, b: float) -> None: + """versor_apply(T_{{-b}}, versor_apply(T_b, X)) decodes to (a, u) within 1e-9.""" + X = embed_quantity(a, "u") + T_pos = translator(b) + T_neg = translator(-b) + + shifted = versor_apply(T_pos, X) + recovered = versor_apply(T_neg, shifted) + + # Intermediate must stay on null cone. + inner_shifted = abs(float(cga_inner(shifted, shifted))) + assert inner_shifted < TOL_NULL, ( + f"Round-trip intermediate not null for (a={a}, b={b}): " + f"|cga_inner| = {inner_shifted:.3e}" + ) + + # Final must stay on null cone. + inner_recovered = abs(float(cga_inner(recovered, recovered))) + assert inner_recovered < TOL_NULL, ( + f"Round-trip result not null for (a={a}, b={b}): " + f"|cga_inner| = {inner_recovered:.3e}" + ) + + value, unit = decode_quantity(recovered, "u") + err = abs(value - a) + assert unit == "u" + assert err < TOL_DECODE, ( + f"Round-trip decode error for (a={a}, b={b}): " + f"got {value}, expected {a}, err = {err:.3e}" + ) + + +# ----- Family 9a: composition into sum ----- +# +# geometric_product(translator(a), translator(b)) must equal translator(a+b) +# component-wise within 1e-9. + +@pytest.mark.parametrize("a,b", GROUP_CASES) +def test_family9a_composition_equals_sum_translator(a: float, b: float) -> None: + """geometric_product(translator(a), translator(b)) == translator(a+b) within 1e-9.""" + T_a = translator(a) + T_b = translator(b) + T_sum = translator(a + b) + + product = geometric_product(T_a, T_b) + residual = np.abs(product - T_sum) + max_residual = float(residual.max()) + assert max_residual < TOL_DECODE, ( + f"Sum-composition residual for (a={a}, b={b}): " + f"max |T_a*T_b - T_{{a+b}}| = {max_residual:.6e}\n" + f"Component residuals (non-zero): " + + str([(i, float(residual[i])) for i in range(len(residual)) if residual[i] > 1e-15]) + ) + + +# ----- Family 9b: commutativity ----- +# +# geometric_product(translator(a), translator(b)) must equal +# geometric_product(translator(b), translator(a)) byte-exactly. +# If this fails, the algebra decodes a non-abelian operation. + +@pytest.mark.parametrize("a,b", GROUP_CASES) +def test_family9b_commutativity_byte_equal(a: float, b: float) -> None: + """geometric_product(translator(a), translator(b)) byte-equals geometric_product(translator(b), translator(a)).""" + T_a = translator(a) + T_b = translator(b) + + ab = geometric_product(T_a, T_b) + ba = geometric_product(T_b, T_a) + + assert ab.tobytes() == ba.tobytes(), ( + f"Commutativity violation for (a={a}, b={b}): " + f"T_a*T_b != T_b*T_a\n" + f"Max component diff: {float(np.abs(ab - ba).max()):.6e}" + )