S1 hygiene: Lake package, Lean CI, and non-trivial lemmas

[NetworkYum]

Summary

Advances Causal Integrity from an orphan Lean axiom sketch toward S1 hygiene: a reproducible Lake package, CI that runs lake build, and derived lemmas that combine axioms rather than only projecting them. Status docs stay honest — this is still a skeleton / hypothesis, not a finished ethical OS.

Framing preserved: coherent causality preferred by action remains the foundation; property is a proof instrument.

What builds

• Lean 4.33.0 via lean-toolchain
• Lake package CausalIntegrity (lakefile.toml, srcDir = formalizations)
• lake build succeeds locally
• GitHub Actions: .github/workflows/lean.yml (leanprover/lean-action)

Library layout

Module	Role
formalizations/CausalIntegrity.lean	Root re-export
formalizations/CausalIntegrity/Axioms.lean	Sorts, predicates, axioms 0–4 & 6, Consent
formalizations/CausalIntegrity/Lemmas.lean	Derived lemmas

Lemmas added (non-trivial / multi-axiom)

• Consent hygiene: incapacitated / coerced / revoked cannot witness Consent
• Agent filter (“nature” attack): non-communicator / non-disputer ⇒ ¬MoralAgent
• Homestead: Null-capture via primitive Unowned + exclusivity for distinct agents
• Theft-shaped: distinct non-consensual interferer neither co-owns nor preserves coherency; homestead-then-seize chain (Axioms 1–3)
• Liability ≠ ownership: unconsented damage ⇒ restitution debt ∧ ¬Owns(damager) (butterfly / exhaust patch)
• Preference link: interference yields a state outside the Coherent class every agent prefers (Axioms 3–4)

Encoding note

FOL Axiom 1 uses timeless ¬∃ Owns, which collapses under capture without a state index. Lean uses a primitive Unowned Null marker with the same intended meaning (documented in axioms.md / formalizations README).

Explicitly out of scope for this S1 slice

• Axiom 5 (UPB / performative contradiction) — needs a language of rules; commented as scoped out
• Forward simulation / pre-action API — S2/S3
• Full non-vacuous Capable / Coerced / Direct thresholds
• Temporal multi-step ownership ledger
• Neural mapping / S2–S3 completeness

Docs

Updated formalizations/README.md, docs/definition-of-done.md, root README status table, abstract/llms/citation/overview/open-problems so S1 is described as hygiene in progress, not “S1 complete.”

Follow-up (repo metadata, not in this PR)

GitHub topics currently include typos that hurt discoverability: alighment → alignment, deontogical-ethics → deontological-ethics, univerally-preferable-behavior → universally-preferable-behavior. These need a repo-settings edit (not available via this PR).

How to verify

lake build

CI should report green on this PR.