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

This checklist is the internal "HOL-grade" filter for papers whose core value
depends on mechanized reasoning, theorem precision, and proof/artifact parity.
Use it after the stable release gate and before venue-specific packaging.

It is intentionally stricter than a generic preprint bar. Passing this checklist
does not guarantee acceptance at any specific venue; failing it means the work
should not be presented as proof-heavy or theorem-grade yet.

See also link:PREFLIGHT.adoc[Publication Pre-Flight Standard].

toc::[]

== 1. Core Theorem Posture

[cols="1,3"]
|===
| Check | Requirement

| Central claims are theorem-sized
| The abstract, introduction, and conclusion state the actual theorem-level contribution, not a vague safety impression.

| Claim vocabulary is disciplined
| Use "prove" only for mechanized results, "show" for empirical evidence, and "conjecture" for unproven statements.

| Parameters and scope are explicit
| Every central theorem states its fragment, semantic model, trust boundary, and side conditions.

| Assumptions are ledgered
| Crypto assumptions, solver assumptions, parser totality assumptions, oracle models, and trusted FFI boundaries appear in one explicit assumption ledger.
|===

== 2. Mechanization Quality

[cols="1,3"]
|===
| Check | Requirement

| Proof artifacts compile cleanly
| Idris2/Lean4/Agda/Coq files build cleanly with no open holes, placeholders, or banned escape hatches.

| No hidden escape hatches
| `believe_me`, `assert_total`, `unsafeCoerce`, `Obj.magic`, `sorry`, `Admitted`, and `postulate` are absent except for documented axioms that the paper names explicitly.

| Central claims are mechanized
| Every theorem that carries the paper's contribution is represented in the proof artifact, not left as prose.

| The mechanization is project-specific
| Proof files are not template scaffolding, copied examples, or empty wrappers that only give the appearance of rigor.
|===

== 3. Paper / Proof / Artifact Parity

[cols="1,3"]
|===
| Check | Requirement

| The theorem statement matches
| Quantification, hypotheses, and conclusions in the paper match the mechanized theorem without omitted side conditions.

| The implementation boundary is honest
| The paper distinguishes the proven core from unchecked tooling, runtime glue, external libraries, and foreign interfaces.

| Examples are representative
| Worked examples and case studies exercise the same fragment and assumptions described by the proofs.

| Benchmarks and tests do not outrun the theory
| Performance, integration, or safety claims outside the proven core are clearly labelled as empirical rather than proven.
|===

== 4. Reproducibility For Reviewers

[cols="1,3"]
|===
| Check | Requirement

| Build path is documented
| A reviewer can find the commands needed to build proofs, run tests, and regenerate paper tables or counts.

| Reviewer time is bounded
| The strongest claims can be checked in a reasonable session without private infrastructure or hidden steps.

| Supporting evidence is in repo
| Proof logs, benchmark commands, metadata, and bibliography are colocated with the paper or linked unambiguously.

| Release state is honest
| Repository maturity metadata, README wording, and paper wording all describe the same current release state.
|===

== 5. Bibliography And Comparison Discipline

[cols="1,3"]
|===
| Check | Requirement

| Related work is real and comparable
| Comparison claims cite real systems and specify the exact axis of comparison.

| Novelty claims are defendable
| "First" or "no prior work" statements are supported by a serious literature check, not intuition.

| Proof audience expectations are met
| Foundational and recent formal-methods references are present where they materially shape the claim.
|===

== Decision Rule

**GREEN**::
All central theorem claims are mechanized, parity is clean, and the paper can
be defended to a proof-heavy audience without soft wording or hidden assumptions.

**YELLOW**::
Mostly there, but 1-3 repairable issues remain: missing side conditions,
mislabelled claims, incomplete bibliography cleanup, or weak proof/artifact
cross-linking.

**RED**::
The mechanization does not yet carry the paper's core contribution, the proof
story and implementation story diverge, or the theorem posture would collapse
under close reading.
