# Proof Obligations Map

## Purpose

RU is the universality engine.

This document states what must be present for each level of claim to be valid, and where that evidence lives in the engine.

The goal is to make every strong statement mechanically auditable.

## Objects

- Robust certificate schema:
  - `sources/ru/robust_certificate_schema.json`
- Robust certificate instances:
  - `sources/ru/robust_certificate_*.json`
- Bridge wrapper schema:
  - `sources/ru_bridge/bridge_certificate_schema.json`
- Bridge wrapper instances:
  - `sources/ru_bridge/bridge_certificate_*.json`
- Global report schema:
  - `sources/ru/global_universality_report_schema.json`
- Global reports:
  - `sources/ru/global_universality_report_*.json`

## Claim types and obligations

### Method universality (primary claim of the engine)

Claim:

- For every finite host reduction in scope, RU outputs either:
  - a contraction certificate object, or
  - an obstruction certificate object with a finite witness

Obligations:

- At least one example of each outcome type exists as audited objects.
- Each outcome has:
  - a bridge wrapper pointing to a robust certificate instance.

Where to check:

- `docs/Artifacts.md` for coverage by outcome type.
- `sources/artifact_index.json` for machine-readable coverage.

### In-class contraction universality (conditional)

Claim:

- For a fixed host reduction, if Doeblin and recurrence are certified on the active face, then projective contraction holds with explicit rate and robustness.

Obligations in a robust certificate:

- Tight core:
  - `tight_core.tight_edges`
  - `tight_core.tight_scc_summary` includes at least one aperiodic SCC relevant to the claim
- Doeblin:
  - `doeblin.word`, `doeblin.L`
  - `doeblin.delta > 0`
  - `doeblin.U_bound` and a stated margin model (`delta_prime_formula`, `U_prime_formula`)
- Recurrence:
  - `recurrence.details.rc1_holds = true`
  - a finite recurrence modulus is recorded (for example `gap_bound_B`)
- Rate pack:
  - `rate_pack.projective_diameter_bound`
  - `rate_pack.tau_unperturbed`
  - a rate formula and chosen evaluation tolerance (`eps_rate`)
- Robustness:
  - `eps_star.eps_A_star` and where relevant `eps_star.eps_c_star`

Where to check:

- Start with the real-host Fibonacci contraction artifact:
  - `docs/Fibonacci_Contraction_Certificate.md`
  - `sources/ru/robust_certificate_fibonacci_realhost_contraction.json`

### OG1 periodic-core obstruction

Claim:

- Strongest aperiodic universality is obstructed because the tight SCC is periodic.

Obligations:

- `tight_core.tight_scc_summary.aperiodic_scc_count = 0`
- `tight_core.tight_scc_summary.periods` contains a period greater than 1
- bridge wrapper classifies as obstruction

Where to check:

- Real-host Fibonacci OG1:
  - `docs/OG1_Fibonacci_PeriodicCore.md`
  - `sources/ru/robust_certificate_fibonacci_realhost_og1_period2.json`

### OG2 active-face inconsistency obstruction

Claim:

- No consistent active face exists because tight propagation forces contradictory supports.

Obligations:

- `tight_core.tight_scc_summary.aperiodic_scc_count >= 1`
- robust certificate notes OG2 mechanism in `tight_core.degeneracy_report.note`
- witness details exist in a host model file under `sources/ru_bridge/` that states the contradiction explicitly

Where to check:

- Real-host-derived OG2 (Ising + projection):
  - `docs/OG2_Ising_Projection_Inconsistency.md`
  - `sources/ru_bridge/og2_ising_projection_inconsistency_model.json`
  - `sources/ru/robust_certificate_og2_ising_projection_inconsistency.json`

### OG3 no-Doeblin-exists obstruction

Claim:

- No finite Doeblin block exists on the active cone; delta(w)=0 for all words.

Obligations:

- Doeblin section records `delta = 0`
- witness file states an invariant mechanism blocking full positivity for all products
- tight SCC can be aperiodic; obstruction is not OG1

Where to check:

- Real-host OG3 (Ising):
  - `docs/OG3_Ising_NoDoeblin.md`
  - `sources/ru_bridge/og3_ising_fusion_no_doeblin_model.json`
  - `sources/ru/robust_certificate_og3_ising_fusion.json`

### OG4 avoidable-Doeblin obstruction

Claim:

- A Doeblin block exists, but can be avoided forever along legal tight paths.

Obligations:

- Doeblin section has `delta > 0` for some word
- recurrence section has `rc1_holds = false`
- `recurrence.details.og4_avoidance_cycle` lists a finite avoidance cycle witness

Where to check:

- Real-host OG4 (Fibonacci idle channel):
  - `docs/OG4_Fibonacci_AvoidableDoeblin.md`
  - `sources/ru/robust_certificate_fibonacci_realhost_og4_idle_avoidable.json`

### Global report claims (chamberwise)

Claim:

- Across a parameter region, the engine provides an audited chamberwise classification.

Obligations:

- A global report object exists under `sources/ru/` and validates against schema.
- It lists:
  - region description
  - chamber classification
  - certificate index pointing to supporting robust certificates
  - explicit boundary obstruction chambers

Where to check:

- Reproducible report doc:
  - `docs/Global_Report_Fibonacci_Alpha.md`
- Report artifact:
  - `sources/ru/global_universality_report_fibonacci_alpha_chambers.json`
