apodictic machine-checked praxeology

2. The Archaeology🔗

How the result came to be stated the way it is. This part goes through the trusted base axiom by axiom, in the order the axioms were forced, with the encodings we tried and rejected along the way. The rejected code is type-checked here, so the reasons for rejection can be inspected rather than trusted.

The part is written from the lab notes of 2026-08-02, 2026-09-04 and 2026-09-05, and from Nozick's 1977 paper, read 2026-09-04. Docstrings quoted here are pulled live from the library and carry pedigree only; the history is in this part and nowhere in the code.

  1. 2.1. The receipt
  2. 2.2. World: the frame the axioms speak of
  3. 2.3. ends_distinguishable: ends can be told apart
  4. 2.4. actual_disposition: which plan is the agent's
  5. 2.5. swap_dominance: the one praxeological premise
  6. 2.6. The hypotheses
  7. 2.7. The units: where interchangeability is used
  8. 2.8. What the law does not rest on
  9. 2.9. Consistency
  10. 2.10. Methodological findings