Fixture Ledger¶

The fixture ledger is the programme heartbeat. It records what the system has actually made executable, what each fixture demonstrates, what it refuses to claim, and which boundary remains open.

Ledger rule¶

A fixture is not a trophy. It is a checked unit of programme behaviour.

Each fixture must answer four questions:

What object entered the programme?
What artifact was produced?
What was mechanically checked or audited?
What inference remains forbidden?

Current fixture sequence¶

Fixture	Stage	Demonstrates	Support status	Forbidden inference	Next dependency
`UF-INV-001`	Foundation 01	Ordinary ideal membership with inequation compilation	exact identity `CHECKED`; semantic bridge `AUDITED`	the source theorem is not certified merely because the identity replays	proof-assistant bridge for semantic compilation
`RAD-NIL-002`	Foundation 02	Radical membership with exponent and model-class boundary	radical witness `CHECKED`; field semantics `AUDITED`; ring generalization `REFUTED`	a valid field theorem cannot be generalized to all commutative rings	formal model-class theorem or Lean bridge
`LOG-GCD-001`	Published	Certified PSD theorem, explicit divisor features, and bounded public claim	theorem and feature identity `CERTIFIED`; prior art `AUDITED`; `PUB-LOG-GCD-001` published	publication does not create novelty, priority, strict-PD, zero-input, or completed-space claims	none; publication gate passed in workflow `29997559180`
`GROBNER-APPLICATIONS-2026-06`	Portfolio	Six application lanes with one selected next fixture	manifest validated in CI	polynomial form does not imply tractability or theorem status	executable application fixture
`RM-DIO-004`	Intake 01	ResearchMath row to problem card to MATHSOLVE handoff	source preservation `AUDITED`; handoff `PROVISIONAL`	dataset status is not a theorem; finite screens are not completeness proofs	MATHSOLVE campaign package
`TROPIC-GROEBNER-001`	Route 01	Tropical weight acceptance/rejection via exact initial-form witnesses	route doctrine `ADDED`; replay `PENDING`	sampled weights do not enumerate the full tropical variety	MATHCERT replay script for initial-form certificates
`APP-GEO-02`	Planned	Automated geometry coordinate theorem with one nondegeneracy condition	not yet built	algebraic identity does not certify exact geometric coverage	Fixture 005 candidate

Capability map¶

UF-INV-001
  verifies: exact ideal-membership arithmetic
  protects: inequation compilation boundary

RAD-NIL-002
  verifies: radical-membership arithmetic with exponent N
  protects: field-versus-ring model boundary

LOG-GCD-001
  verifies: pinned Lean theorem intake, explicit Finsupp Gram realization,
            prior-art governance, repository-native proof replay,
            and publication-stage claim binding
  protects: positive-semidefinite, strict-positive-definite, zero-input,
            dependency-drift, mathematical-novelty, priority, and
            publication-rhetoric boundaries

GROBNER-APPLICATIONS-2026-06
  verifies: lane portfolio completeness and boundaries
  protects: application enthusiasm from becoming method overclaim

RM-DIO-004
  verifies: external corpus intake and MATHSOLVE handoff discipline
  protects: dataset metadata from becoming proof authority

TROPIC-GROEBNER-001
  verifies: sampled tropical initial-form acceptance and rejection discipline
  protects: tropical diagrams and sparse structure from becoming overclaim

What the ledger proves about the programme¶

The fixtures do not prove major mathematics. They prove that the programme can preserve distinctions that research systems often blur:

exact arithmetic versus semantic theorem;
ideal membership versus radical membership;
field theorem versus ring falsehood;
formal theorem versus stronger interpretation;
finitely supported realization versus completed-space packaging;
positive semidefiniteness versus strict positive definiteness;
mathematical prior art versus formal-artifact contribution;
bounded search versus priority evidence;
certification versus publication;
public exposition versus claim promotion;
dependency pinning versus ambient-environment success;
application potential versus application proof;
external corpus status versus independently audited mathematical status;
MATHFORGE triage versus MATHSOLVE campaign;
MATHSOLVE campaign versus MATHCERT certification;
tropical route evidence versus complete fan enumeration.

Promotion discipline¶

A fixture may move a claim upward only when its support route changes.

Movement	Required event
`LEAD` to `AUDITED`	source, object, and boundary reconstructed
`AUDITED` to `CHECKED`	exact replay, proof checker, or independently verified computation succeeds
`CHECKED` to `CERTIFIED`	semantic correspondence is formalized or otherwise crosses the trusted boundary
`CERTIFIED` to `PUBLISHED`	the public claim is bound to certified claim IDs, permanent exclusions, prior-art status, and a passing publication gate
any status to `REFUTED`	counterexample, failed invariant, false generalization, or invalid support route is established

LOG-GCD certification record¶

LOG-GCD-001 crossed both formal and audit boundaries:

LogGcdFeature.lean
  -> pinned repository-native build, workflow 29993578051
  -> logGcd_eq_feature_inner CERTIFIED
  -> LOG-GCD-001-O002 closed

PRIOR_ART_AUDIT.md + prior_art_audit.json
  -> classical GCD-matrix criterion identified
  -> mathematical novelty NOT SUPPORTED
  -> artifact priority NOT ESTABLISHED
  -> LOG-GCD-001-O003 closed

The fixture has no unresolved certification obligation. Its permanent boundary is substantive: the programme may claim a certified formal artifact, but not a new mathematical theorem or a first formalization.

LOG-GCD publication record¶

PUB-LOG-GCD-001 binds the public note and Showcase entry to the certified claim ledger:

LOG-GCD-001-C001 CERTIFIED
LOG-GCD-001-C003 CERTIFIED
LOG-GCD-001-C004 AUDITED boundary
LOG-GCD-001-C005 AUDITED prior-art determination
        |
        v
publication_manifest.json
        |
        +-- exact permitted description
        +-- prohibited novelty and priority descriptions
        +-- canonical public page
        +-- Showcase entry
        +-- strict documentation gate
        |
        v
workflow 29997559180 PASSED
        |
        v
PUB-LOG-GCD-001 PUBLISHED on 2026-07-23

Publication changed visibility, not mathematical status. The published state is now protected against claim demotion, missing evidence, removed boundaries, and unsupported novelty or priority language.

The next visible gap¶

The programme-wide executable gap remains the tropical route:

TROPIC-GROEBNER-001 witness records
  -> MATHSOLVE route decision report
  -> MATHCERT replay script
  -> claim ledger update

No status promotion occurs without a changed support boundary.