IndisputableMonolith.Gravity.Track1BCompilerTrustStatus
Status ledger for Track 1.B gravity proofs that use `native_decide`: it records the algebraic basis and which gate remains open. Gravity auditors cite it to separate closed Lean facts from the named open corrected gate. The module is a structured status object plus a small theorem tying that status to the closed-gate anchors, not a new dynamical derivation.
claimA machine-checkable compiler-trust record for Track 1.B: it packages the basis of the axis-stencil / corrected-quadratic local correspondence and flags that the corrected gate itself is open, while the surrounding Track 1.B statements that rely on kernel decision procedures remain theorem-grade once that status is recorded.
background
Track 1.B is the gravity route that aims at a local Regge / J-cost correspondence via an axis-stencil corrected quadratic. The upstream module Track1BCorrectedQuadratic states that everything it asserts is a theorem (zero sorry, zero RS-internal axiom), while the corrected gate is explicitly named OPEN and is not asserted as proved.
In Lean, some finite algebraic or Boolean obligations are discharged by native_decide (kernel evaluation of a decidable proposition). That is fine for closed finite checks, but a referee still needs a crisp record of what was decided, on what basis, and which named obligation remains open. This module is that record for Track 1.B.
The Recognition gravity setting here is local stencil correspondence, not the global forcing chain (T5 J-uniqueness, T8 $D=3$). J-cost and the corrected quadratic enter only as the upstream objects whose trust status is being annotated.
proof idea
Definition-plus-status module, not a long derivation. It introduces a status structure (CompilerTrustStatus) and a concrete Track 1.B instance (track1BCompilerTrustStatus) that points at the corrected-quadratic basis and marks the open gate. A small companion lemma (track1BCompilerTrustStatus_anchors_closed_gate) ties that status object to the already-closed anchors from the upstream Track 1.B module. No new continuum gravity identity is proved here; the work is packaging and gate bookkeeping for native_decide-backed obligations.
why it matters in Recognition Science
Without an explicit trust ledger, native_decide steps in Track 1.B look like opaque kernel magic. This module makes the basis and the open corrected gate auditable, so downstream gravity claims can cite a named status object rather than an informal comment. It sits directly on Track1BCorrectedQuadratic (axis-stencil local correspondence) and does not itself close the OPEN gate; it prevents silent overclaim while that gate stays open. No downstream consumers are wired in the graph yet; the module is infrastructure for honest Track 1.B citation.
scope and limits
- Does not prove the corrected Track 1.B gate; that gate remains explicitly open.
- Does not derive new J-cost, Regge, or continuum gravity identities.
- Does not justify `native_decide` outside the finite obligations recorded here.
- Does not feed a listed downstream theorem yet (used_by is empty).
- Does not address global RS landmarks (phi ladder, eight-tick, D=3) beyond Track 1.B status.