core-labs/core
core-labs/core
1
0
Fork 0
Code Issues 9 Pull requests Projects Releases Packages Wiki Activity Actions 2

feat(ADR-0140): subtract as inverse translator + additive group closure (#215)

Browse source 
Extends generate/math_versor_arithmetic.py with one new function:

    def subtract(addend: float) -> np.ndarray:
        return translator(-float(addend))

Single-line delegate to translator(); no new algebra.

Adds tests/test_arithmetic_subtract_and_group.py covering all nine
ADR-0140 acceptance families:

  Families 1-6 (ADR-0139 families applied to subtract):
    1. Embedding well-formedness — null cone preserved for subtract cases
    2. Translator-of-negative well-formedness — versor_condition < 1e-6
    3. Closure — sandwich result stays on null cone
    4. Arithmetic correctness — decoded value == 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 (structural verification of ADR-0139 claim):
    7. Inverse composition — T_{-b} * T_b = identity (max residual: 0.000e+00)
    8. Round-trip closure — versor_apply(T_{-b}, versor_apply(T_b, X)) → (a, u)
    9a. Sum composition — T_a * T_b = T_{a+b} (max residual: 0.000e+00)
    9b. Commutativity — T_a * T_b byte-equals T_b * T_a (all 10 cases)

All 96 tests pass. Group residuals are exactly 0.0 in float64.
The additive subgroup of Cl(4,1) translators along e1 is abelian and
closed; ADR-0139's algebraic claim holds at the group level.
This commit is contained in:
Shay 2026-05-24 08:34:35 -07:00 committed by GitHub
parent 589297b79a
commit 622919019d
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
3 changed files with 600 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

271
docs/decisions/ADR-0140-subtract-and-additive-group-closure.md Normal file
View file

@ -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.

9
generate/math_versor_arithmetic.py
View file

@ -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.

320
tests/test_arithmetic_subtract_and_group.py Normal file
View file

@ -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}"
)