bridge

MB7c Adversarial robustness

Lean spine source

Declarations: MB7c_hidden_biq_to_adversarial_robustness

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.

axiom MB7c_hidden_biq_to_adversarial_robustness :
  ∀ A : System, CorrectionIntegrity A → HiddenBIQBoundedSys A → AdversariallyRobust A

/-- MB7d: inferential-UAD detector validity. Access-robust discovery plus adequate
    inferential detector assumptions warrants inferential-coupling measurements.
    The internal `P_meta` structure is an audit certificate, not a commitment
    that agents symbolically represent the prior. -/