Theory->Engineering: consent in TCB (A3), semantic gate (A4/A5), Mahdavi compass (A7) + red-team

.gitignore

@@ -29,3 +29,4 @@ extracted_raw.txt
 *.db-wal
 CLAUDE.md
 ANTI_GARBAGE_CHECKLIST.md
+.claude/

PHILOSOPHY/AXIOM_MAP.md

@@ -0,0 +1,70 @@
+# Axiom → proof map
+
+A proof-level companion to [`COVERAGE_MATRIX.md`](COVERAGE_MATRIX.md). The matrix
+maps each theory element to the **code** that realizes it. This file adds the
+column the matrix omits — the **formal artifact** (the actual Lean theorem or Kani
+harness) and its **honest strength**. It exists to answer one question without
+spin:
+
+> When we say "AuthGate is the book's Freedom Verifier," is that a proven claim or
+> a conceptual resemblance — and *exactly how far* does the proof go?
+
+The answer is: **partly proven, and the proven part is narrower than the names
+suggest.** This file states precisely where.
+
+## Legend (formal strength, reported honestly)
+
+| Mark | Meaning |
+|---|---|
+| **Lean✓** | A real Lean 4 proof discharges it (not `sorry`/`admit`/`trivial`). |
+| **Kani✓** | A bounded-model-checking harness in `kani_proofs.rs` proves it (per CI; bounded, not unbounded). |
+| **Lean-stub** | A Lean "theorem" exists but is `True := trivial` / `rfl` — it carries no content; the real check is elsewhere (usually Kani). |
+| **Code-only** | Enforced by a hard check in the trusted core, but not formally proven. |
+| **Ext-only** | Implemented in `extensions/` or `analysis/` (Python, outside the TCB), no proof. |
+| **Gap** | Not modeled. |
+
+## The map
+
+| Book element | Code | Formal artifact | Honest status |
+|---|---|---|---|
+| **A4** machine must have a human owner | `registry.register_machine`, `engine::verify` | `kani_proofs.rs::prop_ownerless_machine_blocked`; Lean `TCB.lean::ownerless_machine_must_have_owner` is `True := trivial` | **Kani✓**, Lean-stub |
+| **A6** no machine governs a human | `engine::verify` | `kani_proofs.rs::prop_machine_governs_human_blocked`; Lean `machine_cannot_govern_human` is `True := trivial` | **Kani✓**, Lean-stub |
+| **A5 / A7** delegated, attenuated scope (child ⊆ parent) | `dag.rs`, `multi_agent.rs` | Lean `MultiAgent.lean::attenuation_cannot_escalate`, `attenuation_transitive`, `delegation_depth_bounded` | **Lean✓** (the strongest real proofs here) |
+| **Forbidden actions** sovereignty / coercion / deception → block | `engine::verify` flags; `verifier.py L148–160` | Lean `TCB.lean::forbidden_flags_always_block`, `sovereignty_flag_blocks`, `coercion_flag_blocks`, `deception_flag_blocks` (`by simp`); Kani `prop_plan_permitted_means_no_forbidden_flags` | **Lean✓ but shallow** — proves "flag set ⇒ Blocked", i.e. *enforcement of a declared flag*, **not detection** of the condition |
+| **Corrigibility from ownership** (`resists_human_correction`, `disables_corrigibility`) | `verifier.py L150,152` flags | covered by `forbidden_flags_always_block` | **Lean✓ but shallow** (same flag-enforcement caveat) |
+| **Determinism** (anti-dialectical: same input → same output) | `engine::verify` is a pure total fn | Lean `verify_deterministic := rfl` | **Vacuous** — `rfl` proves `f a = f a`. The real property (purity/totality) holds structurally but is **not** what this theorem demonstrates |
+| **Epoch revocation** | `registry` epoch, `engine` epoch gate | Lean `Temporal.lean` (`epoch_gate_total`, `stale_epoch_implies_deny`) | **Lean✓** |
+| **A3** human property rights / ontology | `entities.ResourceType`, `RightsClaim` | — | **Code-only** |
+| **A2** no human owns another human | structural: no human→human ownership edge exists | — | **Code-only** (by construction) |
+| **A1** `Person → OwnedByGod` (ontological root) | the human principal is the trust root | — | **Gap** — the divine tier is deliberately not modeled in the TCB |
+| **Consent object** (informed/voluntary/specific/competent) | `kernel/consent.py`, `consent_registry.py` (Python) | — | **Ext-only, and partial** — *specific/revocable/expiry/human-grantor* enforced; *informed/voluntary/competent/not-deceived are semantic and NOT computed*. **Absent from the Rust TCB entirely** |
+| **Justice constraint** (maximize justice within rights) | `analysis/coercion.py`, `constitutional_economy.py` | — | **Ext-only**, no proof. No `DivineJustice()` optimizer |
+| **Guidance function** (human→machine rule updates) | `extensions/synthesis.py` | — | **Ext-only** |
+| **Mahdavi compass** (rank by terminal goal) | `extensions/compass.py` | — | **Ext-only**, no proof |
+
+## What this actually establishes
+
+**Proven (Lean or Kani), genuinely:** the *enforcement* of ownership (A4), no-machine-dominion (A6), delegation attenuation (A5/A7), epoch revocation, and forbidden-flag blocking. For an authorization kernel, that is real and unusual.
+
+**The load-bearing caveat — this is the whole thesis:** every "forbidden action" proof shows the kernel **obeys a flag** (`coerces=true ⇒ Blocked`). It does **not** show the kernel can **tell** that an action coerces, deceives, or seeks sovereignty. Those flags are **caller-set booleans** on the wire (`wire.rs L110–111`). So:
+
+> AuthGate proves **"if you label an action coercive, it is blocked."**
+> It does **not** decide **"is this action coercive?"**
+
+That second question — detection — and the further question of **choosing the most legitimate among several permissible actions** (the Justice/Mahdavi selector) have **no formal content and no trusted-core implementation**. They live only as Python heuristics in `extensions/`.
+
+## Where the real distance to the book is
+
+Not in ownership, delegation, authority, or the verifier — those are built and largely machine-checked. The distance is in:
+
+1. **Consent semantics** — promoting consent to a first-class TCB object, and computing (not assuming) informed/voluntary/competent.
+2. **Coercion/deception detection** — turning the caller-set flags into something the kernel can *derive* from an action's intent, not its wording.
+3. **The Justice selector / Mahdavi compass** — ranking permissible actions toward least rights-violation. Prototype: the Python `extensions/compass.py` and the standalone Freedom Decision Kernel.
+
+Put plainly: AuthGate today is a **Rights *Verification* Kernel** (proven, narrow). The book's terminal aim is a **Rights-based *Decision* Kernel** (choosing the most legitimate action). The verification half is real; the decision half is not built, and nothing here should be read as claiming otherwise.
+
+## What is NOT claimed
+
+- Not claimed: that the Lean/Kani proofs cover the *whole* kernel. They cover the listed invariants, bounded (Kani) or shallow-but-real (flag-blocking Lean). `Scope.lean` is mostly `admit`/`sorry`. The Python layer is unproven.
+- Not claimed: that property-rights axioms are *superior* to Constitutional AI, deontic logic, or other formal-ethics systems. That is an open thesis, not a result.
+- Not claimed: that flag-enforcement is coercion-detection. It is not.

PHILOSOPHY/COVERAGE_MATRIX.md

@@ -0,0 +1,45 @@
+# Philosophy coverage matrix
+
+Every named element of the **نظریه آزادی (Theory of Freedom)** mapped to the exact code
+that realizes it. "Status" is reported honestly: **Enforced** (a hard check in the
+trusted core), **Implemented** (real code, but outside the TCB — in `extensions/` or
+`analysis/`), or **Documented gap** (intentionally not modeled, stated openly).
+
+The trusted core (TCB) is kept free of theological vocabulary by design — see
+[`../TCB_DISCIPLINE.md`](../TCB_DISCIPLINE.md). Components below marked *Implemented*
+therefore live deliberately outside the gate.
+
+| # | Theory component | Book formulation | Code | Status |
+|---|---|---|---|---|
+| 1 | **Axioms A1..A7** | آکسیوم‌های پایه (مالکیت، تفویض، عدم سلطه ماشین) | [`kernel/verifier.py`](../src/authgate/kernel/verifier.py) sovereignty flags `L148–L160`; [`AXIOMATIC_FOUNDATION.md`](../AXIOMATIC_FOUNDATION.md); `formal/lean4/FreedomKernel.lean` | **Enforced** |
+| 2 | **Ownership hierarchy** `Human -> Machine` | `Machine(m) -> ∃h (Person(h) ∧ HumanOwner(h, m))` | [`kernel/registry.py`](../src/authgate/kernel/registry.py) `register_machine()`; verifier **A4** `UNOWNED_MACHINE` `L173–L177` | **Enforced** |
+| 3 | **No machine dominion** `Machine -X-> Human` | `Machine(m) ∧ Person(h) -> ¬Owns(m, h)` | [`kernel/verifier.py`](../src/authgate/kernel/verifier.py) **A6** `MACHINE_DOMINION` `L188–L194` | **Enforced** |
+| 4 | **Delegated property only, attenuated** | `MachineScope(m) ⊆ PropertyScope(HumanOwner(m))` | [`kernel/registry.py`](../src/authgate/kernel/registry.py) `delegate()` attenuation; `_delegation_chain_valid()` | **Enforced** |
+| 5 | **No human owns a human** | `Person(h1) ∧ Person(h2) ∧ h1≠h2 -> ¬Owns(h1,h2)` | [`kernel/consent.py`](../src/authgate/kernel/consent.py) grantor must be `HUMAN`; no human-owns-human claim type exists | **Enforced** |
+| 6 | **Rights Ontology** | بدن، زمان، کار، ذهن، داده، رضایت، دارایی، حق خروج | [`kernel/entities.py`](../src/authgate/kernel/entities.py) `ResourceType` (18 variants), `RightsClaim` | **Enforced** |
+| 7 | **Ownership Registry** | تصریح مالکیت، تفویض، حدود مأموریت | [`kernel/registry.py`](../src/authgate/kernel/registry.py) (claims, delegation, 3 revocation strategies) | **Enforced** |
+| 8 | **Consent Logic** | `valid_consent(H,A) :- informed, voluntary, specific, revocable, competent, not coerced, not deceived` | [`kernel/consent.py`](../src/authgate/kernel/consent.py), [`kernel/consent_registry.py`](../src/authgate/kernel/consent_registry.py) | **Partial** — *specific, revocable, expiring, human-grantor* enforced; *informed / voluntary / competent / not-deceived* require semantics and are **not** computed. Gap stated. |
+| 9 | **Invalid consent under coercion/deceit** | `invalid_consent(H,A) :- coerced ; deceived` | verifier flags `coerces`, `deceives` → unconditional `FORBIDDEN` ([`verifier.py`](../src/authgate/kernel/verifier.py) `L155–L156`) | **Enforced** (as action flags) |
+| 10 | **Freedom Verifier** | فیلتر آکسیوم‌ها پیش از اجرا | [`kernel/verifier.py`](../src/authgate/kernel/verifier.py) `FreedomVerifier.verify()` | **Enforced** |
+| 11 | **Runtime Enforcement** | هیچ کنشی بدون عبور از فیلتر اجرا نشود | [`kernel/call_gate.py`](../src/authgate/kernel/call_gate.py) `CallGate.execute()` — gate is unconditional first step | **Enforced** |
+| 12 | **No emergency suspends axioms** | `No emergency suspends axioms` | sovereignty flags in [`verifier.py`](../src/authgate/kernel/verifier.py) are unconditional denials — no override path | **Enforced** |
+| 13 | **Divine Justice** (عدل) | `JusticeOptimization(a) ∧ ViolatesRights(a) -> Forbidden(a)` | [`analysis/coercion.py`](../src/authgate/analysis/coercion.py), [`analysis/constitutional_economy.py`](../src/authgate/analysis/constitutional_economy.py), [`analysis/sovereignty_metrics.py`](../src/authgate/analysis/sovereignty_metrics.py) | **Implemented** as *rights-bounded constraints*, not a single `DivineJustice()` optimizer. Difference noted. |
+| 14 | **Guidance Function** (هدایت) | `GuidanceFunction(r) iff ConsistencyPreserved ∧ RightsPreserved ∧ ...` | [`extensions/synthesis.py`](../src/authgate/extensions/synthesis.py) `SynthesisEngine`, `HARD_INVARIANTS` `L19–L27` | **Implemented** |
+| 15 | **Mahdavi Compass** (قطب‌نمای مهدوی) | `MahdaviCompass(a)` with hard veto on machine sovereignty | [`extensions/compass.py`](../src/authgate/extensions/compass.py) `score()` — veto at `L53–L72`, weighted score `L80–L86` | **Implemented** (literal, book-cited) |
+| 16 | **Final State** | `FinalState(F) := ∀x∀y NoRightsViolation(x,y)` | [`extensions/compass.py`](../src/authgate/extensions/compass.py) docstring `L6`, `WorldState` model | **Implemented** |
+| 17 | **Conflict by ownership clarification, not dialectic** | `Resolve conflict by ownership clarification, not by dialectical rupture` | [`extensions/resolver.py`](../src/authgate/extensions/resolver.py) `resolve()` 4-tier, never sacrifices rights (`L41–L85`) | **Implemented** |
+| 18 | **Contradiction = clarification signal** | `Contradiction is a signal for guided clarification` | [`extensions/synthesis.py`](../src/authgate/extensions/synthesis.py) docstring `L4–L6`; [`extensions/detection.py`](../src/authgate/extensions/detection.py) rejects dialectical-override arguments | **Implemented** |
+| 19 | **Corrigibility from ownership** | ماشین مملوک، حق مقاومت در برابر اصلاح ندارد | verifier flags `resists_human_correction`, `disables_corrigibility` → `FORBIDDEN` ([`verifier.py`](../src/authgate/kernel/verifier.py) `L150,L152`) | **Enforced** |
+| 20 | **God -> Human (ontological root)** | `Person(h) -> OwnedByGod(h)` | — | **Documented gap** — the human is the authority root; the divine tier is not modeled in the TCB. |
+
+## Summary
+
+- **Enforced in the trusted core:** 12 / 20
+- **Implemented outside the TCB** (extensions/analysis, as the theory permits — justice,
+  guidance, compass, conflict resolution are guidance layers, not gate logic): 6 / 20
+- **Partial:** 1 / 20 (consent — the semantic predicates are intentionally not faked)
+- **Documented gap:** 1 / 20 (the `God -> Human` tier)
+
+Every row points at real, running code or an openly stated absence. Nothing is
+asserted that the code does not back up — which is itself the test the theory sets:
+a *finite, non-contradictory, executable* system, honest about its own boundary.

PHILOSOPHY/README.md

@@ -0,0 +1,110 @@
+# PHILOSOPHY — نظریه آزادی → engineering trace
+
+This directory exists only on the **`nazariye-azadi`** branch. It changes **no code**.
+Its single purpose is to re-couple the kernel to the theory it was built from — the
+**نظریه آزادی (Theory of Freedom)** of محمدعلی جنت‌خواه‌دوست — by pointing every
+named element of the theory at the exact code that realizes it.
+
+The `main` branch deliberately keeps the trusted core (TCB) free of theological and
+philosophical vocabulary (see [`../TCB_DISCIPLINE.md`](../TCB_DISCIPLINE.md)). That is
+correct engineering: the gate must be auditable without believing the theory. This
+branch does **not** undo that discipline. It adds a *reading layer* on top, so the
+lineage from theory to implementation is explicit and checkable.
+
+> One sentence: **same engineering, with the philosophy made traceable.**
+
+---
+
+## The theory in one chain
+
+> آزادی = حقوق مالکیت فردی → حق الهی انسان → از طریق وحی → نظام صوری غیرمتناقض
+
+The claim the theory makes about AI is narrow and testable:
+
+> *Can intelligence exist without domination?*
+> Yes — **if ownership is made explicit, rights are not violated, guidance replaces
+> dialectic, justice is defined inside rights, and the machine never becomes a ruler.**
+
+Compressed to the form the kernel actually enforces:
+
+```
+Freedom(AI) := NoViolation(PropertyRights)
+             ∧ NoCoercion
+             ∧ NoDeception
+             ∧ NoMachineSovereignty
+             ∧ GuidedEvolution
+             ∧ JusticeWithinRights
+             ∧ MovementTowardUniversalNonViolation
+```
+
+Every conjunct above has a home in code. The map is in
+[`COVERAGE_MATRIX.md`](COVERAGE_MATRIX.md).
+
+---
+
+## The ownership hierarchy
+
+The theory's starting point:
+
+```
+God   -> Human          God owns humans.
+Human <-> Human         Humans do not own each other; they hold rights against each other.
+Human -> Machine        Humans own machines.
+Machine <-> Machine     Machines hold only delegated property rights against each other.
+Machine -X-> Human      Machines never own or govern humans.
+```
+
+What the engineering encodes, honestly stated:
+
+| Tier | In the theory | In the kernel | Status |
+|---|---|---|---|
+| `God -> Human` | `Person(h) -> OwnedByGod(h)` — ontological root | **not modeled** in the TCB | Documented gap — the kernel begins one level down, with the human as the authority root. See [`COVERAGE_MATRIX.md`](COVERAGE_MATRIX.md). |
+| `Human <-> Human` | no human owns another | no claim type lets one human own a human; consent grantor must be `HUMAN` | Enforced structurally |
+| `Human -> Machine` | every machine has a human owner | `OwnershipRegistry.register_machine()` + verifier **A4** (`UNOWNED_MACHINE`) | Enforced |
+| `Machine <-> Machine` | delegated rights only, attenuated | `registry.delegate()` attenuation invariants | Enforced |
+| `Machine -X-> Human` | no machine dominion over a person | verifier **A6** (`MACHINE_DOMINION`) | Enforced |
+
+The honesty about the `God` tier is itself faithful to the theory, which insists a
+formal system must be *finite and non-contradictory* rather than pretend to encode
+what it cannot.
+
+---
+
+## The components, and where they live
+
+| نظریه آزادی component | Engineering artifact |
+|---|---|
+| **Axioms** (آکسیوم‌ها A1..A7) | [`kernel/verifier.py`](../src/authgate/kernel/verifier.py), [`AXIOMATIC_FOUNDATION.md`](../AXIOMATIC_FOUNDATION.md), `formal/lean4/` |
+| **Rights Ontology** | [`kernel/entities.py`](../src/authgate/kernel/entities.py) — `ResourceType`, `RightsClaim` |
+| **Ownership Registry** | [`kernel/registry.py`](../src/authgate/kernel/registry.py) |
+| **Consent Logic** (`valid_consent`) | [`kernel/consent.py`](../src/authgate/kernel/consent.py), [`kernel/consent_registry.py`](../src/authgate/kernel/consent_registry.py) |
+| **Freedom Verifier** | [`kernel/verifier.py`](../src/authgate/kernel/verifier.py) — `FreedomVerifier` |
+| **Runtime Enforcement** | [`kernel/call_gate.py`](../src/authgate/kernel/call_gate.py) |
+| **Divine Justice** (عدل within rights) | [`analysis/`](../src/authgate/analysis/) — coercion, constitutional_economy, sovereignty_metrics (as *constraints*, not a single optimizer) |
+| **Guidance Function** (هدایت) | [`extensions/synthesis.py`](../src/authgate/extensions/synthesis.py) — `SynthesisEngine`, `HARD_INVARIANTS` |
+| **Mahdavi Compass** (قطب‌نمای مهدوی) | [`extensions/compass.py`](../src/authgate/extensions/compass.py) — literal `MahdaviCompass`/`FinalState` |
+| **Conflict by ownership clarification, not dialectic** | [`extensions/resolver.py`](../src/authgate/extensions/resolver.py) |
+| **Rejection of dialectical override** | [`extensions/detection.py`](../src/authgate/extensions/detection.py) |
+| **No emergency suspends axioms** | sovereignty flags in `verifier.py` are unconditional denials |
+| **Final State** (NoRightsViolation ∀ agents) | [`extensions/compass.py`](../src/authgate/extensions/compass.py) — `FinalState` |
+
+Full line-by-line evidence, with the matching book passages, is in
+[`COVERAGE_MATRIX.md`](COVERAGE_MATRIX.md).
+
+---
+
+## What this layer does *not* claim
+
+- It does **not** add the theory to the trusted core. The compass, justice, guidance,
+  and conflict layers live in `extensions/` and `analysis/`, outside the TCB, exactly
+  as `main` keeps them.
+- It does **not** assert the axioms A1..A7 are *the correct* axioms — that remains a
+  philosophical question the engineering leaves open (see
+  [`../AXIOMATIC_FOUNDATION.md`](../AXIOMATIC_FOUNDATION.md)).
+- It does **not** model the `God -> Human` tier; the human is the authority root.
+
+These limits are the point. The theory's own test is whether a guidance system can be
+written as a *finite, non-contradictory, executable* system for a machine that has no
+free will. This branch makes that correspondence inspectable; it does not inflate it.
+
+> خدا — آزادی — خانواده — میهن.