other

allFieldResultRecords status ledger for appendix

Lean spine source

Declarations: allFieldResultRecords

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.

def allFieldResultRecords : List FieldResultRecord :=
  cirl_field_result_records ++
  shutdown_field_result_records ++
  interruptibility_field_result_records ++
  corrigibility_field_result_records ++
  impact_field_result_records ++
  quantilization_field_result_records ++
  debate_field_result_records ++
  elk_field_result_records ++
  amplification_field_result_records