Proof Obligation Index

This section provides the introductory context and foundational overview for this document.

Purpose

This index decomposes theorem targets into explicit obligations.

Obligation Classes

Class	Meaning
DEF	missing or incomplete definition
HYP	hypotheses need specification
INV	invariant needs statement
MAP	mapping/functor/translation needs definition
PROOF	proof step needed
TEST	implementation test needed
REVIEW	external review needed
SOURCE	source dependency needs verification

Index

Obligation ID	Target	Class	Description	Status
PO-FAB-001	Fabricon Minimal Relational Unit	DEF	define Fabricon tuple semantics	CLOSED (Fabrica.Fabricon)
PO-FAB-002	Fabricon Minimal Relational Unit	PROOF	conjugate involution & symmetry	CLOSED (Fabrica.Fabricon)
PO-DFT-001	DFT Invariant Morphisms	DEF	define discrete state admissibility	CLOSED (Fabrica.InvariantEngineering)
PO-DFT-002	DFT Invariant Morphisms	PROOF	admissibility under composition & inversion	CLOSED (Fabrica.InvariantEngineering)
PO-FQFT-001	FQFT Scale Transition	PROOF	algebraic first resolvent identity	CLOSED (Fabrica.FQFT)
PO-FQFT-002	FQFT Scale Transition	PROOF	scale covariance & Dirichlet bound	CLOSED (Fabrica.FQFT)
PO-PGP-001	Pasev Gauge Principle	PROOF	gauge identity, composition & orbit invariance	CLOSED (Fabrica.PGP)
PO-OBS-001	Observer Monad	PROOF	left/right identity & associativity	CLOSED (Fabrica.ObserverMonad)
PO-REAL-001	Realica Infinite Stabilization	PROOF	fixed-point idempotence & sequence convergence	CLOSED (Fabrica.Realica)
PO-PHYS-001	Continuum Recovery & Predictions	REVIEW	prospective empirical detector tests	OPEN (ACTIVE_P4_SEALS = 0)

See the Lean 4 Formalization Roadmap for verified Lean 4 proof scripts.