Showcase¶

The programme in one view: three mathematical execution modes, one continuity layer, eight governed domains, explicit handoffs, and a refusal to confuse momentum with completion.

Purpose

Make mathematical work cumulative, inspectable, and difficult to fool.

I MATHFORGE Questions become maps

II MATHSOLVE Maps become campaigns

III MATHCERT Claims meet the boundary

MATH-PROGRAMME preserves governance, decisions, terminology, publication, archival state, and the authoritative integrated artifact. It is not a fourth proof stage.

The central transformation¶

Stage	Governing question	Required artifact	Change achieved
Curiosity	What might be worth studying?	Lead note	A direction becomes visible
Reconstruction	What was actually asked?	Source map	Ambiguity is removed
Campaign	What exact obligation can be attacked?	Work Package	Search becomes structured
Evidence	What proof, computation, or obstruction exists?	Claim ledger	Support becomes inspectable
Handoff	What can now be checked?	Certification packet	Dependencies become explicit
Certification	What crossed the declared boundary?	Checked artifact	Local reliance becomes warranted
Integration	What is the authoritative current account?	Ledger, reviews, ADRs, public page	Meaning survives revision

What the programme refuses¶

01Promising ore presented as refined metal

Discovery may be exciting without being authoritative.

02Elegant exposition presented as discharged proof

Understanding helps a proof; it does not replace one.

03Finite computation presented as an infinite theorem

The bridge must itself be proved.

04Governance status presented as theorem status

Completed, published, selected, and archived describe artifacts unless a mathematical support route says otherwise.

Status vocabulary¶

Conjectural Computed Provisional Certified Rejected

These compact labels summarize mathematical support. They are not the same as artifact lifecycle or campaign disposition. See the Programme Status Taxonomy.

Domain portfolio¶

Domain	Mathematical state	Current programme boundary
01 · Union-Closed Sets	Open conjecture	Foundational demonstration domain; local proofs and bounded certificates only
02 · Navier–Stokes Critical Integrability	Open problem	Equation-specific critical-integral routes; no regularity theorem
03 · Hodge Conjecture	Open conjecture	Source and equivalence normalization; no new algebraicity result
04 · Birch–Swinnerton-Dyer	Open conjecture	WP00–WP04 promoted; selected restricted target remains unproved
05 · Poincaré Reconstruction	Solved classical theorem	Qualified reconstruction archive; no new proof or complete formalization
06 · Yang–Mills Existence and Mass Gap	Open problem	Source-normalized axiomatic dossier; no continuum construction or physical gap theorem
07 · P versus NP	Open problem	Machine and encoding lock; no equality, separation, algorithm, or unrestricted lower bound
08 · Riemann Hypothesis	Open conjecture	Function and zero normalization; no proof, disproof, or newly certified zero range

The catalogue is not a scoreboard. Different domains may legitimately produce a source audit, a false-proof atlas, a negative result, a selected target, a bounded certificate, or an archival dossier.

Executable fixture 001 · Exact algebraic identity¶

Source statement x² = 1 and x ≠ −1 implies x = 1 over every field extension of Q

01 · Semantic compilationAudited

Replace the inequation by an inverse variable.

02 · Exact identityChecked

Replay sparse polynomial arithmetic over exact rationals.

03 · Source implicationAudited

Depends on both semantic translation and checked identity.

Exact witnessexpanded coefficient by coefficient

x − 1 = t(x² − 1) + (1 − x)(t(x + 1) − 1)

The fixture proves that a serialized witness can be checked and adversarially mutated without promoting the surrounding semantic implication beyond its audited bridge.

Executable fixture 002 · Radical membership¶

Field-level statement x² = 0 implies x = 0 over every field extension of Q

Valid model classField extensions of Q

No nonzero nilpotent elements.

Refuted generalizationAll commutative Q-algebras

The dual numbers contain a nonzero nilpotent.

The checker distinguishes ideal membership from radical membership and preserves the false broader statement with its countermodel.

Fixture 003: The logarithmic GCD kernel¶

Certified Gram identity K(m,n) = log(gcd(m,n)) = ⟨φ(m),φ(n)⟩ for positive inputs and a finitely supported divisor feature vector

01 · Prior artClassical

General GCD-matrix theory already supplies the incidence-factorization criterion.

02 · Formal artifactCertified

Lean checks positive semidefiniteness and the exact finite-support Gram realization.

03 · Public claimPublished

The publication gate preserves every exclusion and makes no novelty claim.

No novelty or priority claim

not a new theorem
not a novel kernel
not a first proof
not a first feature representation
not a first Lean formalization

Publication changed visibility, not mathematical history. The theorem remains classical; the formal and editorial contribution is stated without a priority claim.

Review posture¶

I know which domain I am reading, what is proved, what is computed, what is conjectural, what failed, what was ruled out, which artifact is authoritative, and what must happen next.