# RU Theorem Anchor Integration

## Overview

RU is a certificate engine for universality and obstructions in constrained nonnegative propagation. Host structures supply finite inputs. Outputs are audited certificates or finite obstruction witnesses.

## Where the theorem submission lives

- `sources/theorem_submission_v19/rigidity_gapfree_global/`

Key compiled PDF:

- `sources/theorem_submission_v19/rigidity_gapfree_global/rigidity_gapfree_global_universality.pdf`

Key TeX components (selected):

- `canonical_normalization.tex` (normalization and potentials)
- `aubry_tight_core.tex` (tight core extraction and structure)
- `doeblin_word_search.tex` (finite witness search for Doeblin words)
- `doeblin_stability.tex` (robustness of Doeblin margins)
- `contraction_from_doeblin.tex` (Birkhoff/Hilbert metric contraction chain)
- `explicit_rate_pack.tex` (explicit rate formulas and constants)
- `global_universality_theorems.tex` (theorem statements)
- `global_universality_verification.tex` (verification workflow)
- `global_universality_artifacts.tex` (schema and artifact contracts)

The JSON schemas shipped in this engine match the theorem submission schemas:

- `sources/ru/robust_certificate_schema.json` matches the theorem engine schema
- `sources/ru/global_universality_report_schema.json` matches the theorem engine schema

## How certificates map to theorem hypotheses

A robust certificate instance is the proof-carrying object that records the hypotheses needed to invoke the theorem chain.

### Tight core

Certificate fields:

- `tight_core.tight_edges`
- `tight_core.tight_scc_summary`
- `tight_core.tight_gap_gamma`

Theorem role:

- identifies the active core on which minimizers concentrate
- ensures the combinatorial structure used by recurrence and Doeblin checks is stable

### Doeblin witness

Certificate fields:

- `doeblin.word`, `doeblin.L`
- `doeblin.delta`, `doeblin.U_bound`
- stability formulas `delta_prime_formula`, `U_prime_formula`

Theorem role:

- provides the minorization positivity needed for a uniform projective diameter bound

### Contraction and rate pack

Certificate fields:

- `rate_pack.projective_diameter_bound`
- `rate_pack.tau_unperturbed`
- `rate_pack.kappa_prime_formula`

Theorem role:

- applies Hilbert metric contraction (Birkhoff/Bushell chain) to obtain an explicit exponential rate

### Recurrence or obstruction

Certificate fields:

- `recurrence.details.rc1_holds`
- if false: `recurrence.details.og4_avoidance_cycle` (OG4 witness)
- periodicity is recorded in `tight_core.tight_scc_summary.periods` (OG1)

Theorem role:

- converts existence of a Doeblin block into unavoidable occurrence along tight paths, yielding global contraction
- or records finite witnesses for obstruction types

## How to audit the theorem linkage

- Start from a example artifact doc under `docs/Flagship_*.md`.
- Open its robust certificate instance under `sources/ru/`.
- Locate the corresponding theorem component in `sources/theorem_submission_v19/rigidity_gapfree_global/`.
- Verify that each predicate used in the theorem statement is represented as an explicit certificate field.

This keeps the engine honest: the theorem sources are present, and the certificate objects are the only source of strong claims.
