IndisputableMonolith.Gravity.Track1BCompilerTrustStatus

   1import IndisputableMonolith.Gravity.Track1BCorrectedQuadratic
   2
   3namespace IndisputableMonolith
   4namespace Gravity
   5namespace Track1BCompilerTrustStatus
   6
   7/-!
   8# Compiler-Trust Status for the Track 1.B Corrected Gate
   9
  10This module records, in a machine-checkable structure `CompilerTrustStatus`,
  11that the Track 1.B corrected-quadratic gate at `N = 5`
  12(`Track1BCorrectedQuadratic.correctedTrack1BGateAtN5_closed`) relies on
  13`native_decide` and therefore extends the kernel basis.
  14
  15The extra axioms introduced are:
  16- `Lean.ofReduceBool`: allows the kernel to trust the compiler's reduction
  17  of boolean expressions.
  18- `Lean.trustCompiler`: grants general compiler trust for native computation.
  19
  20The `N = 5` gate itself is closed (`gate_open = false` in
  21`correctedTrack1BStatus`), but the all-cardinality generalization remains open.
  22-/
  23
  24/-- Machine-checkable record of the basis and open-problem status
  25for a theorem whose proof relies on `native_decide`. -/
  26structure CompilerTrustStatus where
  27  /-- Whether the proof uses `native_decide`. -/
  28  uses_native_decide : Bool
  29  /-- Extra axioms beyond the standard Lean basis. -/
  30  extra_axioms : List String
  31  /-- The standard Lean kernel basis. -/
  32  standard_basis : List String
  33  /-- Whether the all-cardinality generalization remains open. -/
  34  all_cardinality_open : Bool
  35
  36/-- The compiler-trust status of the Track 1.B corrected gate at `N = 5`.
  37The gate is closed via `native_decide` (see
  38`Track1BCorrectedQuadratic.correctedTrack1BGateAtN5_closed`), so the kernel
  39basis is extended by `Lean.ofReduceBool` and `Lean.trustCompiler` on top of
  40the standard `propext / Classical.choice / Quot.sound` basis. The
  41all-cardinality generalization remains open. -/
  42def track1BCompilerTrustStatus : CompilerTrustStatus where
  43  uses_native_decide := true
  44  extra_axioms := ["Lean.ofReduceBool", "Lean.trustCompiler"]
  45  standard_basis := ["propext", "Classical.choice", "Quot.sound"]
  46  all_cardinality_open := true
  47
  48/-- **Anchoring theorem.** The trust-status record is anchored to the real
  49result: the corrected Track 1.B gate at `N = 5` is closed
  50(`gate_open = false` in `correctedTrack1BStatus`), discharged by
  51`native_decide` via `correctedTrack1BGateAtN5_closed`, and the trust status
  52correctly records `uses_native_decide = true`. -/
  53theorem track1BCompilerTrustStatus_anchors_closed_gate :
  54    track1BCompilerTrustStatus.uses_native_decide = true ∧
  55    Track1BCorrectedQuadratic.correctedTrack1BStatus.gate_open = false := by
  56  exact ⟨rfl, rfl⟩
  57
  58end Track1BCompilerTrustStatus
  59end Gravity
  60end IndisputableMonolith