Theoretical analysis establishes a resource theory of reflection in formal systems, demonstrating that diagonal closure governs fixed-point existence.
Paper 26 (General Self-Reference Calculus) showed that any system with full representability (repr-spec) satisfies the Master Fixed-Point Theorem (-1). Paper 27 (Closure Audits) formalized when determinacy is genuine vs. silently outsourced. The present paper fills the graded middle ground: how much internalization is enough for which fixed points, and how that maps to selector strength (NEMS IIa/IIb) in an abstract, non-physics way. We parameterize representability by a class ⊆ ( → ): a system may only internalize transformers in . The key notion is diagonal closure: is closed under the diagonalization template F ↦ (c ↦ F( (c,c))). We prove the Diagonal Closure Theorem: if is diagonally closed, then every F ∈ has a mixed fixed point p F( p). When is not diagonally closed, we prove a formal method-level separation: identity-only on with F ∈ but G_F ∉ , so the diagonal construction cannot produce a fixed point via (G_F). This yields a resource theory of reflection: levels of internalization correspond to achievable fixed-point guarantees. Full is the top level; we deliver a Lean-proved strict separation (identity-only) and roadmap further hierarchies. We bridge to Closure's internality predicate and to SelfReference's MFP-1, showing that Reflection extends both conservatively. The development is mechanized in Lean 4 (without custom axioms beyond Lean/mathlib; classical choice used only where explicitly stated), as the Reflection library in nems-lean. Trust boundary. Stratified representability and diagonal-closure hypotheses are explicit; the strict separations are about the formal constraints, not every physical "reflection" metaphor. Mechanization is nems-lean . See .
No takes yet. Share an insight, caveat, or question.
Nova Spivack (2026) studied this question.
Synapse has enriched 5 closely related papers on similar clinical questions. Consider them for comparative context: