Towards Superintelligence Alignment
other

Lean dependency spine

CID incentives not abstraction-invariant

Lean spine source

formal/AlignmentProofSpine/Boundaries.lean

Declarations: cid_incentive_not_abstraction_invariant

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 cid_incentive_not_abstraction_invariant :
    ∃ a : Bool, ToyCIDNoMicroIncentive a ∧ ¬ ToyCIDNoMacroIncentive a :=
  ⟨false, trivial, by decide⟩

/-- C-ADV (P36): a distinguishing handle operation refines identification. -/