Gravity Track1 Bcompiler Trust Status Track1 Bcompiler Trust Status

Compiler trust status

In a machine-checked library of formal theorems, a proof is only as strong as the axioms it invokes. The standard logical kernel of the Lean proof assistant rests on three axioms: propositional extensionality, choice, and quotient soundness. Most proofs stay within that basis. But some proofs use a tactic called native_decide, which asks the compiler to evaluate a boolean expression and trust the result. That trust is an extra assumption, not part of the kernel's three axioms.

The declaration track1BCompilerTrustStatus is a small record that makes this extra trust explicit for one specific result: the corrected Track 1.B quadratic gate at N = 5. The record states that the proof of this gate uses native_decide, and that it therefore extends the kernel basis with two additional axioms: Lean.ofReduceBool, which lets the kernel trust the compiler's reduction of boolean expressions, and Lean.trustCompiler, which grants general compiler trust for native computation. The record also lists the standard basis it builds on, and it flags that the all-cardinality generalization remains open.

The anchoring theorem track1BCompilerTrustStatus_anchors_closed_gate connects the record to the actual result: the N = 5 gate is closed, meaning gate_open = false in the corrected status, and the record correctly reports uses_native_decide = true. In plain terms, the single gate at N = 5 has been proved, but the proof leans on compiler trust, and the broader claim for all cardinalities has not been established.

What the declaration does not claim is just as important. It does not claim that the N = 5 gate is proved within the standard kernel basis; it explicitly says the opposite. It does not claim that the all-cardinality generalization is proved; that is marked open. And it does not claim that compiler trust is equivalent to kernel trust; it merely records that the proof uses it. The value of the record is honesty: it names the extra assumptions so that anyone reading the library knows exactly what the proof depends on.

/-- The compiler-trust status of the Track 1.B corrected gate at `N = 5`.
The gate is closed via `native_decide` (see
`Track1BCorrectedQuadratic.correctedTrack1BGateAtN5_closed`), so the kernel
basis is extended by `Lean.ofReduceBool` and `Lean.trustCompiler` on top of
the standard `propext / Classical.choice / Quot.sound` basis. The
all-cardinality generalization remains open. -/
def track1BCompilerTrustStatus : CompilerTrustStatus where
  uses_native_decide := true
  extra_axioms := ["Lean.ofReduceBool", "Lean.trustCompiler"]
  standard_basis := ["propext", "Classical.choice", "Quot.sound"]
  all_cardinality_open := true

/-- **Anchoring theorem.** The trust-status record is anchored to the real
result: the corrected Track 1.B gate at `N = 5` is closed
(`gate_open = false` in `correctedTrack1BStatus`), discharged by
`native_decide` via `correctedTrack1BGateAtN5_closed`, and the trust status
correctly records `uses_native_decide = true`. -/
theorem track1BCompilerTrustStatus_anchors_closed_gate :
    track1BCompilerTrustStatus.uses_native_decide = true ∧
    Track1BCorrectedQuadratic.correctedTrack1BStatus.gate_open = false := by
  exact ⟨rfl, rfl⟩

What this page does not claim

The N = 5 gate is proved within the standard kernel basis alone. The all-cardinality generalization is proved. Compiler trust is equivalent to kernel trust.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Gravity/Track1BCompilerTrustStatus.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: