// SPDX-License-Identifier: CC-BY-SA-4.0
// Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>

= TRG Canonical Proof Suite — Mathematical, Scientific, Engineering (M/S/E-CPS)
:status: v1.1 (proposed) — 90-day review window open from 2026-04-18
:date: 2026-04-18
:toc: preamble

This is the *Canonical Proof Suite* referenced from
`TOOLCHAIN-READINESS-GRADES.adoc` §6.6. A hyperpolymath language
toolchain MUST be able to *express, machine-check, and re-run nightly*
every entry in this suite to qualify above grade *E*.

The suite is versioned. Suite expansions over time are expected and
may demote A-grade components — that demotion is acceptable and is the
mechanism by which TRG keeps pace with the frontier.

== Pass condition

A toolchain passes the M/S/E-CPS iff:

. Every entry in this document has at least one machine-checked proof
  in the language under audit.
. Every proof is re-checked nightly under at least one qualifying
  prover (see `templates/QUALIFYING-PROVERS.adoc`).
. Every proof contains zero `believe_me`, `assert_total`, `Admitted`,
  `sorry`, `postulate`, `unsafeCoerce`, or any other escape hatch
  from the banned-construct list in `TOOLCHAIN-READINESS-GRADES.adoc` §6.5.
. The corpus of proofs is publicly archived and reproducibly buildable
  from a clean checkout in a fresh environment.

== Mathematics

[cols="1,3,3",options="header"]
|===
| # | Theorem | Where to look for an existing proof to port

| M1 | *Infinitude of primes* (Euclid) | mathlib4 `Mathlib.NumberTheory.Primes.Basic`; Coq `Coquelicot`; Idris2 stdlib examples; Agda `agda-stdlib` `Data.Nat.Primality`
| M2 | *Lagrange's theorem* (group order divides) | mathlib4 `Mathlib.GroupTheory.OrderOfElement`; Coq `mathcomp.algebra.fingroup`; Agda `Algebra.Properties.Group`
| M3 | *Intermediate value theorem* (real-valued continuous functions) | mathlib4 `Mathlib.Analysis.SpecialFunctions.Polynomials`; Coq `Coquelicot.Continuity`
| M4 | *Compactness of \[0, 1\]* (Heine–Borel for the closed unit interval) | mathlib4 `Mathlib.Topology.MetricSpace.Compact`; Coq `Coquelicot.Compactness`
| M5 | *Yoneda lemma* (category theory, locally small categories) | mathlib4 `Mathlib.CategoryTheory.Yoneda`; Agda `agda-categories`; Idris2 community library
| M6 | *Deduction theorem / modus ponens closure* (propositional logic) | Coq stdlib `Classical`; Isabelle/HOL `Main`; mathlib4 `Logic.Basic`
| M7 | *Linearity of expectation* (finite discrete random variables) | mathlib4 `Probability.Basic`; Isabelle/HOL `Probability`
| M8 | *Rank-nullity theorem* (finite-dimensional linear maps) | mathlib4 `LinearAlgebra.Dimension`; Coq `mathcomp.algebra`; Isabelle HOL-Analysis
| M9 | *Unique factorization in a UFD* (integers as base case) | mathlib4 `RingTheory.UniqueFactorizationDomain`; mathcomp
| M10 | *Knot composition forms a commutative monoid* (connected sum with unknot as identity) | No standard formal-library port; KnotTheory.jl + Schubert's prime-decomposition theorem as reference
| M11 | *Pigeonhole principle* (finite case, arbitrary surjection) | mathlib4 `Combinatorics.Pigeonhole`; Coq `Finite`; Isabelle HOL-Library
| M12 | *Dominated convergence theorem* (Lebesgue integration) | mathlib4 `MeasureTheory.DominatedConvergence`; Coquelicot; Isabelle HOL-Analysis
| M13 | *Hahn-Banach extension theorem* (functional analysis) | mathlib4 `Analysis.NormedSpace.HahnBanach`; Isabelle HOL `Hahn_Banach`
| M14 | *Max-flow / min-cut duality* (graph theory) | Isabelle HOL `Flow_Networks`; no canonical mathlib port yet
|===

== Science

[cols="1,3,3",options="header"]
|===
| # | Theorem | Where to look for an existing proof to port

| S1 | *Conservation of energy from time-translation invariance of the Lagrangian* (Noether's theorem, classical-mechanics special case) | Coq `mathcomp-analysis`; Lean `mathlib4` `Mathlib.MeasureTheory.Function.LocallyIntegrable` (parts); HOL Light analysis library
| S2 | *Gauss's law from Maxwell's equations* (in differential form, vacuum case) | Coq `Coquelicot`; Lean `mathlib4` integration / divergence theorems; Isabelle/HOL physics archive
| S3 | *Second law of thermodynamics for an isolated system* (Boltzmann H-theorem, statistical-mechanics formulation) | Lean `mathlib4` `Mathlib.MeasureTheory.Integral.Lebesgue` + entropy; Isabelle/HOL `Probability`
| S4 | *Heisenberg uncertainty for position and momentum* (operator-algebra formulation, ⟨ΔxΔp⟩ ≥ ℏ/2) | Lean `mathlib4` `Mathlib.Analysis.InnerProductSpace.Basic`; Coq `mathcomp.analysis.normedtype`
| S5 | *Shannon source-coding theorem* (rate ≥ entropy is necessary) | Coq `infotheo`; Lean `mathlib4` `Mathlib.InformationTheory` (in progress); Isabelle/HOL `Information_Theory`
| S6 | *Law of mass action* (equilibrium condition for an elementary reaction, chemistry) | No standard formal-library port; derive from Gibbs-free-energy minimum
| S7 | *Lorentz-boost composition / relativistic velocity addition* (special relativity) | mathlib4 (in progress); Coq `mathcomp-analysis`
| S8 | *Hardy-Weinberg equilibrium* (stability under random mating, population genetics) | No standard formal-library port; derive from allele-frequency algebra
| S9 | *Chandrasekhar mass upper bound* (white-dwarf stars, astrophysics) | No standard formal-library port; derive from hydrostatic equilibrium + degenerate-gas equation of state
| S10 | *R_0 threshold for endemic-equilibrium existence* (compartmental epidemiology) | No standard formal-library port; derive from SIR / SIS stability analysis
|===

== Engineering

[cols="1,3,3",options="header"]
|===
| # | Theorem | Where to look for an existing proof to port

| E1 | *Lyapunov stability of a linear time-invariant system with negative-definite Lyapunov function* | Coq `Coquelicot.ODE`; Lean `mathlib4` linear-algebra parts; control-theory community libraries
| E2 | *Equivalence of two adder designs* (e.g. ripple-carry vs carry-lookahead, single bit-width) | HOL Light hardware verification archive; Coq `Bedrock`; Lean `mathlib4` (parts)
| E3 | *Bound on cantilever beam deflection* (Euler–Bernoulli, single point load) | Isabelle/HOL physics archive; community Coq `mechanics` projects
| E4 | *Correctness of merge sort* (output is a sorted permutation of the input) | Idris2 stdlib `Data.List.Sort`; Lean `mathlib4` `Mathlib.Data.List.Sort`; Coq `Coq.Sorting.Mergesort`; Agda `agda-stdlib` `Data.List.Sort`
| E5 | *Needham–Schroeder symmetric-key fix* (attack absent in the corrected protocol) | Isabelle/HOL `Auth/`; Coq `Bedrock` protocol verification; ProVerif transcripts as oracle
| E6 | *CSTR steady-state mass balance closure* (chemical engineering) | No standard formal-library port; first-principles balance equation
| E7 | *Carnot efficiency upper bound* (heat engine between two reservoirs) | Isabelle HOL-Thermo; derive from second-law / Clausius inequality
| E8 | *Nyquist-Shannon sampling theorem* (2W sufficient rate for bandlimited reconstruction, signal processing) | No standard formal-library port; `infotheo` may have adjacent results
| E9 | *Newton's method local quadratic convergence* (numerical analysis) | Isabelle HOL-Analysis; Coq `Coquelicot`
| E10 | *Weibull / bathtub-curve failure-rate bound* (reliability engineering) | No standard formal-library port; derive from Weibull hazard function
| E11 | *Kirchhoff voltage + current laws* (lumped-element circuits, power engineering) | Isabelle HOL `Circuits` (community); derive from charge + energy conservation
|===

== How a language toolchain ports this suite

. *Identify a qualifying prover* from `templates/QUALIFYING-PROVERS.adoc` (Idris2,
  Lean 4, Rocq, or Agda for v1).
. *For each suite entry* — find an existing proof in that prover's
  ecosystem (the third column above is a starter map). Port it to the
  language under audit's proof system *if* the language is itself a
  proof system; otherwise, use the language to *encode the statement
  and the proof obligation*, then discharge the obligation in the
  qualifying prover and link the artefact.
. *Wire each proof into nightly CI*. Every proof must be re-checked
  every 24 hours; any proof failure for more than 24 hours triggers
  immediate demotion per `TOOLCHAIN-READINESS-GRADES.adoc` §5.8.
. *Archive the proof corpus* under `.machine_readable/proofs/canonical-proof-suite/`
  in the language repo. Each proof gets a JSON sidecar with: prover
  used, proof file path, last-checked timestamp, kernel version,
  elapsed time, and the soundness-proof citation for the prover
  itself.
. *Publish a status table* in the language repo's README showing
  pass/fail for every suite entry. The table is itself a claim and
  is itself subject to the invariant-path doc-claims grounder.

== Versioning

* *v1.0* (2026-04-12) — initial set of 15 entries (5 mathematics + 5
  science + 5 engineering). Suite SHALL be reviewed and may be
  expanded annually.
* *v1.1 (proposed)* (2026-04-18) — 20 new entries in four priority
  tiers, taking the suite from 15 to 35 entries (14 mathematics + 10
  science + 11 engineering). Fills zero-coverage holes in logic
  (M6), probability (M7), chemistry (S6), chemical engineering (E6),
  knot theory (M10), relativity (S7), biology (S8), epidemiology
  (S10), reliability engineering (E10), and electrical power (E11).
  90-day co-signed review window opens at this commit; expansions
  take effect no earlier than 2026-07-17. Second-reviewer co-sign
  pending.
* When the suite is expanded, every existing A-grade component is
  re-evaluated against the new suite at the next assessment cycle.
  Components that no longer pass are demoted to grade B until they
  add the new entries.
* Suite expansions are co-signed by at least two reviewers (per the
  dual-use co-signing rule) and announced 90 days before they take
  effect, to give A-grade components a fair window to add the new
  entries.

== Notes on choice of entries

The 15 entries in v1.0 are deliberately *representative* not
*exhaustive*. The criterion for inclusion is:

. *Educational standing* — every working scientist or engineer has
  encountered the result and can recognise it.
. *Existing formal proofs* — at least one of the qualifying provers
  already has a machine-checked proof somewhere in its ecosystem,
  so the porting work is bounded.
. *Compositional independence* — no two entries reduce trivially to
  each other, so all 15 must be independently exercised.
. *Domain coverage* — five entries from each of mathematics, science,
  and engineering, so no domain dominates and a toolchain that can
  only express one kind of formal reasoning is excluded.

== Open invitation

The suite is open to challenge. If you think an entry is the wrong
choice, propose a replacement with a justification. If you think the
domain coverage is unbalanced, propose a rebalancing with evidence.
The suite earns trust by surviving critique, not by avoiding it.
