ora-0201

A Claim ledger

The accompanying Lean audit classifies all 89 theorem-like environments in the manuscript. Sixteen machine-checked kernels currently support 28 of those claims: seven are direct finite or logical theorems, while twenty-one inherit a checked kernel but still require their categorical specialization to be encoded. The audit assigns the remaining claims to routine Mathlib reduction, new categorical interfaces, higher-categorical infrastructure, analysis/probability developments, or externally sourced mathematics.

In particular, Lean verifies the (N-1) informative-response argument, iteration of settled observer answers, preservation of registered independent blocks, invariance under constant loss shifts, finite composable transport, observational non-identifiability, the two-arm bandit counterexample, observer-based enforcement failure, the commuting-update diamond, and conditional geometric amplification. It also checks finite hypothesis restriction, probe refinement, causal down-set minimality, observational quotients, and scalar comparator monotonicity. These certificates do not yet formalize hypothesis fibrations, tangent comparison cells, or homotopy-coherent semantics; the ledger therefore states those boundaries explicitly.

Lean status	Claims	Publication meaning
Directly verified	7	ORACLE theorem in the checked project
Kernel checked	21	categorical specialization remains
Mathlib reduction	7	local definitions remain
Categorical interface	21	new domain encoding required
Higher infrastructure	11	tangent, homotopy, or sheaf layer
Analysis/probability	20	substantial analytic development
Externally sourced	2	classical theorem with citation

Claim	Status	Boundary
ORACLE categorical prior	Definition	Universe-relative sub-2-category of \(\mathbf{Cat}\); targets learned only up to a declared observational equivalence
Generatively presented world	Definition	World category, learned sketch, preservation doctrine, completed algebraic theory, and structure-preserving interpretation are distinct target levels
Categorical presentation modes	Definition	Sound transcript category, declared fairness, and an explicit distinction between positive witnesses and certified negative facts
ORACLE hypothesis fibration	Definition	Contravariant category of transcript-indexed consistent models and a coherent section along the observed presentation
Categorical identification in the limit	Definition	Specified hypothesis class, presentation protocol, query language, and behavioral or explanatory convergence criterion
Observational extension obstruction	Proposition	A finite transcript admitting two models that disagree on an admissible query
Finite categorical identification	Proposition	Known finite inventory and fair active access to domain, codomain, identity, composition, and equality tables
Finite conservative doctrine stabilization	Theorem	Finite doctrinal query quotient, realizable retained target, eventually separating probes, and conservative transport on monotonically settled queries; literal base stabilization additionally requires a unique minimal representing doctrine and a stable selection rule
Query-relative UOCL specialization	Definition	Explicit hypothesis category, presentation, query doctrine, observational quotient, non-anticipatory update, and success criterion
Established-method specialization criterion	Proposition	Reindexing-compatible updates induce a UOCL instance; persistent UOCL also requires conservative transport of settled query answers
Theory-bearing UOCL	Definition	Learns generators, relations, completion, and functorial model semantics; generative adequacy does not imply minimality, completeness, or faithfulness
Collider probe refinement	Proposition and running example	Restriction of exact response-functor equivalence along nested probe subcategories; approximate empirical quotients need not be monotone
Semantic presentation invariance	Proposition	Naturally equivalent model categories cannot be separated by queries that factor through their model semantics
ORACLE–UOCL enrichment square	Program declaration	Semantic identification precedes effective categorical learning; tangent structure and decision structure are independent enrichments whose intersection supports DIAL
Differential-realization obstruction	Proposition	Tangent queries factoring through the coEilenberg–Moore coalgebra realization cannot distinguish differential presentations with equivalent realized tangent answers
PACC UOCL	Definition	Equivalence-invariant categorical probes, bounded discrepancy, a declared probe distribution, structural coverage, and separate accuracy and confidence parameters
PACC evolvability	Definition	Polynomially bounded categorical mutation neighborhoods; selection sees aggregate empirical probe performance rather than example-indexed repairs; mutations remain doctrine-valid and invariant under declared equivalences
PAC as discrete PACC	Proposition	Discrete instance and label categories with objectwise zero–one probes recover ordinary PAC risk and quantifiers exactly
Finite realizable PACC	Theorem	Finite query quotient, realizable target, zero–one discrepancy, i.i.d. probes, and a sample-consistent learner
Finite agnostic PACC	Theorem	Finite query quotient, bounded probe loss, i.i.d. probes, and empirical risk minimization; excess risk follows from uniform Hoeffding control
Persistent PACC confidence	Proposition	Finite horizon, conditional per-time guarantees, a union bound, and conservative comparison maps on the settled doctrine

Claim	Status	Boundary
Least causally available past	Proposition	Small poset of times; causal regions are downward closed
Online and persistent UDL	Definitions	Prefix restriction, non-anticipation, and registered coherent transport
Fixed-shape online Kan invariance	Theorem	Small indexing categories, fixed \(J,K\), and existence of the relevant Kan extensions
Prefix exactness	Definition	Invertible coherent Beck–Chevalley mates for growing observation diagrams
Online Kan quotient refinement	Proposition	Conservative revelation and existence of prefixwise quotients
Decision nerve and skeletal filtration	Proposition	Small decision-history category and its ordinary simplicial nerve
Inner-horn composition	Proposition	Ordinary categorical nerve; full Kan filling occurs exactly for groupoids
Simplicial online UDL	Definition	Compatible decorations on truncated simplex categories
Skeletal continuity of UDL	Theorem	Filtered colimits commute with the pointwise limits used by the right Kan extension
Homotopy-coherent online UDL	Definition	Localization at declared semantic weak equivalences and existence of derived Kan extensions
Homotopy Kan invariance	Proposition	Objectwise equivalence in the localized decision semantics
Homotopical repair profile	Definition	Derived mapping spaces for registered horn-lifting problems
Two-component inner-horn repair	Proposition and worked example	Two contractible candidate components and one later binary consistency constraint
Derived skeletal continuity	Theorem	Presentable stable target and finite pointwise right-Kan consistency shapes
Derived tangent comparison	Open problem	Requires a homotopical tangent functor and compatibility with derived Kan extensions
Static right-Kan comparator semantics	Proposition	Nonempty connected finite time category and existence of the required limit
Online comparison observer	Definition	Common value types and a separately declared comparison morphism
Crossword universal completion	Definition and proposition	Finite clue–crossing incidence diagram in \(\mathbf{Set}\) with registered, length-typed candidate sets
Sudoku universal completion	Definition and proposition	Finite cell–unit incidence diagram with registered all-different relations
FRM fixed-point admission	Definition and empirical connection	Soundness requires decoded learned fixed points to factor through the universal Sudoku solution object
Categorical OCO declaration	Definition	Convex decision algebra, order-lax losses, comparator and tangent declarations
Euclidean OCO recovery	Proposition	Nonempty bounded closed convex \(K\subseteq \mathbb {R}^d\) and bounded convex losses
Finite enriched Kan accumulation	Theorem	Finite horizon, discrete observations, \(\mathbb {R}\)-linear enrichment
Exact tangent comparison	Theorem	Fixed diagram shape and standard tangent on finite-dimensional vector spaces
Typed FTRL sensitivity	Proposition	Positive-definite cumulative Hessian and smooth interior readout
Metric-proximal FTRL tangent lift	Theorem	Smooth convex loss, positive-definite metric, and positive proximal scale
Proximal contraction certificate	Theorem	Anchor tangent; strict contraction requires relative strong convexity
Normalized FTRL tangent convergence	Theorem	Uniform coercivity and convergence of normalized base and tangent data
Contractive update tangent convergence	Theorem	Finite-dimensional smooth realization and uniform linearized contraction
FTRL/mirror equivalence	Corollary	Unconstrained, constant-step, Euclidean, linearized-loss presentation
Bandit barycentric reconstruction	Proposition	Finite arms and a full-support sampling distribution; equality holds after expectation
No deterministic pathwise bandit reconstruction	Proposition	At least two arms and arbitrary loss vectors
Bandit tangent and second-moment control	Proposition	Sampling distributions bounded away from the simplex boundary
Barycentric tangent reconstruction	Proposition	Differentiable full-support sampling and loss curves
Bandit regret transfer	Theorem	Oblivious losses, adapted full-support sampling, and a pathwise surrogate bound
Entropic adversarial bandit rate	Corollary	Finite arms, oblivious losses, and importance-weighted exponential updates
One-point smoothed-gradient reconstruction	Proposition	Convex Euclidean domain, ball smoothing, and differentiability of the average
Free convex completion for boosting	Proposition	Finite-support mixtures in \(D(H)\) and pointwise convex structure on \(K^C\)
Conditional weak-to-strong amplification	Theorem	Requires a supplied potential contraction certificate; deriving that certificate from a categorical weak learner remains open
Decision-presentation quotient	Proposition	UDL semantics, readout, and observer must invert every registered presentation equivalence

Claim	Status	Boundary
Comparator-sketch representation	Theorem	Right-Kan-admissible reference-shape map, replete admissible class, and existence of the right Kan extension
Block-static comparator spectrum	Proposition and corollary	Finite chain, contiguous partitions, and real-valued minimization for regret monotonicity
Approximate comparator observer transfer	Proposition	Chosen trajectory metric and Lipschitz evaluation and observer; not supplied by universality
Intrinsic asynchronous execution	Definition	Finite event poset, processor ownership, causal-past reads, and an external linearization observer
Asynchronous schedule invariance	Theorem	Finite event poset and commuting update endomorphisms at every incomparable pair
Asynchronous distributed minimization and Q-learning	Worked interpretation	Local component objectives, declared stale reads, fair coordinate updates, and separately supplied stochastic and contraction observers
Endogenous comparator descent	Open problem	Requires closed-loop construction before testing descent along a reference shape
Generator-level agentic safety	Proposition	Realized information category generated by declared edges whose objects and morphisms lie in an admitted execution subcategory
Safety under information-shape extension	Theorem	Pointwise right Kan extension and closure of the admitted subcategory under the required comma-category limits
Asynchronous revocation obstruction	Proposition	Incomparable revocation and use events with a decision rule adapted only to the local causal past
Audit observer distinguishability	Proposition	Faithfulness is necessary only on safety-relevant executions and does not detect channels outside the observer’s domain
Temporal contract descent	Proposition	Behavioral contract is a subobject in a sheaf topos and local verification witnesses agree on every overlap
Resilient intervention naturality	Open problem	Stop, veto, revocation, and rollback must commute with delegation and revoke derived authority
Independent-block repair	Proposition	Product decomposition on the registered context and queries factoring through protected complementary blocks
Canonical homotopy-coherent repair	Proposition	Contractible admissible filler space and homotopy-invariant downstream semantics
Quadratic tangent repair residual	Theorem	Finite-dimensional smooth realization, exact linearized repair, and Lipschitz derivative
Euclidean approachability checkpoint	Theorem	Closed convex target, bounded vector payoff, and Blackwell separating condition
Compositional structural transport	Theorem	Beck–Chevalley pasting, conservative observers, safety preservation, and coherent tangent comparisons when applicable
Finite persistence core	Theorem	Finite environment path and a common subobject admitting structural transport at every step; infinite persistence remains open
Causal interpretation	Not established	Requires intervention semantics and identification assumptions