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

= Foundations Readiness Grades (FRG)
:toc: left
:toclevels: 3

[cols="1,3", options="header"]
|===
| Field | Value

| Standard | Foundations Readiness Grades
| Version | 1.0
| Date | 2026-05-28
| Status | Active
| Author | Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
| License | PMPL-1.0-or-later (MPL-2.0 automatic legal fallback)
| Family | Rhodium Standard Repositories (RSR)
| Companion to | Toolchain Readiness Grades v1.0, Adoption Readiness Grades v1.0, Component Readiness Grades v2.2
| Relationship | Language-whole sibling tier (CRG = component, TRG = toolchain, ARG = adoption, FRG = mathematical foundations)
|===

== Abstract

Foundations Readiness Grades (FRG) is a strict-by-construction grading
scheme for the *mathematical foundations of a language*. It sits at
the language-whole tier of the estate grading hierarchy:

* *CRG* grades individual *components*.
* *TRG* grades the *toolchain*.
* *ARG* grades the language as a *thing someone can adopt*.
* *FRG* grades the language's *mathematical foundations*.

FRG uses the same letter grades as CRG, TRG, and ARG
(`X | F | E | D | C | B | A`) and the same worst-of-any-required-element
aggregation rule. The evidence required at each grade asks a different
question: *"is the language's typing discipline mathematically
grounded?"*. That is the question of FRG.

FRG is *independent* of TRG and ARG — a language can be FRG-C
(preservation theorem closed) while remaining TRG-D (toolchain still
incomplete), and vice versa. The single cross-axis coupling is
*ARG-A requires FRG ≥ B*: no language is judged school-grade adoptable
unless its foundations have crossed into layered, cross-prover
territory.

FRG distils estate practice. The four-layer redesign in ephapax
(L1 regions / L2 modality / L3 echo / L4 dyadic), the 10-level
TypeLL → PanLL → VCL-total type-safety lineage, the Echidna
neurosymbolic verifier, and the banned-constructs discipline are all
folded in as evidence rungs.

This standard is part of the Rhodium Standard Repositories (RSR)
family of standards maintained by hyperpolymath.

== 1. Scope

This standard applies to:

* Any programming language, query language, or domain-specific
  language whose *typing discipline* is intended to carry meaning —
  i.e. the language claims that well-typed programs have some
  recoverable property (safety, totality, resource discipline, etc.).
* The *language as a mathematical object* — the formal calculus that
  the implementation is purported to refine.

This standard does NOT apply to:

* Languages whose typing is *advisory* only (no soundness claim
  intended). Such languages are FRG-X by definition and should not
  attempt to grade themselves.
* Toolchain components (use TRG).
* Adoption surfaces (use ARG).
* Repository hygiene (use RSR).

=== 1.1 Per-language extension

Each adopting language SHOULD publish a `spec/FRG-PROFILE.adoc` in
its own repo that tightens this baseline with language-specific
obligations. A profile MAY only tighten, never loosen. Examples of
valid tightening:

* AffineScript: "Grade C requires the formalised QTT fragment to be
  closed under the affine restriction (no q=ω escape via the affine
  rule)."
* Ephapax: "Grade C requires preservation closed *per layer*
  (preservation_l1, preservation_l2, preservation_l3) with the
  cross-layer composition closed under explicit invariants —
  not via patched single-layer admits."
* VCL-total: "Grade B requires Cross-modal consistency proofs over
  ≥ 3 of the 8 octad modalities."
* My-lang: "Grade C requires the calculus's borrow-checker to be
  modelled in the formal calculus, not stubbed out."

The profile shape is defined in `templates/FRG-PROFILE-TEMPLATE.adoc`.

== 2. Normative References

* *CRG v2.2* — Component Readiness Grades. FRG inherits CRG's letter
  vocabulary and release-stage mapping.
* *TRG v1.0* — Toolchain Readiness Grades. FRG inherits TRG's
  `qualifying-provers` list (Idris2, Lean 4, Rocq, Agda) and TRG's
  `banned-constructs` list verbatim.
* *ARG v1.0* — Adoption Readiness Grades. ARG-A requires FRG ≥ B.
* *RSR* — Rhodium Standard Repositories. FRG-graded language repos
  MUST be RSR-compliant at the level required by TRG at the same
  grade.
* *TypeLL → PanLL → VCL-total* — The 10-level type-safety lineage.
  FRG grades cite the achieved level explicitly from grade D upward.
* *Echidna* — The estate's neurosymbolic proof verifier. Required in
  CI from FRG-A.

== 3. Required Foundations Surfaces

FRG grades the *language as a mathematical artefact*. A "foundations
surface" is one of the public evidence classes that establishes the
language's mathematical grounding. The required surfaces are:

=== 3.1 Mathematical core (M)
* *M1* Abstract syntax formalised in a qualifying prover
* *M2* Typing judgment formalised in a qualifying prover
* *M3* Operational (or denotational) semantics formalised in a
  qualifying prover
* *M4* Preservation theorem *statement* present in the formalisation
* *M5* Progress theorem *statement* present in the formalisation

=== 3.2 Proof landings (P)
* *P1* Preservation theorem *closed*: 0 admits, 0 axioms, 0 sorries
  (zero banned constructs in the proof)
* *P2* Progress theorem *closed*
* *P3* Counterexample-driven regression suite: known unsound
  variants are encoded as `Qed`'d counterexample lemmas (ephapax
  `Counterexample.v` is the canonical example)
* *P4* Layered / orthogonal decomposition: independent concerns
  (structural / region / modality / effect / echo) are separated
  into distinct judgments with explicit cross-layer invariants

=== 3.3 Verification rigor (V)
* *V1* Single qualifying prover used for M1-M5
* *V2* Cross-prover replication ≥ 2 (the central preservation
  theorem is closed in a second qualifying prover)
* *V3* Cross-prover replication ≥ 3
* *V4* Echidna neurosymbolic verifier integrated in CI as a gate

=== 3.4 TypeLL classification (L)
* *L1* Syntactic parsability (parser accepts the input)
* *L2* Well-formedness (structure matches the grammar)
* *L3* Schema conformance (references resolve to declared entities)
* *L4* Type compatibility (operator arities and types align)
* *L5* Nullability tracking (`NULL` propagates explicitly)
* *L6* Injection resistance (parameterisation as type-level invariant)
* *L7* Linear types (QTT q=1 on resources)
* *L8* Session types (state-indexed protocols)
* *L9* Effect systems / Modal types / Proof-carrying code
* *L10* Quantitative type theory / cross-cutting

For each language, the FRG profile cites the highest level achieved
and *with evidence*. Claiming L7 without a linear-typing soundness
proof is not L7; it is L4 with linear-typing aspirations.

=== 3.5 Banned constructs (B)
* *B0* Zero `believe_me`, `Admitted`, `sorry`, `postulate`,
  `unsafeCoerce`, `Obj.magic`, `unsafePerformIO`, `assume`, `axiom`,
  or equivalent in proof code (inherited from TRG)
* *B1* Per-prover banned-construct lint runs in CI

=== 3.6 Operational equivalence (O)
* *O1* Operational checker / type checker / borrow checker tested
  against the formal judgment
* *O2* Differential testing: random programs are well-typed by the
  implementation if and only if they are well-typed by the formal
  judgment (or a documented gap is recorded)
* *O3* Reference implementation: a small, audit-friendly reference
  implementation exists alongside the production implementation

=== 3.7 Kernel-soundness contribution (K)
* *K1* Upstream contribution to one of the qualifying provers
  (Idris2, Lean 4, Rocq, Agda) within the last 12 months — proof
  library, tactic, soundness fix, or curated counterexample suite

== 4. Grade Definitions

=== 4.1 Grade X — No formal artefact

*Release stage:* None
*Stability posture:* No claim
*Honest shorthand:* `no-formalisation`

The language has no formalisation in any qualifying prover. The
typing rules exist (if at all) only as informal prose or as the
implementation's source code. No evidence rung from §3.1 is met.

*Evidence required:* None. This is the absence of foundations
evidence.

*Common position:* Most languages live here at birth. Honest.

=== 4.2 Grade F — Provably wrong, unmarked

*Release stage:* Reject, deprecate, or delegate
*Stability posture:* Actively misleading
*Honest shorthand:* `false-claim`

A formalisation exists *and* one of the central theorems
(preservation, progress, soundness) is *known to be false* under the
current formulation, *and* the formalisation is not marked as
archaeology / superseded / counterexample-witnessed. The language
is claiming foundations it does not have.

Two examples make the rung concrete:

* A `Theorem preservation` closed by an `Axiom` whose statement is
  itself the conclusion being proved (circular discharge).
* A calculus whose `formal/` contains a counterexample lemma
  (`Counterexample.v` style) closed by `Qed`, demonstrating that
  the central theorem is false as stated, *without* the legacy
  `preservation` statement being marked superseded by a redesign
  document.

FRG-F is rare and important. The grade exists so that a language
can be honestly de-promoted without having to silently invalidate
historical claims. Ephapax's pre-redesign `formal/Semantics.v`
state (preservation stated, `Counterexample.v` `Qed`'d, no
redesign locked in) was FRG-F by this definition for the days
before PRESERVATION-DESIGN.md was committed; the redesign
*evacuates* the F-grade by reclassifying the legacy preservation
statement as archaeology and committing to a layered redesign as
canonical.

*Evidence required to assign F:*
* Counterexample present in the proof corpus, `Qed`'d.
* Original theorem not marked superseded, archaeological, or
  conditional on a recorded redesign plan.
* No layered/sequenced redesign document committed.

*Evacuation path from F to D:* Mark legacy as archaeology, commit a
canonical redesign document (e.g. `PRESERVATION-DESIGN.md`), and
begin the work — at which point the language re-enters D.

=== 4.3 Grade E — Well-formedness only  *(pre-alpha)*

*Release stage:* Pre-alpha
*Stability posture:* Syntactic ground only
*Honest shorthand:* `well-formed`

The language has a formalisation that establishes well-formedness:
the abstract syntax and typing judgment are encoded in a qualifying
prover, but no preservation or progress claim has been stated
formally yet. No banned constructs in what exists.

*Smell test:* "We've written down the rules in Coq."

*Evidence required (worst-of, all MUST be PASSED):*

* TRG ≥ E for the formalisation tooling (the prover, build, CI)
* M1 (abstract syntax formalised in a qualifying prover)
* M2 (typing judgment formalised in a qualifying prover)
* B0 (zero banned constructs in formalisation)
* TypeLL ≥ L2 (well-formedness) declared in the FRG profile
* Formalisation lives in the canonical repo `formal/` directory and
  is built by CI

=== 4.4 Grade D — Preservation stated  *(pre-alpha+)*

*Release stage:* Pre-alpha+
*Stability posture:* Foundations begun
*Honest shorthand:* `preservation-stated`

The language has stated the central preservation/progress theorems
in the formalisation. Operational or denotational semantics is
formalised. Admits are explicitly *tracked* (a PROOF-NEEDS.md
catalog enumerates every open goal). The work is honest about what
is and isn't done; it is *not* yet closed.

*Smell test:* "We know what we're trying to prove."

*Evidence required (all E + the following):*

* M3 (operational or denotational semantics formalised)
* M4 (preservation theorem *stated*)
* M5 (progress theorem *stated*)
* TypeLL ≥ L4 declared with evidence
* PROOF-NEEDS.md (or equivalent) lists every open goal with file,
  line, and the conjecture's role
* Each open goal is either:
** Explicitly `Admitted` / `sorry` with a comment citing the
   PROOF-NEEDS.md entry, OR
** Closed via `Qed`
+
*No silent admits.* Banned-construct lint forbids untracked
admits.

=== 4.5 Grade C — Preservation closed  *(alpha gate)*

*Release stage:* Alpha
*Stability posture:* Core soundness established
*Honest shorthand:* `core-closed`

The central preservation and progress theorems are *closed* in a
qualifying prover with zero admits, zero axioms, zero sorries, and
zero banned constructs throughout the proof tree. PROOF-STATUS.a2ml
exists and is current. This is the *alpha gate* of FRG — below C
the language's foundations are aspirational.

*Smell test:* "If the formalisation says it's typeable, it stays
typeable through evaluation."

*Evidence required (all D + the following):*

* P1 (preservation theorem closed: 0 admits, 0 axioms, 0 sorries)
* P2 (progress theorem closed)
* TypeLL ≥ L6 declared with evidence
* PROOF-STATUS.a2ml present and current in `formal/`
* B0 + B1 (zero banned constructs *and* CI lint actively enforcing)
* TRG ≥ C for the formalisation tooling
* Diversity-metrics check: the formalisation has been peer-reviewed
  by ≥ 1 reviewer outside the founder's immediate collaborators

=== 4.6 Grade B — Layered + cross-prover  *(beta gate)*

*Release stage:* Beta
*Stability posture:* Robust foundations
*Honest shorthand:* `layered-cross-prover`

The formalisation has matured beyond a single-layer proof tree.
Distinct concerns (structural discipline / region capability /
modality / echo / dyadic interaction, or the equivalents for the
language) are factored into independent layers with explicit
cross-layer invariants. Counterexample-driven regression catches
known-false variants. The central theorem is replicated in a
second qualifying prover. The language is genuinely *robust*
against the failure modes that motivated formalisation in the first
place.

*Smell test:* "If we strengthen one concern, the proof of the
others doesn't have to change."

*Evidence required (all C + the following):*

* P3 (counterexample regression suite: ≥ 3 `Qed`'d
  counterexample lemmas establishing what the calculus does NOT
  prove)
* P4 (layered / orthogonal decomposition with documented
  cross-layer invariants)
* V2 (cross-prover replication ≥ 2 for the central preservation
  theorem)
* O1 (operational checker tested against the formal judgment for
  ≥ 1000 worked examples)
* TypeLL ≥ L8 declared with evidence
* TRG ≥ B for the formalisation tooling
* External (non-collaborator) single-party review of the
  formalisation completed

=== 4.7 Grade A — Verified + cross-validated  *(stable)*

*Release stage:* Stable
*Stability posture:* Field-grounded
*Honest shorthand:* `kernel-grade`

The language's foundations are field-grounded. Cross-prover
validation has reached three qualifying provers. The Echidna
neurosymbolic verifier is integrated as a CI gate. The
implementation has been certified against the formal judgment via
differential testing at scale. The language has contributed
back to a qualifying prover's kernel-soundness ecosystem within
the last 12 months. Past FRG-A is not part of this scheme —
what lies beyond is a *cultural phenomenon* (a research
programme), not a property of the language. FRG-A is the cap.

*Smell test:* "Three independent prover communities agree it's
sound."

*Evidence required (all B + the following):*

* V3 (cross-prover replication ≥ 3 for the central preservation
  theorem)
* V4 (Echidna in CI as a required gate; failures block merge)
* O2 (differential testing: random programs agree between the
  formal judgment and the implementation; ≥ 100k tests run in CI
  rolling window)
* O3 (audit-friendly reference implementation present alongside
  the production implementation)
* TypeLL = L10 (cross-cutting) declared with evidence
* K1 (kernel-soundness contribution to a qualifying prover within
  the last 12 months)
* TRG = A for the formalisation tooling
* 5-nines on the standing priority axes (TRG §5.7.5 adopted
  verbatim)
* Unanimous 6+6 (humans + LLMs) signoff per TRG
  `templates/A-GRADE-LLM-PANEL.adoc`

=== 4.8 Demotion on loss  *(critical)*

Loss of any A-grade gate (kernel-soundness contribution lapses
past 12 months, Echidna CI gate disabled, cross-prover replication
falls below 3, differential testing window collapses, signoff
rescinded, banned construct introduced in any layer) *immediately*
demotes the language. There is no grace period. Same rule as TRG
§5.8 and ARG §4.8.

Specific FRG demotion triggers worth naming explicitly:

* *Any single `Admitted`, `sorry`, or banned construct introduced
  into the proof tree* — instant demotion to the highest grade
  whose evidence still holds.
* *Counterexample lemma broken / removed* — demotion proportional
  to which property the counterexample was witnessing.
* *Cross-prover replication falls behind the main calculus by
  more than one release* — demotion from A to B (V3 floor lost),
  or from B to C (V2 floor lost), as applicable.

== 5. Aggregation Rule

FRG aggregation is *worst-of-any-required-foundations-surface*. The
language's FRG grade is the *lowest* grade achieved across all
required foundations surfaces at the candidate grade's evidence floor.

*No averaging. No weighting. No partial credit.*

A language with M1-M5 + P1-P2 at B (layered, cross-prover) but
TypeLL only at L5 is *FRG-D*, not "FRG-B-with-typing-gap". The
honest grade tells the maintainer what to focus on next.

== 6. Definitions

=== 6.1 "Qualifying prover"

Inherited verbatim from TRG. Currently: Idris2, Lean 4, Rocq
(formerly Coq), Agda. A formalisation in any other system (Isabelle,
F*, Twelf, etc.) is admissible by per-language profile tightening
but does not satisfy the baseline.

=== 6.2 "Banned constructs"

Inherited verbatim from TRG. Includes (non-exhaustive):
`believe_me`, `Admitted`, `sorry`, `postulate`, `unsafeCoerce`,
`Obj.magic`, `unsafePerformIO`, `assume`, `axiom`, equivalents in
other provers, and any compile-time-evidence-erasure construct
acting as a proof escape hatch.

A *tracked admit* (an `Admitted` whose statement is enumerated in
PROOF-NEEDS.md with a discharge plan) is permitted at grades D and
below. It is forbidden at grades C and above (the C-gate is "0
admits, 0 axioms, 0 sorries").

=== 6.3 "Closed theorem"

A theorem is *closed* iff:

1. Its statement is fully ground (no remaining proof obligations).
2. Its proof tree contains zero banned constructs (per §6.2).
3. Every transitively-used lemma is itself closed by this
   definition.

A theorem whose proof depends on an `Axiom` whose statement is
not itself a closed theorem is *not closed*.

=== 6.4 "Layered decomposition"

A formalisation is *layered* iff distinct mathematical concerns
are factored into separate judgments such that:

1. Each layer's preservation theorem can be stated independently
   of the others.
2. Cross-layer composition is explicit (a named composition
   lemma, not implicit in the term structure).
3. Strengthening one layer does not require re-proving the others.

The ephapax four-layer redesign (L1 regions / L2 modality /
L3 echo / L4 dyadic) is the canonical example, encoded in
`formal/PRESERVATION-DESIGN.md`.

=== 6.5 "Counterexample regression suite"

A collection of *positive* lemmas (closed by `Qed` / equivalent)
that demonstrate what the calculus does *not* prove. The canonical
example is ephapax's `formal/Counterexample.v`, in which three
`Qed`'d lemmas establish that the original preservation statement
is *false*, motivating the four-layer redesign.

A counterexample lemma is `Qed`'d positive content: it proves the
*existence* of a configuration the calculus must not type. The
calculus is then strengthened to exclude that configuration.

=== 6.6 "Echidna in CI"

The hyperpolymath neurosymbolic proof verifier is invoked as a CI
gate on every PR that touches `formal/`. Failures block merge.
This requires both Echidna ≥ TRG-C and the language's formalisation
to expose its judgments to Echidna's verification protocol.

=== 6.7 "Differential testing"

Random programs are generated (per a documented generator) and
fed to both the implementation's type checker and the formal
judgment's executable interpretation. Disagreements are recorded
as bugs and resolved before merge. A 100k-test rolling window
implies running ≥ 100k tests per release cycle.

== 7. Per-Language Profile Mechanism

Each adopting language publishes `spec/FRG-PROFILE.adoc` in its repo,
following `templates/FRG-PROFILE-TEMPLATE.adoc`. The profile:

* States the current honest grade (X / F / E / D / C / B / A).
* Cites the evidence for each criterion (file paths, theorem names,
  commit SHAs, PROOF-NEEDS.md entries, PROOF-STATUS.a2ml lines).
* Records the path to the next grade with concrete next steps,
  including specific open theorems and their location.
* Carries an iteration history with dates and previous grades
  retained.
* MAY tighten the baseline (add language-specific obligations).
* MUST NOT loosen the baseline.

A language's FRG-PROFILE.adoc is itself a *VCL-total proposition* —
its content is `DECLARE`'d to VeriSimDB on each commit. Drift
between the profile's claimed grade and the underlying proof state
(any new admit, removed `Qed`, etc.) is detected by VeriSimDB's
cross-modal drift monitor and surfaces as a *foundations-stale*
alert.

== 8. Self-Assessment

The FRG specification's own FRG grade is *not applicable* — FRG
grades languages, not specifications. The FRG specification is
graded by the CRG of the standards repo and by the TRG of the
documentation tooling.

The FRG document set is self-assessed against its own
internal-consistency criteria in `SELF-ASSESSMENT.adoc`.

== 9. Conformance

A language conforms to FRG if:

1. Its FRG grade is recorded in `spec/FRG-PROFILE.adoc` in its repo.
2. The grade is supported by the evidence described in §4 for that
   grade and every grade below it.
3. The profile is reviewed at least once per release cycle, and on
   any demotion event within 7 days.
4. The aggregation rule of §5 is respected (worst-of, no averaging).
5. Demotion is recorded immediately on loss of any required
   evidence (§4.8).
6. Per-commit attestations are emitted to VeriSimDB at grade C and
   above.
7. The language's CI runs the banned-construct lint (§6.2) and
   blocks merge on violation from grade D upward.

== 10. Open Questions / Versioning

This is FRG v1.0. Likely v2 changes once cross-prover ecosystem
matures:

* The "≥ 3 qualifying provers" floor at A is *plucked from
  intuition*: it is the minimum number that breaks any single-prover
  ecosystem capture. May need to drift up if the qualifying-prover
  set grows (Twelf, F*, Isabelle adoptions are under discussion).
* The "100k differential tests per release" at A is order-of-
  magnitude reasoning; the exact number should be re-baselined
  against the first FRG-A candidate's actual coverage.
* The "kernel-soundness contribution within 12 months" at A is
  intentionally narrower than mere bug-fix contribution — it
  requires soundness-relevant upstream work. May be too narrow;
  re-baseline once tested.
* The relationship to Echidna is currently encoded as a hard
  CI-gate at A. This may relax to "any production neurosymbolic
  verifier" if a second one emerges in the estate or upstream.
* TypeLL = L10 at A is currently a hard gate. May be relaxed for
  domain-specific languages whose semantics genuinely require less
  (a configuration language may legitimately cap at L6).

== 11. Honest Comparison to Real-World Software Standards

To the author's knowledge, FRG-A is not matched by any language
standard currently in use. The closest comparators:

* *CompCert / CakeML* — FRG-A by FRG's criteria. End-to-end
  verified compilers; cross-prover replicated in part;
  kernel-soundness contributions upstream. The model.
* *Idris2 (the language, not its formalisation)* — FRG-B. The
  language is formally grounded (QTT), preservation is closed for
  the core fragment, but cross-prover replication is incomplete.
* *Rust (2024)* — FRG-D leaning C. RustBelt formalised a fragment;
  preservation closed for that fragment in Coq; cross-prover
  replication absent; the full language exceeds the formalised
  fragment.
* *Haskell (2024)* — FRG-D. System F + extensions formalised in
  several places; preservation for the *full* GHC dialect is open;
  the production compiler is well past what the formalisation
  covers.
* *Most "I built a type system" weekend projects* — FRG-X or
  FRG-E. Honest.

The author expects approximately *one* hyperpolymath language to
reach FRG-C in year one (ephapax, post-four-layer-redesign),
approximately *zero* to reach B, and *zero* to reach A. That is the
correct order of magnitude. If FRG-A becomes easy to hit, the bar
is wrong and the standard MUST be raised.

This standard is open to challenge. If you think the bar is too
low, specify what evidence class, foundations surface, or
verification-rigor requirement is missing.

== 12. Machine-Readable Grade Declaration

Languages using FRG SHOULD include in their `READINESS.md`:

[source,markdown]
----
**Current FRG Grade:** D
**Current ARG Grade:** D
**Current TRG Grade:** D
**Current CRG Grade:** C
**Current RSR Compliance:** FULL
----

This line is parsed by `just frg-grade` and `just frg-badge` from
`rsr-template-repo`.

== Revision History

[cols="1,1,1,3", options="header"]
|===
| Version | Date | Author | Changes

| 1.0 | 2026-05-28 | Jonathan D.A. Jewell | Initial release. FRG fills the mathematical-foundations tier (CRG = component, TRG = toolchain, ARG = adoption, FRG = foundations). Grade vocabulary X-A inherited from CRG/TRG/ARG. Worst-of aggregation and immediate demotion inherited from TRG. Cross-axis coupling: ARG-A requires FRG ≥ B. TypeLL 10-level lineage folded into the L surface. Banned-constructs and qualifying-provers inherited from TRG verbatim.
|===
