1. IR001 — Rational representation equivalence (planned)
2. IR002 — Rational operations respect representation (planned)
3. IR003 — Rational order and decision (planned)
4. IR004 — Absolute value and interval arithmetic (planned)
5. IR005 — Finite rational folds (planned)
6. IR006 — Dyadic domination (planned)
7. IR007 — Finite pigeonhole (planned)
8. IR008 — Bounded decidable minimum (planned)
9. IR009 — Power difference factorization (planned)
10. IR010 — Geometric tail arithmetic (planned)
11. IR011 — Factorial lower bounds (planned)
12. IR012 — Approximation operations without real sorts (planned)
13. IR013 — Integer square root totality (planned)
14. IR014 — Dyadic sqrt2 enclosures (planned)
15. IR015 — Sqrt2 algebra and strict bounds (planned)
16. IR016 — Even-square descent (planned)
17. IR017 — Logarithm series remainder (planned)
18. IR018 — Logarithm interval and node gaps (planned)
19. IR019 — Exponential partial-sum totality (planned)
20. IR020 — Exponential explicit tail (planned)
21. IR021 — Finite binomial convolution (planned)
22. IR022 — Exponential addition and integer powers (planned)
23. IR023 — Exponential order and Lipschitz (planned)
24. IR024 — Log-exp inverse at two (planned)
25. IR025 — Canonical approximation totality (planned)
26. IR026 — Canonical approximation accuracy (planned)
27. IR027 — Identification with the requested constant (planned)
28. IR028 — A strict coarse enclosure (planned)
29. IR029 — Quadratic ring operations (planned)
30. IR030 — Quadratic equality is decidable (planned)
31. IR031 — Norm identity and multiplicativity (planned)
32. IR032 — Integral quadratic norm separation (planned)
33. IR033 — Quadratic powers and coefficient height (planned)
34. IR034 — Distinct frequencies with quantitative gap (planned)
35. IR035 — Cleared rational quadratic lower bound (planned)
36. IR036 — Auxiliary parameter arithmetic (planned)
37. IR037 — Matrix row/column enumerations (planned)
38. IR038 — Uniform denominator clearing (planned)
39. IR039 — Auxiliary matrix height (planned)
40. IR040 — Linear-map image box (planned)
41. IR041 — Strict box cardinality inequality (planned)
42. IR042 — Small nonzero integer kernel vector (planned)
43. IR043 — Auxiliary low jets vanish algebraically (planned)
44. IR044 — Annihilating polynomial construction (planned)
45. IR045 — Moment polynomial identity (planned)
46. IR046 — Nonzero quadratic products (planned)
47. IR047 — Bounded nonzero jet at zero (planned)
48. IR048 — Least nonzero jet across all nodes (planned)
49. IR049 — Selected jet height and separation (planned)
50. IR050 — Weak compositions and homogeneous sums (planned)
51. IR051 — Monomial divided differences (planned)
52. IR052 — Homogeneous-sum enclosure (planned)
53. IR053 — Factorial-binomial cancellation (planned)
54. IR054 — Finite exponential divided-difference estimate (planned)
55. IR055 — Polynomial Hermite cardinal basis (planned)
56. IR056 — Finite confluent interpolation identity (planned)
57. IR057 — Explicit interpolation coefficient bound (planned)
58. IR058 — Polynomial-to-exponential tail transfer (planned)
59. IR059 — Zero-jet interpolation estimate (planned)
60. IR060 — Approximate-zero interpolation estimate (planned)
61. IR061 — Exponential jet identity (planned)
62. IR062 — Growth on the interpolation interval (planned)
63. IR063 — Factorial and q-to-r descent (planned)
64. IR064 — Explicit combined gap (planned)
65. IR065 — Negative irrationality checkpoint (planned)
66. IR066 — Rational competitors outside the unit interval (planned)
67. IR067 — Uniform perturbation of algebraic jets (planned)
68. IR068 — Finite accuracy removes vanishing assumptions (planned)
69. IR069 — Excluded neighborhood with rational slack (planned)
70. IR070 — Decidable precision-to-certificate bridge (planned)
71. IR071 — Irrationality certificate soundness (planned)
72. IR072 — Full positive HA irrationality (planned)
73. IR073 — Certificate-search totality (planned)
74. IR074 — Representation-invariant endpoint (planned)
75. IR075 — Quadratic polynomial remainder certificate (planned)
76. IR076 — Finite multivariate substitution error (planned)
77. IR077 — Finite Taylor derivative identity (planned)
78. IR078 — Denominator-cleared confluent identity (planned)
79. IR079 — Formal atanh/exponential coefficient recurrence (planned)
80. IR080 — Formal recurrence identifies rational series (planned)
81. IR081 — Composition-tail bound at one third (planned)
82. TR001 — Integer polynomial evaluation stability (planned)
83. TR002 — Coded algebraic extension presentations (planned)
84. TR003 — General denominator and norm separation (planned)
85. TR004 — Variable-node auxiliary estimate (planned)
86. TR005 — Polynomial nonvanishing bridge (planned)
87. TR006 — Full positive transcendence (planned)
88. ENG001 — Contract and definition elaboration gate (planned)
89. ENG002 — Existing-premise audit (planned)
90. ENG003 — Model-free native baseline (planned)
91. ENG004 — Guarded SMT/TPTP export (planned)
92. ENG005 — External hint reconstruction (planned)
93. ENG006 — Hostile replay and independent Lean (planned)
94. ENG007 — Bounded scheduler and accounting (planned)
95. ENG008 — Final irrationality closure and presentation (planned)
96. ENG009 — Fallback proof-translation pilot (not primary route) (planned)