Gravity Track1 Bcompiler Trust Status Compiler Trust Status

Compiler trust status

In formal mathematics, a proof is only as strong as the rules it is allowed to use. The Recognition Science framework's machine-checked library of formal theorems normally relies on three standard axioms: propositional extensionality, choice, and quotient soundness. The declaration CompilerTrustStatus is a record that tracks when a proof steps outside that minimal basis. It names the extra assumptions a proof uses, so anyone reading the library can see exactly where the foundation widens.

The specific case recorded here concerns the Track 1.B corrected-quadratic gate at N = 5. That gate is a boolean condition that the framework's own corrected quadratic formula must satisfy at the fifth step. The gate is closed: the record shows `gate_open = false`, meaning the condition holds. But the proof that it holds was discharged by a mechanism called `native_decide`, which asks the compiler to evaluate the expression rather than the kernel to derive it. Because of that, the proof relies on two extra 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 declaration does not claim that the N = 5 gate is proved in the minimal axiom basis. It explicitly records that `uses_native_decide = true` and lists the two extra axioms alongside the standard three. It also records that the all-cardinality generalization, the statement that the gate closes for every N, remains open: `all_cardinality_open = true`. So the record is an honest ledger of what was established and under what assumptions, not a claim that the full result is kernel-checked with no extras.

What the declaration does establish, through its anchoring theorem, is that the trust-status record accurately describes the real state of the N = 5 gate. The theorem `track1BCompilerTrustStatus_anchors_closed_gate` proves that the record's `uses_native_decide` flag is true and that the gate is indeed closed. That is a machine-checked fact about the record itself. The practical consequence: a reader of the library can see at a glance that one specific gate was closed with compiler help, and that the broader claim across all cardinalities is still a target, not a result.

/-- Machine-checkable record of the basis and open-problem status
for a theorem whose proof relies on `native_decide`. -/
structure CompilerTrustStatus where
  /-- Whether the proof uses `native_decide`. -/
  uses_native_decide : Bool
  /-- Extra axioms beyond the standard Lean basis. -/
  extra_axioms : List String
  /-- The standard Lean kernel basis. -/
  standard_basis : List String
  /-- Whether the all-cardinality generalization remains open. -/
  all_cardinality_open : Bool

/-- 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 in the minimal axiom basis. The all-cardinality generalization is closed. Compiler trust is equivalent to the standard kernel axioms.

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: