Referee Map And Checklist

Referee map and verification checklist

This subsection is a navigation aid for referees and readers who want to audit the logical spine and the “finite artifact” outputs without reading every narrative paragraph.
It does not introduce new claims; it points to where each claim is proved and to which finite outputs realize it.

Proof spine (what implies what).

The flagship statement is Theorem .
Its six bullets are proved by the theorems and algorithms listed in Table .

[t]
\centering
\small
{p{0.30\linewidth}p{0.24\linewidth}p{0.22\linewidth}p{0.18\linewidth}}
\toprule
Claim in Theorem & Load-bearing statement(s) & Primary file(s) & Artifact output(s) \\
\midrule
Decidable island (instance level) & Theorem & jsr_decidability_frontier.tex & obstruction_witness.json or robust_certificate.json + frontier_report.json \\
Gap-free contraction on tight dynamics & Theorem and rate formulas in \S & contraction_from_doeblin.tex, explicit_rate_pack.tex & rate_pack fields $(\tau,C,\kappa)$ \\
Contraction along minimizing trajectories & Theorem and the forcing chain & forcing_positive_density.tex, contraction_from_doeblin.tex & rate pack reused along minimizers \\
Minimizer-level frontier sharpening & Propositions and & minimizer_level_recurrence_converse.tex & finite palette constants $(L,\varepsilon_{\min},U_{\max})$ \\
Robustness radius and degraded constants & Sections — & robust_certificate_schema.tex, tight_core_stability.tex, doeblin_stability.tex, recurrence_robustness.tex & epsilon_star, degraded $(\tau’,C’)$ \\
Cover-or-atlas on compact families & Theorem , Proposition , Algorithm & global_universality_theorems.tex, region_net_certification.tex, global_universality_completion.tex & frontier_atlas_report.json (and optionally GlobalUniversalityCertificate/GlobalUniversalityReport) \\
\bottomrule

\caption{Referee map: where each flagship claim is proved and which finite output object realizes it.}

Fast audit checklist (artifact-first).

A reader can sanity-check the entire program by following the artifact contracts rather than the narrative.
The checklist below is phrased so each item can be verified by reading a single definition/lemma plus its associated algorithm.

• Reduction contract. Confirm the normalization/reduction assumptions and the tightness potential construction (Sections –).
• Tight core and periodicity. Verify SCC decomposition and aperiodicity labels are computed from the tight graph and are stable under a strict tightness gap (Section ).
• Doeblin witness. Verify the product-automaton search produces a concrete word $w$ and a face support certificate, or else returns an explicit failure witness (Section and Section ).
• OG2/OG3 witness format. Verify that face-map failure and Doeblin failure can be serialized as a finite inconsistency-cycle witness and either a cut witness or a product-automaton nonreachability certificate (Lemma , Lemma , Corollary ).
• Pipeline correctness. Verify the termination and soundness theorem that ties each branch to its witness lemma and the contraction branch to the Doeblin + recurrence contraction theorem (Section ).
• Conditional completeness on tight dynamics. Verify that uniform projective contraction on the induced tight subshift forces the existence of a Doeblin block and excludes avoidance cycles, yielding an equivalence between “uniform contraction” and “Doeblin + non-avoidance” on a tight SCC (Section ).
• Minimizer-level converse and closure. Verify that a strong, shift-uniform form of trajectory-level contraction forces a finite recurrence modulus for contractive blocks along minimizers (RC$^{\star}_{\min}$), and that this finite palette condition yields shift-uniform contraction with explicit constants extracted from the palette (Section , Propositions and ).
• Recurrence predicate. Verify how (RC1) is checked or refuted via the avoidance graph, and how this converts to a bounded-gap return modulus (Section and Section ).
• Rate pack. Verify the explicit contraction constant chain from Doeblin minorization to Hilbert-metric contraction, and the closed-form rate-pack extraction (Sections and ).
• Robustness. Verify that each predicate used in the pipeline is recorded with explicit margins and that the stability radius $\varepsilon^*$ is computed from those margins (Section ).
• Global-on-$\Theta$. Verify the net/region procedure and the cover-or-atlas termination statement, including the explicit work bound via the net size (Sections –).
• Necessity of the obstruction taxonomy. Confirm that each obstruction class OG1–OG4 is required by a concrete realizable instance that passes all earlier gates (Section , Proposition ).
• Sharpness of the recurrence layer. Verify that Doeblin existence does not imply contraction on all minimizers without a recurrence/forcing hypothesis (Section , Proposition ).
• Decidability and work bounds. Confirm the conservative complexity bounds for each subroutine and the global net-based work bound (Section ).

What “machine-checkable” means here.

The term is used in the limited sense that every decision branch is represented by a finite artifact and every quantitative claim in the certified regime reduces to checking finitely many inequalities whose inputs are recorded in that artifact.
The included JSON schemas specify the required fields and their semantics for the witness and certificate objects
(frontier_report_schema.json, frontier_atlas_report_schema.json, obstruction_witness_schema.json, og2_inconsistency_witness_schema.json, og3_cut_witness_schema.json, og3_nonreachability_certificate_schema.json, rate_pack_schema.json, robust_certificate_schema.json, global_universality_report_schema.json, and global_universality_certificate_schema.json).