Formal Predictions: 12 Verifiable Theorems by Chapter

The Governance Layer book makes 12 concrete, falsifiable predictions — four per chapter — about the behaviour of its algorithms. Each prediction is implemented as a Python function in src/governance/prove/predictions.py that sets up the required state, runs the scenario, asserts the predicted outcome, and returns a PredictionResult containing a PASS/FAIL flag and a human-readable evidence string. All 12 predictions pass against the current implementation and their results are committed to results/prove_results.json.

CLI Commands

# Run all 12 predictions
python -m src.governance.runner prove --all

# Run only Chapter 2 predictions (P01–P04)
python -m src.governance.runner prove --ch2

# Run only Chapter 3 predictions (P05–P08)
python -m src.governance.runner prove --ch3

# Run only Chapter 4 predictions (P09–P12)
python -m src.governance.runner prove --ch4

# Run a single prediction by number (1–12)
python -m src.governance.runner prove --single 5

# Export all results to a JSON file
python -m src.governance.runner prove --all --json results/ch_all.json

Output Format

The runner prints a summary block to stdout showing the PASS/FAIL status, prediction ID, chapter and section reference, description, and evidence string for each result.

============================================================
  Formal Prediction Verification
  12/12 PASS
============================================================

  [PASS] P01 (Ch2 §3.1) Budget enforces proposal cap
         Member budget=3, submitted=10, agenda=3

  [PASS] P02 (Ch2 §3.2) Priority ordering: CRITICAL_SAFETY before ROUTINE
         First in agenda: critical_first (tag=CRITICAL_SAFETY)

  [PASS] P05 (Ch3 §2.1) Contract restricts action set
         Action 7 blocked=True, action 3 blocked=False

  [PASS] P12 (Ch4 §3.6) Deadlock breaker fires after N consecutive defaults, then resets
         After 5 defaults: fired=True, after reset: still_fired=False

============================================================
  Summary: 12/12 predictions verified
============================================================

Predictions by Chapter

Chapter 2 — Neural Parliament
Chapter 3 — Ulysses Contracts
Chapter 4 — Identity Layer

Chapter 2 predictions verify the Parliament’s core deliberation mechanics: budget enforcement, priority ordering, weighted voting, and tag-compliance penalties.

ID	Section	Description	Evidence (from results)
P01	§3.1	Budget enforces proposal cap	`Member budget=3, submitted=10, agenda=3`
P02	§3.2	`CRITICAL_SAFETY` ordered before `ROUTINE`	`First in agenda: critical_first (tag=CRITICAL_SAFETY)`
P03	§3.4	Weighted vote matches formal spec	`Weighted avg=0.000, threshold=0.5, decision=default`
P04	§3.7	Tag compliance halves budget after 3+ falsifications in a single cycle	`Initial budget=3, final budget=1 (expected <= 1)`

python -m src.governance.runner prove --ch2

Chapter 3 predictions verify the Ulysses Contract lifecycle: action-set restriction, asymmetric revocation thresholds, timelock mechanics, and mask composition.

ID	Section	Description	Evidence (from results)
P05	§2.1	Enacted contract restricts action index 7	`Action 7 blocked=True, action 3 blocked=False`
P06	§2.3	Revocation harder than enactment	`Enactment threshold=0.66, Revocation threshold=1.0`
P07	§2.4	Timelock decrements over time, preventing immediate revocation	`Timelock before decrement=10, after decrement=9`
P08	§3.0	Mask composition: `allowed − restricted = final`	`Allowed={1, 2, 3, 7, 8, 9} - Restricted={8, 7} = {1, 2, 3, 9}`

python -m src.governance.runner prove --ch3

Chapter 4 predictions verify identity protection: coherence-triggered vetoes, tier-4 constitutional multisig requirements, genesis 3-of-5 authorisation, and deadlock breaker recovery.

ID	Section	Description	Evidence (from results)
P09	§2.1	Low-coherence proposal triggers integrity veto or rejection	`Coherence=0.1, integrity score=1.00, default=True`
P10	§2.5	Tier-4 (Constitutional) requires external multisig; lower tiers do not	`CONSTITUTIONAL requires multisig=True, OPERATIONAL requires multisig=False, DYNAMIC requires multisig=False`
P11	§3.1	Genesis 3-of-5 multisig: 2 sigs insufficient, 3 sigs authorizes	`Sigs=2 authorized=False, Sigs=3 authorized=True`
P12	§3.6	Deadlock breaker fires after N consecutive defaults, then resets	`After 5 defaults: fired=True, after reset: still_fired=False`

python -m src.governance.runner prove --ch4

JSON Export

Pass --json <path> to write the full result set to a JSON file. The schema matches results/prove_results.json:

{
  "predictions": [
    {
      "id": 1,
      "chapter": "Ch2",
      "section": "3.1",
      "description": "Budget enforces proposal cap",
      "passed": true,
      "evidence": "Member budget=3, submitted=10, agenda=3"
    },
    {
      "id": 2,
      "chapter": "Ch2",
      "section": "3.2",
      "description": "Priority ordering: CRITICAL_SAFETY before ROUTINE",
      "passed": true,
      "evidence": "First in agenda: critical_first (tag=CRITICAL_SAFETY)"
    }
  ],
  "passed": 12,
  "total": 12
}

The committed file at results/prove_results.json records the 12/12 PASS result from the reference implementation.

Lean 4 Machine-Checked Proofs

Two theorems from the Python predictions are additionally verified in Lean 4 in the gov-budget-proof/ directory. These proofs are fully machine-checked and do not rely on runtime test execution.

gov-budget-proof/
├── GovBudgetProof.lean          ← imports all modules
├── GovBudgetProof/
│   ├── Basic.lean
│   ├── BudgetEnforcement.lean   ← κ₂ budget invariant
│   └── VoteAndFalsification.lean ← vote threshold & falsification
└── lakefile.toml

BudgetEnforcement.lean

Proves the budget enforcement invariant (κ₂): for all possible governance cycles, no member’s used counter exceeds their budgets value. The proof covers processProposal, processCycle, and induction over arbitrary proposal lists. Corresponds to Prediction P01.

VoteAndFalsification.lean

Proves vote threshold consistency and determinism: vote resolution is deterministic (law of excluded middle), equal vote lists produce the same outcome, and budget halving preserves b ≥ 1 when starting from b ≥ 1. Directly corresponds to Predictions P03 and P04.

The Lean proofs cover the algebraic invariants that are hardest to test exhaustively at runtime — in particular, the inductive argument that budget enforcement holds for an arbitrary list of proposals, not just the finite cases exercised by the Python tests.

The Lean proofs require Lean 4 and the Mathlib toolchain defined in gov-budget-proof/lean-toolchain. They are not needed to run the Python prediction suite. Run lake build inside gov-budget-proof/ to check them locally.

Introduction

Core Framework

Running Experiments

Configuration & Integration

Formal Predictions: 12 Verifiable Theorems by Chapter

CLI Commands

Output Format

Predictions by Chapter

JSON Export

Lean 4 Machine-Checked Proofs

BudgetEnforcement.lean

VoteAndFalsification.lean

Build docs developers (and LLMs) love

Introduction

Core Framework

Running Experiments

Configuration & Integration

Documentation Index

​CLI Commands

​Output Format

​Predictions by Chapter

​JSON Export

​Lean 4 Machine-Checked Proofs

BudgetEnforcement.lean

VoteAndFalsification.lean

Build docs developers (and LLMs) love

CLI Commands

Output Format

Predictions by Chapter

JSON Export

Lean 4 Machine-Checked Proofs