Corpus
Corpus · Registry · Dashboard

Registry Dashboard — Book I: Categorical Foundations

Browse Objects Registry Overview Filter Rules

Filter rule on this page: dashboard_display — counts the five display types (definition, lemma, proposition, remark, theorem). The full registry root for I has 254 objects across all types; this dashboard enumerates 254 of them. See the Filter Rules manifest for the authoritative definitions, or the Release Manifest for the per-book reconciliation across all surfaces.

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 —

Save or share this page for inspection

Download a portable dossier, copy a reviewer note, or send this page to someone who can inspect it.

Email to expert