Kernel Trust Profile 0.1: a machine-readable declaration of what a body of machine-checked mathematics rests on

A specification for declaring what a body of machine-checked mathematics rests on. CITATION.cff standardises how to cite a project and SPDX standardises its licence. Nothing standardises what it rests on — whether a theorem is standing on an unfinished proof several files upstream, or was obtained by trusting a compiler rather than a kernel. Both look exactly like success and neither is visible to anyone downstream. A Kernel Trust Profile is that statement, in a fixed shape, computed from the artifact rather than asserted by its author. Six design rules keep a profile from becoming a badge. It must be mechanically recomputable by a third party from the named revision (R1). Absence is not zero — null means not measured, while 0 is a positive claim that must be backed by a measurement (R2). Statement and proof dependencies stay separate, because a statement dependency changes what was proved and a proof dependency changes only how (R3). Reach is invariant under inlining and factoring while amplification is not, so a profile must report reach and must not rank by amplification (R4). There is no composite trustworthiness score: a theorem either reaches an unfinished proof or it does not, and averaging that against anything invents precision the measurement does not have (R5). And it must be emittable by any tool that can compute a declaration graph, since a format only one program can produce is a file format and not a standard (R6). Includes the JSON Schema and 14 worked profiles covering Lean 4 libraries and five Metamath databases — ZFC, intuitionistic logic, New Foundations, quantum logic and higher-order logic. Those examples exist to test the specification against data gathered before the specification was written; four fields are null across every profile because those measurements were never taken, which is R2 doing its job. A profile carries no claim about correctness, quality or importance and is not a certificate. It reports provenance: which trust assumptions a library's theorems actually reach. Specification CC-BY-4.0; implementations unencumbered. Canonical home: f-keys.com/gonzalgo/kernel-trust/