SDS-007: CRL-Math Algebraic Reasoning Service

Document Type

Software Design Specification (SDS)

Purpose

Defines the concrete instantiation of the Ciphered Reasoning Loop (CRL) pattern for algebraic simplification and mathematical reasoning, including schema definitions, invariant policies, and agent roles.

1. Overview

This specification implements ADR-014 (Ciphered Reasoning Loop) for the domain of algebraic simplification. The key insight is that most “LLM math errors” are really missing side-conditions (illegal cancellation, domain slips, extraneous roots) — not reasoning failures per se.

CRL-Math turns math agent correctness into invariant compliance, not model cleverness.

2. Representations

The CRL-Math system operates across four representation types:

Rep	Name	Description
F	Formal AST	Typed expression AST + step list
G	Knowledge Graph	Nodes = expressions/steps/obligations, edges = “rewrites_to / requires”
N	Natural Language	Proof-carrying explanation (citations to StepIDs)
A	Agent Trace	Tool checks + hashes attached to steps

3. Entity Schemas

3.1 Expression

{
  "expr_id": "string",
  "surface": "string",              
  "rep": "F | G | N | A",
  "type": "string",                  
  "assumptions": ["string"]        
}

Example:

{
  "expr_id": "E0",
  "surface": "(sqrt(x^2 - 2x + 1)) / (x - 1)",
  "rep": "F",
  "type": "Real -> Real",
  "assumptions": []
}

3.2 Step

{
  "step_id": "string",
  "rule": "string",                  
  "input_expr_ids": ["string"],
  "output_expr_id": "string",
  "obligations_added": ["string"],   
  "witness_ids": ["string"]          
}

Rules Catalog (Algebra):

FACTOR_DIFF_SQUARES
REWRITE_QUADRATIC_TO_SQUARE
SQRT_OF_SQUARE_REAL
ABS_OVER_SELF_TO_SIGN
CANCEL_FACTOR
DISTRIBUTE
COMBINE_LIKE_TERMS

3.3 Obligation

{
  "obl_id": "string",
  "predicate": "string",             
  "origin_step_id": "string",
  "status": "required | discharged | contradicted"
}

Obligation Generators (Unsafe Rules):

Operation	Obligation Generated
Cancel factor `f(x)`	`f(x) ≠ 0`
Divide by `f(x)`	`f(x) ≠ 0`
`sqrt(f(x))` in reals	`f(x) ≥ 0`
Even power root	Handle ± or emit branch obligation
`log(f(x))`	`f(x) > 0`

3.4 Witness

{
  "wit_id": "string",
  "kind": "CAS | AlgebraRule | RandomTest | ProofChecker",
  "payload_hash": "string",          
  "note": "string"
}

4. Invariant Policies

These policies are the “cipher key” — enforceable rules the loop must satisfy.

I₁ Symbol Identity & Scope

Variables keep identity across steps. α-renaming allowed, capture not.

I₂ Domain & Side-Condition Preservation

Policy "I2_DomainObligationsPreserved"
  statement: >
    If a Step applies a rule that may change definedness (divide/cancel/log/sqrt),
    then it must emit an Obligation capturing the required side condition, and that
    Obligation must be present in the final output conditions unless discharged.

I₃ Equivalence Mode Declaration

Policy "I3_EquivalenceModeDeclared"
  statement: >
    Every simplification result must declare its EquivalenceMode. If Conditional,
    the final output must include the accumulated Obligations as explicit conditions.

Equivalence Modes:

Exact: New expr equals old for all values in domain
Conditional: Equals old under accumulated obligations
PartialFunction: Matches where both defined

I₃b Real Square Root Constraint

Policy "I3b_SqrtSquareRealIsAbs"
  statement: >
    Over real numbers, sqrt(u^2) rewrites to |u| (not u) unless an explicit condition
    u >= 0 is added and preserved.

I₄ Witnessed Rewrites

Policy "I4_WitnessedRewrites"
  statement: >
    Every Step must have at least one Witness, and rules that are commonly unsafe
    (cancel/divide/branch) must have tool-backed Witness (CAS or randomized tests).

I₅ No Orphan Narrative Claims

Policy "I5_NoOrphanNarrativeClaims"
  statement: >
    Every natural language claim must reference one or more Step IDs that justify it.

5. Agent Roles

5.1 Planner (LLM)

Proposes candidate rewrite strategies in terms of goals + obligations
Does NOT output raw text; outputs structured Step candidates

5.2 Formalizer (Tool or Constrained LLM)

Converts proposed moves into ExprAST/Step objects
Attaches required obligations to each step

5.3 Verifier (CAS / Python / Proof Checker)

Validates each step + side conditions
Produces Witness artifacts with payload hashes

5.4 Explainer (LLM)

Generates natural language (N) ONLY from verified Steps
Must reference StepIDs for every claim

5.5 Auditor (Policy Engine)

Checks all invariants (I₁–I₅)
Rejects orphan text, missing witnesses, dropped obligations
Enforces round-trip equivalence

6. Tool Strategy

For each Step:

CAS Equivalence Check — Run symbolic algebra check under obligations
Randomized Numeric Tests — 10–50 test points avoiding obligation-violating values
- Cheap, high-signal
- Catches: illegal cancellation, sign errors, missing ±, non-matching expressions

7. Loop Execution (Single Iteration)

Input

Goal: simplify (x^2 - 1)/(x - 1)

Step 1 — Encode F→G

Create nodes for expressions, goal, current assumptions.

Step 2 — Operate in G

Planner suggests: “factor numerator, cancel (x-1)”.

Step 3 — Formalize (G→F candidate)

Formalizer proposes:

S1: x^2 - 1 = (x-1)(x+1) (rule: FACTOR_DIFF_SQUARES)
S2: (x-1)(x+1)/(x-1) = x+1 obligation: x-1 ≠ 0

Step 4 — Validate

Verifier checks:

S1 algebraic identity OK
S2 requires side condition: x≠1

Step 5 — Decode to N

Explainer produces:

“Factor the numerator as (x−1)(x+1). For x≠1, cancel (x−1) to get x+1.” with citations: [S1][S2] and explicit domain note.

Round-trip Check

Does the narrative assert anything not supported by steps? No.
Does it omit the obligation? No.

Commit

Store steps, obligations, tool outputs, and hashes.

8. Stress Test Example

Problem: \(f(x) = \frac{\sqrt{x^2 - 2x + 1}}{x - 1}\)

This combines:

Square-root branch behavior (sqrt((·)^2))
Cancellation/division domain (denominator x-1)
Piecewise result (sign function)
Classic LLM failure: returning “1” and forgetting discontinuity

Correct CRL Steps:

Step	Rule	Result	Obligation
S1	REWRITE_QUADRATIC_TO_SQUARE	`sqrt((x-1)^2) / (x-1)`	None
S2	SQRT_OF_SQUARE_REAL	`\|x-1\| / (x-1)`	None
S3	ABS_OVER_SELF_TO_SIGN	`piecewise(1 if x>1, -1 if x<1)`	O1: `x ≠ 1`

Final Result: \(f(x) = \begin{cases} 1 & x > 1 \\ -1 & x < 1 \end{cases} \quad \text{undefined at } x = 1\)

9. Failure Mode Prevention

Failure Mode	How CRL Prevents It
Hidden side-conditions	Every cancel/divide/sqrt generates tracked obligations
Narrative/proof mismatch	N must be generated from StepIDs; rhetoric can’t drift
Multi-agent contradiction	Agents disagree over proposed Steps, not conflicting text
Tool hallucination	Tool outputs are hashed and referenced; claims without witnesses rejected
Branch loss	I₃b forces `sqrt(u²) → \|u\|`

10. Simplicity Metric

To prevent agents chasing nonsense rewrites, define simplicity:

AST node count ↓
Operator precedence depth ↓
Number of fractions ↓
Polynomial degree normalized (factored or expanded per policy)

Important: Simplicity must not override invariants. A “simpler” form with obligations is acceptable — but obligations must be surfaced.

11. Integration Points

SEA™ Component	Role in CRL-Math
Semantic Core	SBVR rules for obligation generation
Knowledge Graph	Step/Expression/Obligation nodes; provenance edges
CALM Validation	Policy enforcement (I₁–I₅)
Agent Config Service	Define Planner/Formalizer/Verifier/Explainer/Auditor roles
Artifact Engine	Generate proof-carrying explanations

MVP Scope

⏳ Post-MVP (specialized reasoning domain)