CompilerTrustStatus
plain-language theorem explainer
A four-field record that packages whether a proof used native decision, which extra axioms it added, the standard Lean kernel basis, and whether an all-cardinality generalization is still open. Gravity auditors cite it when documenting compiler trust for the Track 1.B corrected gate at N = 5. It is a plain structure definition with no proof obligations.
Claim. A machine-checkable status record consisting of four fields: a boolean flag for whether the proof uses native decision; a list of extra axioms beyond the standard Lean basis; the standard kernel basis (propositional extensionality, classical choice, quotient soundness); and a boolean flag for whether the all-cardinality generalization remains open.
background
Track 1.B in the gravity stack closes a corrected-quadratic gate at fixed cardinality $N = 5$. The closing proof goes through Lean's native_decide, which means the kernel no longer sits on the pure classical basis alone: it also trusts the compiler's reduction of boolean expressions.
This module's job is bookkeeping, not physics derivation. The structure is the typed container for that bookkeeping. Module documentation states that the extra axioms are Lean.ofReduceBool and Lean.trustCompiler, layered on propext, Classical.choice, and Quot.sound. The $N = 5$ gate itself is closed, while the generalization to arbitrary cardinality is left open.
Upstream gravity material (the corrected Track 1.B quadratic gate) is the theorem whose trust surface this record describes; the structure itself does not restate that gate.
proof idea
No proof. The declaration is a structure with four fields of type Bool, List String, List String, and Bool. Inhabitants are built by supplying concrete values for each field, as in the sibling definition that records the Track 1.B status.
why it matters
Recognition Science gravity claims that pass through native decision need an explicit, machine-checkable trust surface so auditors can separate kernel-closed mathematics from compiler-trusted computation. This structure is that surface.
Its sole immediate consumer is the concrete status value for the Track 1.B corrected gate at $N = 5$, which sets native decision to true, lists Lean.ofReduceBool and Lean.trustCompiler as extras, records the standard three-axiom basis, and marks the all-cardinality generalization open. That value is the audit trail for correctedTrack1BGateAtN5_closed.
It does not advance the forcing chain (T0–T8), the Recognition Composition Law, or the mass ladder; it is infrastructure for honest claim classification in the gravity track.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.