Kernel-Component Payload Types
Abstract
Each of the twenty-one kernel components indexes its own payload theorem type.
Theorem 1.1 (Every kernel component carries an indexed payload).
Proof. Machine-checked in Lean as D5/S0/Computability/KernelComponentPayload.every_kernel_component_carries_a_payload (✓ std3). ∎
Source. Repository-derived.
Commentary.
The type KernelComponent has exactly the twenty-one entries from the source load table: history, relation, group action, ledger, diagonal, state, address, phase, time, projection, zeta, infinity kernel, data, infinity sigma, normalization, dual, reflection, theta, proposition, certificate, and ontology.
PayloadTheorem is a dependent type indexed by those components. Every cited load label is a constructor at its exact index, including both labels where a table cell lists two loads. Consequently a component is part of the statement type of its payload: deleting that component would make the corresponding constructor ill-typed. A canonical dependent function supplies a witness for all twenty-one indices.
Repository searches found no existing exact or generalized encoding. No Mathlib theorem is used because the matrix is source-specific. This module deliberately imports none of the cited theorem modules: it certifies the load-bearing typing relation only and does not claim to reprove, combine, or strengthen their mathematical contents.
References
- Truth anchor:
D5/S0/Computability/KernelComponentPayload.every_kernel_component_carries_a_payload