This dashboard provides a complete inventory and formalization status map for Book I: Categorical Foundations. It covers the coherence kernel, orbit generation, earned arithmetic, and the full holomorphic machinery. Each registry object carries a scope label (established, tau-effective, or conjectural) and a formalization status. Use the statistics below to assess coverage, the dependency summary to trace proof chains, and the object list to navigate to individual entries in the registry.

Book I Registry Dashboard

Generated: 2026-03-10

Statistics

• Total objects: 254

• By type: axiom: 7

  construction: 2

  corollary: 4

  definition: 104

  lemma: 8

  proposition: 44

  remark: 32

  theorem: 53

• Formalization: formalized: 221

  not_applicable: 26

  planned: 7

• Scope: conjectural: 4

  established: 169

  tau-effective: 81

Dependency Summary

• Max chain depth: 42 (I.P27)
• Most depended-on: I.D03 (16 uses), I.D02 (13 uses), I.T05 (12 uses)
• No dependencies (foundational): I.K0, I.R16, I.R19

Part Coverage

| Part | Objects | Formalized | Planned | N/A | |——|———|————|———|—–| | 1 | 19 | 14 | 0 | 5 | | 2 | 10 | 10 | 0 | 0 | | 3 | 28 | 27 | 0 | 1 | | 4 | 19 | 14 | 1 | 4 | | 5 | 8 | 7 | 1 | 0 | | 6 | 4 | 2 | 1 | 1 | | 7 | 13 | 10 | 1 | 2 | | 8 | 14 | 14 | 0 | 0 | | 9 | 9 | 9 | 0 | 0 | | 10 | 7 | 5 | 1 | 1 | | 11 | 6 | 6 | 0 | 0 | | 12 | 7 | 4 | 2 | 1 | | 13 | 16 | 16 | 0 | 0 | | 14 | 18 | 18 | 0 | 0 | | 15 | 10 | 9 | 0 | 1 | | 16 | 10 | 10 | 0 | 0 | | 17 | 12 | 10 | 0 | 2 | | 18 | 41 | 33 | 0 | 8 | | 19 | 3 | 3 | 0 | 0 |

Object List

| ID | Type | Name | Scope | Lean | |—-|——|——|——-|——| | I.K0 | axiom | Universe Postulate | estab | form | | I.D01 | definition | Five Generators | estab | form | | I.D02 | definition | Progression Operator rho | estab | form | | I.D03 | definition | Diagonal Discipline | estab | form | | I.D04 | definition | Static Kernel tau_0 | estab | form | | I.K1 | axiom | Strict Order (K1) | estab | form | | I.K2 | axiom | Omega Fixed Point (K2) | estab | form | | I.K3 | axiom | Orbit-Seeded Generation (K3) | estab | form | | I.K4 | axiom | No-Jump / Cover (K4) | estab | form | | I.K5 | axiom | Beacon Non-Successor (K5) | estab | form | | I.K6 | axiom | Object Closure (K6) | estab | form | | I.P01 | proposition | Generator Distinctness | estab | form | | I.P02 | proposition | rho Injectivity Per Orbit | estab | form | | I.X01 | construction | The Generative Act | estab | form | | I.D05 | definition | Orbit Rays | estab | form | | I.D06 | definition | Iterator Ladder | estab | form | | I.T01 | theorem | Ontic Closure | estab | form | | I.T02 | theorem | Iterator Ladder Saturation | estab | form | | I.P03 | proposition | Pairwise Disjointness of Orbits | estab | form | | I.P04 | proposition | Orbit Countability | estab | form | | I.D07 | definition | tau-Idx (Earned Natural Numbers) | estab | form | | I.D08 | definition | Rank Transfer Maps | estab | form | | I.D09 | definition | Swap Operator sigma | estab | form | | I.D10 | definition | Index Addition | estab | form | | I.D11 | definition | Index Multiplication | estab | form | | I.D12 | definition | Index Exponentiation | estab | form | | I.D13 | definition | Index Tetration | estab | form | | I.D14 | definition | Program Monoid | estab | form | | I.D15 | definition | Three-Level Equality | estab | form | | I.T03 | theorem | Composition Associativity | estab | form | | I.P05 | proposition | Tetration Injectivity | estab | form | | I.D16 | definition | NF Address Encoding | estab | form | | I.D17 | definition | ABCD Coordinate Chart | estab | form | | I.T04 | theorem | Hyperfactorization Theorem | estab | form | | I.T05 | theorem | Prime Polarity Theorem | estab | form | | I.D18 | theorem | Algebraic Lemniscate | estab | form | | I.D19 | definition | Boundary Ring and Scalars | tau-e | form | | I.D20 | definition | Split-Complex Scalars | tau-e | form | | I.D21 | definition | Truth4 Logic | tau-e | form | | I.D22 | definition | Holomorphic Transformers | tau-e | form | | I.X02 | construction | Earned Category and Topos | tau-e | form | | I.T06 | theorem | Global Hartogs | tau-e | form | | I.R01 | remark | Axiom Independence | estab | — | | I.L01 | lemma | Pentation Non-Injectivity | estab | form | | I.T07 | theorem | Rigidity of tau | estab | form | | I.T08 | theorem | Categoricity of tau_0 | estab | form | | I.P06 | proposition | Arithmetic Laws | estab | form | | I.L02 | lemma | NF-Confluence | estab | form | | I.D16a | definition | Denotational Order | estab | form | | I.P07 | proposition | Well-Ordering of Obj(tau) | estab | form | | I.D19a | definition | Internal Divisibility | estab | form | | I.D19b | definition | Internal Primes | estab | form | | I.T09 | theorem | FTA on tau-Idx | estab | form | | I.D19c | definition | Tower Atom | estab | form | | I.D19d | definition | Greedy Peel Algorithm | estab | form | | I.P08 | proposition | Dimension Theorem (dim_tau = 4) | estab | form | | I.L03 | lemma | No-Tie Determinism | estab | form | | I.L04 | lemma | Strict Remainder Descent | estab | form | | I.C01 | corollary | Constructive Encoding via ABCD | estab | form | | I.D19e | definition | Prime Spectral Signature | estab | form | | I.D23 | definition | Genealogical Decomposition (Spine) | estab | form | | I.D24 | definition | Address DAG | estab | form | | I.P09 | proposition | Metric Inequality | estab | form | | I.D25 | definition | Omega-Tail (Compatible Tower) | estab | form | | I.D26 | definition | Polarized Omega-Germ | estab | form | | I.T10 | theorem | Split-Complex Forced | estab | form | | I.D27 | definition | Bipolar Spectral Algebra | estab | form | | I.D28 | definition | Boundary Local Ring | estab | form | | I.D19f | definition | Prime Enumeration and Sieve | estab | form | | I.D29 | definition | CRT Decomposition | estab | form | | I.D30 | definition | Teichmueller Lift | estab | form | | I.T11 | theorem | Minimal Alphabet Theorem | estab | form | | I.T11a | theorem | Six-Generator Rigidity Failure | estab | form | | I.T11b | theorem | Four-Generator Ladder Incompleteness | estab | form | | I.T11c | theorem | Tetration Algebraic Degradation | estab | form | | I.L05 | lemma | Growth Escape | estab | form | | I.D31 | definition | tau-Membership Relation | estab | form | | I.P10 | proposition | Membership Decidability | estab | form | | I.D32 | definition | Set-Theoretic Operations | estab | form | | I.P11 | proposition | Distributive Lattice | estab | form | | I.D33 | definition | Bounded Powerset | estab | form | | I.L06 | lemma | Well-Foundedness of Membership | estab | form | | I.P12 | proposition | Countability of Set(tau) | estab | form | | I.D34 | definition | Master Constant iota_tau | tau-e | form | | I.D35 | definition | Number Tower | tau-e | form | | I.D36 | definition | Constructive Reals | tau-e | form | | I.D37 | definition | Lemniscate Characters | tau-e | form | | I.D38 | definition | Character Group | tau-e | form | | I.T12 | theorem | Spectral Decomposition | tau-e | form | | I.D39 | definition | Crossing Point | tau-e | form | | I.D40 | definition | Bipolar Fourier Transform | tau-e | form | | I.T13 | theorem | Explosion Barrier | tau-e | form | | I.P13 | proposition | Boolean Recovery | tau-e | form | | I.D41 | definition | Subobject Classifier Preview | tau-e | form | | I.P14 | proposition | Omega Unique Fixed Seed | estab | form | | I.P15 | proposition | Sum Zero Iff Both Zero | estab | form | | I.T14 | theorem | No Additive Inverse | estab | form | | I.T15 | theorem | No Ring Negation | estab | form | | I.P16 | proposition | Positive Core Closure | estab | form | | I.P17 | proposition | Universal Additive Cancellation | estab | form | | I.T16 | theorem | Mul Cancel Fails at Zero | estab | form | | I.T17 | theorem | Multiplicative Cancellation iff Positive | estab | form | | I.P18 | proposition | Zero Vacuous | estab | form | | I.P19 | proposition | Integral Domain | estab | form | | I.P20 | proposition | Ultra Dist Self | estab | form | | I.P21 | proposition | Congruent Tails Agree | estab | form | | I.D42 | definition | D-Differentiability | tau-e | form | | I.D43 | definition | Split-CR Equations | tau-e | form | | I.P22 | proposition | Sector Independence | tau-e | form | | I.D45 | definition | Omega-Germ Transformer | tau-e | form | | I.D46 | definition | Tower Coherence | tau-e | form | | I.D47 | definition | Tau-Holomorphic Function | tau-e | form | | I.D48 | definition | Tau-Holomorphic Map | tau-e | form | | I.T18 | theorem | CRT Coherence Constraint | tau-e | form | | I.P23 | proposition | No Simultaneous Projection | tau-e | form | | I.T19 | theorem | Diagonal-Free Protection | tau-e | form | | I.T20 | theorem | Composition Closure | tau-e | form | | I.P24 | proposition | HolFun Associativity | tau-e | form | | I.L07 | lemma | Tail Agreement Propagation | tau-e | form | | I.T21 | theorem | Tau-Identity Theorem | tau-e | form | | I.D49 | definition | Hol(L) | tau-e | form | | I.D50 | definition | Tau-Arrow | tau-e | form | | I.D51 | definition | Cat_tau | tau-e | form | | I.T22 | theorem | Category Axioms | tau-e | form | | I.P25 | proposition | Thin Category | tau-e | form | | I.D52 | definition | Tau-Functor | tau-e | form | | I.D53 | definition | Natural Transformation | tau-e | form | | I.D54 | definition | Yoneda Embedding | tau-e | form | | I.T23 | theorem | Yoneda Lemma | tau-e | form | | I.D55 | definition | Finite Limits in Cat_tau | tau-e | form | | I.D56 | definition | Tau-Site | tau-e | form | | I.D57 | definition | Presheaf Topos | tau-e | form | | I.T24 | theorem | Grothendieck Topos | tau-e | form | | I.P26 | proposition | Countable Topos | tau-e | form | | I.T25 | theorem | Omega_tau Subobject Classifier | tau-e | form | | I.D58 | definition | Characteristic Morphism | tau-e | form | | I.D59 | definition | Earned Topos | tau-e | form | | I.P27 | proposition | Paraconsistent Character | tau-e | form | | I.D60 | definition | Categorical Product | tau-e | form | | I.T26 | theorem | Product Universal Property | tau-e | form | | I.D61 | definition | Cartesian Monoidal Structure | tau-e | form | | I.D62 | definition | Categorical Coproduct | tau-e | form | | I.T27 | theorem | Distributivity | tau-e | form | | I.D63 | definition | Bi-Monoidal Structure | tau-e | form | | I.D64 | definition | Internal Hom | tau-e | form | | I.T28 | theorem | Cartesian Closed | tau-e | form | | I.P28 | proposition | Self-Enrichment | tau-e | form | | I.D65 | definition | Spectral Coefficients | tau-e | form | | I.D66 | definition | Restriction Map | tau-e | form | | I.T29 | theorem | Spectral Determination | tau-e | form | | I.D67 | definition | Primorial Thinness | tau-e | form | | I.L08 | lemma | CRT Extension | tau-e | form | | I.T30 | theorem | Removable Singularity | tau-e | form | | I.T31 | theorem | Global Hartogs Extension | tau-e | form | | I.D68 | definition | Earned Stage-Determined Point | tau-e | form | | I.C02 | corollary | Stages from Limit | tau-e | form | | I.P29 | proposition | Passage to Book II | tau-e | form | | I.D75 | definition | Generative Counting Principle | estab | form | | I.P33 | proposition | Counting as Structural Feature | estab | form | | I.T35 | theorem | Cantor Diagonal Inapplicability | estab | form | | I.P34 | proposition | No Unearned Decimal Diagonal | estab | form | | I.P35 | proposition | No Unrestricted Comprehension | estab | form | | I.P36 | proposition | No Free Cartesian Diagonal | estab | form | | I.D76 | definition | Omega-Germ Approach | estab | form | | I.T36 | theorem | Unique Infinity Object | estab | form | | I.P37 | proposition | Ultrametric Replaces Cardinality | estab | form | | I.D77 | definition | Meta-Logical Substrate | estab | form | | I.R15 | remark | Structural Rules Inventory | estab | form | | I.D78 | definition | Diagonal-Linear Correspondence | estab | form | | I.T37 | theorem | Diagonal-Linear Correspondence | estab | form | | I.D79 | definition | Program Monoid as Linear Calculus | estab | form | | I.R16 | remark | Linear Logic Glossary | estab | form | | I.T38 | theorem | Linearity Census | estab | form | | I.P38 | proposition | Classical.em Eliminability | estab | form | | I.R17 | remark | Gap Declaration | estab | form | | I.D80 | definition | Self-Hosting Degree Classification | estab | — | | I.R18 | remark | Proof-Theoretic Landscape Survey | estab | — | | I.D81 | definition | CCC-Linear Dichotomy | estab | form | | I.T39 | theorem | K5 Structural Exclusion | estab | form | | I.R19 | remark | Barr’s Star-Autonomous Categories | estab | — | | I.D82 | definition | Enrichment Frontier Classification | estab | form | | I.R20 | remark | E0-E3 Literature Map | estab | — | | I.R21 | remark | Scale Declaration | estab | — | | I.D83 | definition | Primorial Presheaf | estab | form | | I.T40 | theorem | Presheaf Characterization | estab | form | | I.T41 | theorem | Bi-Square Characterization | estab | form | | I.D84 | definition | Constructive Reals | estab | form | | I.T42 | theorem | Archimedean Property | estab | form | | I.P39 | proposition | TauReal Ring Axioms | estab | form | | I.D85 | definition | Elliptic Complex Field | estab | form | | I.D86 | definition | Elliptic-Hyperbolic Dichotomy | estab | form | | I.T43 | theorem | TauComplex Ring Axioms | estab | form | | I.D87 | definition | Elliptic Quaternions | estab | form | | I.T44 | theorem | Quaternion Non-Commutativity | estab | form | | I.R22 | remark | Hurwitz Classification Preview | estab | — | | I.D88 | definition | Cyclotomic Fields | estab | form | | I.T45 | theorem | Roots of Unity CRT Decomposition | estab | form | | I.R23 | remark | Galois Theory Preview | estab | — | | I.D89 | definition | Diagonal Resonance | estab | form | | I.D90 | definition | Identity Slippage | estab | form | | I.D91 | definition | Shadow Identity | estab | form | | I.R24 | remark | Five Reasons Why The Bug Hides | estab | — | | I.R25 | remark | Orthodox Foundations Under the Lens | estab | — | | I.T46 | theorem | Ontic Identity Invariance | estab | form | | I.C03 | corollary | No Identity Decoherence | estab | form | | I.T47 | theorem | Slippage Breaks Unique Omega | estab | form | | I.D92 | definition | Identity-Faithful Reception | estab | form | | I.D93 | definition | Structural Instability | estab | form | | I.T48 | theorem | Structural Instability Theorem | estab | form | | I.R26 | remark | Implications for Absolute Meaning | estab | — | | I.R27 | remark | Honest Scope Declaration | estab | — | | I.D94 | definition | Orbit-Set Map | estab | form | | I.P40 | proposition | Extensionality | estab | form | | I.P41 | proposition | Self-Containment Partition | estab | form | | I.P42 | proposition | Order Bound | estab | form | | I.R28 | remark | Inseparability of N and omega | estab | form | | I.R29 | remark | Finite-Infinite Boundary | estab | form | | I.R30 | remark | Duality and Atoms | estab | form | | I.D95 | definition | τ-Measure Space | tau-e | form | | I.D96 | definition | Tower σ-Algebra | tau-e | form | | I.T49 | theorem | Countable Additivity | tau-e | form | | I.P43 | proposition | Measure Compatibility | tau-e | form | | I.D97 | definition | Galois Automorphism | tau-e | form | | I.D98 | definition | Galois Group of Primorial Stage | tau-e | form | | I.T50 | theorem | Fundamental Theorem of Internal Galois Theory | tau-e | form | | I.P44 | proposition | CRT-Galois Decomposition | tau-e | form | | I.D99 | definition | τ-Integral | tau-e | form | | I.T51 | theorem | Linearity of Integration | tau-e | form | | I.P45 | proposition | Monotone Convergence | tau-e | form | | I.D101 | definition | Prime Counting in Progressions | estab | form | | I.D102 | definition | Chebyshev Bias Measure | tau-e | form | | I.T52 | theorem | Bias at Primorial Levels | tau-e | form | | I.R31 | remark | Wiring Primitives | estab | — | | I.R32 | remark | Product-Free Operator Definitions | estab | — | | I.R33 | remark | Route B Axioms Comparison | estab | — | | I.R34 | remark | Normalization Endofunctors M and E | estab | — | | I.R35 | remark | Address Combinators: Merge and Lift | estab | — | | I.R36 | remark | CGANF to ABCD Design Evolution | estab | — | | I.R37 | remark | Cluster Collapse in ABCD Context | estab | — | | I.R38 | remark | Token-Set vs Tuple Encoding | estab | — | | I.R39 | remark | Dimension Readout Functors | estab | — | | I.P46 | proposition | No Second Linearity | estab | — | | I.C04 | corollary | NF Deduplication Invariant | estab | — | | I.D103 | definition | Polarity Pairing | estab | — | | I.R40 | remark | Pairing Density | estab | — | | I.D104 | definition | PolStream | estab | — | | I.R41 | remark | PolStream Aperiodicity | estab | — | | I.R42 | remark | Lemniscate Lipschitz Forward Reference | estab | — | | I.R43 | remark | Quaternion Open Question | conje | — | | I.D105 | definition | Tau-Weighted Boundary Constants | estab | — | | I.D106 | definition | Tau-Bayesian State | conje | — | | I.P47 | proposition | Bayesian Factorization | conje | — | | I.R44 | remark | Lean Bayesian Status | conje | — | | I.R45 | remark | Distributivity from Combinators | estab | — |