FormalRV.Verifier.ProofGate — the anti-cheat ENFORCEMENT of the verifier. `#verify_clean foo` is a hard build-time check: it succeeds iff `foo` is fully proved using ONLY the standard kernel axioms (`propext`, `Classical.choice`, `Quot.sound`) — NO `sorryAx`, NO custom `axiom`s. If `foo`'s proof is incomplete or leans on any extra axiom, `#verify_clean` raises an ELABORATION ERROR and the build FAILS. This is the "Lean verifier rejects the implementer's submission unless the whole thing is proved" mechanism: the user (spec-setter) writes `#verify_clean <submission>` at the bottom of the obligation; the implementer cannot land a submission that hides a `sorry` or sneaks in an axiom, because the kernel's transitive axiom set is inspected and the build is gated on it.

def allowedAxioms : List Name

theorem clean_example : 1 + 1 = 2

private axiom unproven_fixture : (2 : Nat) + 2 = 4
#verify_rejects unproven_fixture     -- ✓ correctly rejected (a real proof is required)

FormalRV.Verifier.ShorSpec — the AIRTIGHT obligation a Shor implementation must satisfy. The USER (spec-setter) fixes the inputs: the number `N` to factor, the LP code `code` (a `CSSCode`), and the logical operators `L` (a `LogicalBasis`, giving the logical Z̄_i for every logical qubit). The IMPLEMENTER must then inhabit `VerifiedShorOnCode N Δ k code L`, and `#verify_clean` (ProofGate) rejects any submission that uses `sorry` or an extra axiom. Every field is a REAL obligation — no escape hatches, no vacuous `:= True` placeholders: `code_valid` / `code_qldpc` / `logical_valid` / `N_target` are DECIDABLE facts about the user's inputs (a `= true` / concrete `Prop`), so they cannot be faked. `succeeds` demands the genuine measurement-success metric `probability_of_success ≥ κ/(log₂N)⁴` on an oracle satisfying `ModMulImpl` (the actual SQIR Shor statement) — NOT a gate-count proxy. `realized_on_code` demands a CONCRETE physical circuit on the code's qubits that REALIZES the logical oracle through an encoding isometry into the code (`uc_eval physical · enc = enc · uc_eval (u i)`), with the user's `L.zbar` as the logical Z observables. This is a matrix equation — it is false unless the physical construction genuinely implements the logical computation. This file only DEFINES the obligation (it compiles). The construction + proof is the implementer's job, gated by `#verify_clean`.

def ShorTarget (N : Nat) : Prop

def LogicalShorSucceeds (a r N m bits : Nat)
    (u : Nat → BaseUCom (bits + FormalRV.BQAlgo.sqir_modmult_rev_anc bits)) : Prop

def OracleRealizedOnCode (code : CSSCode) {k : Nat} (_L : LogicalBasis code k)
    {dim : Nat} (u : Nat → BaseUCom dim) : Prop

structure VerifiedShorOnCode (N Δ k : Nat) (code : CSSCode) (L : LogicalBasis code k) : Prop

theorem verified_guarantees {N Δ k : Nat} {code : CSSCode} {L : LogicalBasis code k}
    (h : VerifiedShorOnCode N Δ k code L) :
    code.valid = true ∧ code.is_qldpc_code Δ = true ∧ L.valid = true ∧
    ¬ Nat.Prime N ∧
    (∃ a r m bits u, LogicalShorSucceeds a r N m bits u ∧ OracleRealizedOnCode code L u)