feat(trg-cps): propose v1.1 suite expansion — 20 new entries across 10 uncovered disciplines

Bump TRG Canonical Proof Suite from v1.0 to v1.1 (proposed), adding 20
new rows in the M / S / E tables:

Mathematics (+9): M6 deduction theorem (logic), M7 linearity of
expectation (probability), M8 rank-nullity (linear algebra), M9
unique factorization (number theory beyond primes), M10 knot
composition commutative monoid (knot theory), M11 pigeonhole
(combinatorics), M12 dominated convergence (measure theory), M13
Hahn-Banach (functional analysis), M14 max-flow min-cut (graph
theory).

Science (+5): S6 law of mass action (chemistry), S7 Lorentz velocity
addition (special relativity), S8 Hardy-Weinberg equilibrium
(biology), S9 Chandrasekhar mass bound (astrophysics), S10 R_0
threshold (epidemiology).

Engineering (+6): E6 CSTR steady-state mass balance (chem eng), E7
Carnot efficiency bound (thermo cycles), E8 Nyquist-Shannon sampling
(signal processing), E9 Newton's method quadratic convergence
(numerical), E10 Weibull bathtub bound (reliability), E11 Kirchhoff
laws (electrical power).

Rationale: v1.0 gap analysis found zero coverage in logic,
probability, chemistry, chem eng, knot theory, relativity,
epidemiology, reliability, and power. The 20 new entries were
selected on the same inclusion criteria as v1.0 (educational
standing + existing formal proofs where possible + compositional
independence + domain coverage).

Governance: the spec's §versioning section self-mandates a co-signed
90-day review window for suite expansions, announced before
taking effect. This commit starts that 90-day window. Expansions
take effect no earlier than 2026-07-17. Second-reviewer co-sign
pending. Until the window closes and co-signatures are in place,
v1.1 entries are labelled "proposed" and do not affect any
toolchain's grade.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

Author: hyperpolymath

toolchain-readiness-grades/templates/CANONICAL-PROOF-SUITE.adoc

@@ -2,8 +2,8 @@
 // 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.0 — gate to leave grade E
-:date: 2026-04-12
+: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
@@ -40,6 +40,15 @@ A toolchain passes the M/S/E-CPS iff:
 | 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
@@ -53,6 +62,11 @@ A toolchain passes the M/S/E-CPS iff:
 | 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
@@ -66,6 +80,12 @@ A toolchain passes the M/S/E-CPS iff:
 | 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
@@ -95,6 +115,15 @@ A toolchain passes the M/S/E-CPS iff:
 * *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