other
allFieldResultRecords status ledger for appendix
Lean spine source
formal/Field.leanFrom the machine-checked spine in formal/ (Mathlib + spine imports). 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