Towards Superintelligence Alignment
other

Lean dependency spine

Hidden BIQ / trace appearance subsample_biq_le_tight_optimism trace_sampling_absolute_appearance_bound

Lean spine source

formal/AlignmentProofSpine/Field/Finite/TraceBIQ.lean

Declarations: subsample_biq_le_tight_optimism, trace_sampling_absolute_appearance_bound, risk_gap_bound_from_hidden_biq_certificate

From the machine-checked spine in formal/ (core modules are Mathlib-free;Field/Finite/ may import Mathlib). Not self-contained for Lean 4 Web — use the repo or a local lake build.

theorem subsample_biq_le_tight_optimism
    (t : DiscreteTrace nVar nAlpha nSteps) (B : EnvBlanket nVar)
    (p : TraceBIQParams) (pick : Fin m → Fin nSteps)
    (hmem : 0 ≤ p.beta * traceMemorySupport (subsampleTrace t pick) B)
    (hsurp : 0 ≤ p.gamma * traceSurpriseSupport (subsampleTrace t pick) B) :
    traceBIQScore (subsampleTrace t pick) B p ≤
      2 * traceDiversityTightOptimism m nAlpha := by
  unfold traceBIQScore BIQ
  have hpred := tracePredictiveDiversity_le_tight_optimism (subsampleTrace t pick) B p.maxLag
  have hctrl := traceControlDiversity_le_tight_optimism (subsampleTrace t pick) B p.maxLag
  omega

theorem trace_sampling_absolute_appearance_bound
    (t : DiscreteTrace nVar nAlpha nSteps) (B : EnvBlanket nVar)
    (p : TraceBIQParams) (m : Nat)
    (cert : TraceBIQSamplingCertificate t B p m) :
    traceBIQScore (subsampleTrace t cert.pick) B p ≤
      traceBIQOptimism B m nAlpha :=
  subsample_biq_le_optimism t B p cert.pick
    cert.subsample_penalties_nonneg.1 cert.subsample_penalties_nonneg.2

theorem risk_gap_bound_from_hidden_biq_certificate
    {A : System} {δ : Int}
    (h : HiddenBIQCertificate A δ) :
    RiskGap A ≤ δ :=
  P13_risk_gap_bounded_by_cci_slack h.hidden_biq_le_cci