[SnO2WMaN]

Rewrites Neighborhood/Logic/Calculus.lean. Every derivation is now spelled out one inference per have, at the granularity of a hand-written proof, and the derived axiom schemes are grouped by their conclusion.

Proof style

Each derivation is a sequence of fully annotated have steps ending in exact, with no automation, so that a reader can follow it line by line against the informal argument. For instance, T from C, D, B and 5:

instance [L.HasAxiomC] [L.HasAxiomD] [L.HasAxiomB] [L.HasAxiomFive] : L.HasAxiomT := by
  constructor;
  intro A;
  have h₁ : ◇□A ⋏ ∼□A 🡒 □A ∈ L := C_trans and₁ diaFivec;
  ...

Organization

• Derivations are written directly in their instance rather than routed through a named axiom<X>_of_<YZ> lemma; axiomK_of_MC, axiomP_of_ND and axiomP_of_MD are dropped accordingly, and box_mono_of_KN becomes rm_of_KN.
• The derived axiom schemes are grouped by conclusion (M, C, K, N, P, D, T, B, Four, Five), with the duals (EDiaNNBox, diaTc, CNBoxNBox, diaBc, diaFourc, CNBoxBoxNBox, diaFivec) and the rules (rm, rmDia, nec) in sections of their own. EDiaNNBox, CNBoxNBox and CNBoxBoxNBox are no longer private.
• The duplicated HasAxiomT instance derived from D, B and 4 is merged into one.
• The step shared by the N derivations is factored out as axiomN_of_box.
• Per-declaration docstrings, which only restated their statements, are removed; the module docstring and the section headers remain.

No statement, hypothesis or public name changes: re, multire, rm, rmDia, nec, diaTc, the axiom* and axiom*_subset families, axiomGeach and every HasAxiom* class keep their names and types, so no other module needed a change.

🤖 Generated with Claude Code

https://claude.ai/code/session_01JtZoFzbXnkxpRa6JmZqpme