track1BCompilerTrustStatus
plain-language theorem explainer
Records the compiler-trust footprint of the corrected Track 1.B discrete-curvature gate at N=5: the gate is closed by native decision, so the kernel is extended by boolean-reduction trust and general compiler trust on top of the classical basis, while the all-cardinality generalization stays open. Gravity auditors cite this when auditing which axioms underwrite that gate. It is a four-field structure literal, not a derived proof.
Claim. The compiler-trust status of the corrected Track 1.B gate at $N=5$ is the record with native decision enabled, extra axioms for boolean-reduction trust and general compiler trust, standard classical basis $\{\mathrm{propext},\,\mathrm{Classical.choice},\,\mathrm{Quot.sound}\}$, and the all-cardinality generalization marked open.
background
Track 1.B in the gravity stack concerns a corrected quadratic gate on discrete curvature data. At fixed cardinality $N=5$ that gate is closed (gate_open = false), discharged by Lean's native_decide tactic via the corrected-gate lemma in the Track1BCorrectedQuadratic module.
CompilerTrustStatus is a machine-checkable four-field record for any such native-decide proof: whether native decision is used, which extra axioms sit beyond the standard kernel basis, what that standard basis is, and whether an all-cardinality generalization remains open. The module doc states the extra axioms explicitly: Lean.ofReduceBool (trust compiler reduction of booleans) and Lean.trustCompiler (general native-computation trust), layered on propext / Classical.choice / Quot.sound.
This definition simply packages that status for the $N=5$ corrected gate; the mathematical closure of the gate itself lives upstream.
proof idea
Definitional structure literal. The four fields of CompilerTrustStatus are assigned directly: native-decide flag true; extra-axiom list the two compiler-trust axioms; standard basis the three classical kernel axioms; all-cardinality-open flag true. No tactics, no lemmas, no computation beyond the record construction.
why it matters
Gives a citable, machine-checkable audit trail for the axiom footprint of the closed Track 1.B gate at $N=5$. Downstream, the anchoring theorem track1BCompilerTrustStatus_anchors_closed_gate ties this record to the real gate status: it proves the native-decide flag is true and that correctedTrack1BStatus.gate_open = false, discharged by reflexivity against the upstream closed-gate fact.
In the Recognition gravity program this matters because discrete curvature / Regge-style gates feed the broader forcing story (eight-tick structure, $D=3$). Keeping the compiler-trust extension explicit prevents silent kernel inflation when the gate is reused. The record also flags the open problem: the all-cardinality generalization is not closed.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.