somamaley-ux/non-degenerate-construction-kernel-admissibility: Kernel Reference v0.3.0 — Constructed necessity and exact realization

Abstract

v0.3.0 — Constructed necessity and exact original realization Lean companion to the v51 reference edition of Non-Degenerate Construction and the Kernel of Admissibility. This release checks the mathematical necessity chain developed around Proposition 2.4. Independently specified original subjects, complete uses, dependent witnesses, and their incidence relation supply the starting data. Qualification, assessment, original-identity retention, and the exact-realization criterion are constructed and proved. A prepackaged A1–A4 certificate or a proposed reader's soundness is not an input to this chain. Added checked mathematics IncidenceNecessity proves actual qualification, unique complete semantic qualification assessment, identity separation, the exact criterion for uniform transfer of original grounds, constructive original-incidence retention, and original-ground defect tests. NecessityRealization constructs an exact relational reader if and only if code fibres preserve the original profile. It proves uniqueness on the realized image, unique original-object reconstruction, omission/surplus/collision witnesses, and exact criteria for loss under erasure. The relational existence theorem uses no choice of representative. ObjecthoodNecessity constructs the regime from original incidence, proves its qualification semantics, derives the represented kernel roles, and assembles the necessity and universal realization results. Its finite authorization bridge extracts an actual original witness at the cut and supplies the corresponding constructed kernel realization. ContextualComposition derives finite heterogeneous congruence from original one-hole contexts, identifies the tuple quotient with the product of the sort quotients, and constructs the unique partial operation with its original domain image. ComparisonAndReindexing constructs semantic comparison and its groupoid laws, proves the finite-zigzag completeness criterion for primitive generators, and derives complete-evidence and support preservation from original edge and role-data reindexing. The original API, the five manuscript extensions, and the v0.2.0 reference mathematics remain supported. The complete build and theorem audit include the added modules; the verification inventory identifies the exact checked declaration set. Manuscript correspondence The v51 manuscript presents the incidence, identity, realization, and witnessed-failure results directly after Proposition 2.4. The role record is used together with that entire necessity chain. The manuscript explains why its semantic subjects and relations are those of actual identity-bearing incidence; the formalization checks the stated implications from those independently specified data. Kernel governance remains necessary for non-degenerate determinate objecthood, including unobserved incidence. The constructive and classical steps are identified separately. Classical qualification is semantic and need not be computable. A unique qualification answer does not make a multivalued physical result single-valued. Incorrect reporters remain subject to the original incidence tests. The numerical metric specialization of the checked binary normal form retains its short written proof. The reference PDF, manuscript project archive, Lean source archive, checksums, and verification record accompany the release. See PAPER_REFERENCE.md and KERNEL_PAPER_FORMALIZATION_STATUS.md for the artifact identities and exact theorem map. Verification 51 modules built; all 2,814 project constants inspected. 911/911 public theorem axiom reports and all 15 original anchors passed. Only propext, Classical.choice, and Quot.sound occur; no project axiom or proof placeholder. Fresh Linux CI and the complete semantic audit passed. Independent mathematical and publication review passed. The 69-page PDF has 60 numbered statements; all 55 prior statements and 82 prior label numbers remain stable. A clean three-pass rebuild matches all page text and reference labels. Commit: 754e9304ecf4c8f1e1b6733d99c615930181e439. Counts of theorem declarations include compiler-generated public equation lemmas.