Gosper's algorithm records WHICH of its acceptance modes admitted an antidifference, and correctly reports the geometric identity for k*2^k as weaker than the full telescoping test it uses for k

Identifier: F:cas-gosper-acceptance-mode-distinguishes-geometric-from-telescoping
Proof route: cas-certificate
External status: proved
Axiom footprint: cas.exact-rational-and-cas-expr-normal-form: both the telescoping identity and the geometric identity are decided by axeyum-cas's own zero-test (crate::equal / CasExpr normalization), not through crate::Kernel::add_declaration., cas.gosper-telescoping-equation: that a rational-consecutive-ratio term's antidifference satisfies S(k+1)-S(k)=term, and that the geometric fragment's c*X(k+1)-X(k)=p(k) equation correctly produces an antidifference for p(k)*c^k, are Gosper's algorithm taken as read; this fact does not re-derive Gosper's theorem, only that the CAS's own two certificate types are correctly and distinguishably assigned., cas.acceptance-mode-is-recorded-not-merely-decided: AUDITED 2026-09-01. gosper.rs's three (now five, counting IdenticallyZero and GeometricIdentity) acceptance modes used to collapse into a bare returned CasExpr with no field recording which one fired -- the specific ADR-1400 finding #1 for this module. GosperEvidence and admissible_mode now make the mode part of the result and its admission a total, exhaustively-tested function of the three underlying decisions (see admission_policy_is_exhaustive_and_refutation_blocks_the_weak_mode in the same module, not cited by this fact). This fact only exercises two of the five variants (TelescopingSimplified, GeometricIdentity, both from is_full_telescoping()==true/false respectively); it does NOT exercise TelescopingRaw or the strictly-weaker ReducedGosperIdentity fallback mode on a concrete term, and makes no claim about either.

Recorded description

axeyum_cas::gosper::gosper_sum_certified(term, var) returns not just an antidifference but a typed GosperEvidence saying which of its acceptance modes admitted it. For the term k, the antidifference k(k-1)/2 is certified by the FULL exact telescoping zero-test (GosperEvidence::TelescopingSimplified, for which is_full_telescoping() is true). For the geometric x polynomial term k*2^k, the antidifference is certified instead by the geometric fragment's decidable identity c*X(k+1)-X(k)=p(k) (GosperEvidence::GeometricIdentity, for which is_full_telescoping() is false) -- a DIFFERENT and non-interchangeable certificate, even though both results are correct antidifferences. Before this distinction was recorded, gosper_sum returned a bare CasExpr with no field saying which of the (then three, now five) acceptance modes fired, so a consumer needing the strength of the full telescoping test had no way to tell it apart from a term admitted only by the weaker reduced or geometric identities. Cas-internal under ADR-0601 SS2: gosper_sum's certification runs entirely inside axeyum-cas's own zero-test machinery; there is no kernel bridge.

Formal statement

(gosper-sum-certified
  (term-a k) (sum-a (/ (* k (- k 1)) 2)) (evidence-a TelescopingSimplified)
  (term-b (* k (pow 2 k))) (sum-b X) (evidence-b GeometricIdentity)
  (assert (is-full-telescoping evidence-a))
  (assert (not (is-full-telescoping evidence-b)))
  (assert (not (= evidence-a evidence-b))))

Dependencies

The graph shows direct ledger edges. Follow a node to open its artifact page.

0 direct dependencies 0 direct dependents

Evidence

cas-gosper-acceptance-mode-recorded-on-two-terms

Kind: witness-replay
Status: checked

Supports: gosper_sum_certified assigns the FULL telescoping certificate to k's antidifference and the DIFFERENT, weaker geometric-identity certificate to k*2^k's antidifference, with is_full_telescoping() correctly distinguishing them

Checker command

cargo test -p axeyum-cas --lib gosper::tests::the_acceptance_mode_is_recorded_on_the_result -- --exact 2>/dev/null | grep -cE '^test gosper::tests::the_acceptance_mode_is_recorded_on_the_result \.\.\. ok$'

Evidence notes

Verified both directions on this host: the real test path gives count=1, exit=0; the same command against a deliberately wrong test path (…_WRONG) gives count=0, exit=1. `grep -cE` consumes the pipe so it cannot SIGPIPE.

Provenance

{
  "date": "2026-09-01",
  "established_by": "lane cas-facts-round-two, following docs/research/11-design-review/2026-09-01-cas-certificate-reconstruction-audit.md's finding #1 (gosper.rs's three acceptance modes were indistinguishable in the returned value) and confirming the repair it called for had since landed (GosperEvidence, admissible_mode, gosper_sum_certified in gosper.rs).",
  "source": "W. Gosper's algorithm for indefinite hypergeometric summation; the geometric-times-polynomial fragment's separate decidable identity is this repository's own design choice, documented at gosper.rs's module level as avoiding a removable pole the rational path's reconstruction would otherwise carry through a definite sum's boundary substitution.",
  "prior_art": [
    {
      "who": "R. William Gosper Jr.",
      "what": "the algorithm deciding hypergeometric summability and producing a rational-certificate antidifference when one exists",
      "year": 1978,
      "where": "Decision procedure for indefinite hypergeometric summation, Proc. Natl. Acad. Sci. USA 75(1), 40-42",
      "attribution": "standard attribution; this lane did not consult the primary source"
    }
  ]
}