feat(a-sounder-constitution): typed civic contagion simulator — rights as transition constraints

a-sounder-constitution/0.1-AI-MANIFEST.a2ml

@@ -0,0 +1,49 @@
+# SPDX-License-Identifier: MPL-2.0
+---
+### [META]
+id: "a-sounder-constitution"
+level: 1
+parent: "../0-AI-MANIFEST.a2ml"
+
+---
+### [AI_MANIFEST]
+description: |
+  Research proof-of-concept: a Plague Inc.-style civic simulator (a typed
+  cellular automaton) whose central claim is that RIGHTS ARE TYPE CONSTRAINTS
+  ON LEGAL STATE TRANSITIONS, not resources. A sound constitution makes
+  coercive downgrades of personhood (e.g. Person -> Property) unrepresentable;
+  an unsound one permits them and buys fast order by domination at the cost of
+  legitimacy and resilience.
+
+  Read README.adoc first, then docs/TYPE-THEORY.adoc, then formal/Constitution.idr.
+
+canonical_locations:
+  type_checker: "src/constitution.js"   # the central mechanic (sound vs unsound)
+  engine: "src/engine.js"               # cellular automaton + gliders + turn loop
+  catalogue: "src/scenarios.js"         # doctrine (glider) catalogue + scenarios
+  playable_ui: "web/"                   # canvas simulator (serve over HTTP)
+  headless_demo: "sim/compare.mjs"      # quantitative sound-vs-unsound proof
+  tests: "tests/"                       # node --test (mechanics + thesis-level)
+  formal_proof: "formal/Constitution.idr"
+  docs: "docs/"
+
+invariants:
+  - "The central thesis MUST stay enforced in BOTH layers: formal/Constitution.idr
+     (statically: Property has no inhabitant in the sound Person type) and
+     src/constitution.js (dynamically: checkTransition returns UNREPRESENTABLE)."
+  - "src/ is pure model logic with NO DOM dependency, so it runs identically in
+     the browser and in Node (tests + headless comparison)."
+  - "The simulation MUST stay deterministic given a seed (src/rng.js); the test
+     suite and sim/compare.mjs depend on it."
+  - "Coercive doctrine effects MUST be routed through checkTransition — never
+     applied directly — or the constitution stops meaning anything."
+  - "Zero runtime dependencies: Node 22 + a static file server + a browser."
+
+run:
+  headless: "node sim/compare.mjs   (or: npm run sim)"
+  tests: "node --test               (or: npm test)"
+  serve: "python3 -m http.server 8080  (or: npm run serve); open /web/"
+
+status: "pre-alpha research artefact; JS+tests+UI run today; Idris2 not yet CI-checked here"
+
+graduation_target: "typell (typed personhood-lattice core) once the JS/Idris bridge and TypeLL/QTT mapping land"

a-sounder-constitution/MOTIVATION.adoc

@@ -0,0 +1,131 @@
+// SPDX-License-Identifier: MPL-2.0
+// Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
+= Motivation, novelty, and graduation path
+Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
+:toc:
+:icons: font
+
+== The sharp thesis
+
+> Build a Plague&nbsp;Inc.-like civic simulator where the "pathogen" is not a
+> disease but a constitutional doctrine, norm, fear, right, or type error. The
+> main innovation is that **rights are not resources; they are type constraints
+> on legal state transitions.** An unsound constitution can produce fast stable
+> order by permitting domination. A sound constitution restricts coercive moves
+> but produces deeper resilience.
+
+== Why it looks novel (near-miss survey)
+
+The ingredients all exist; the synthesis does not appear to.
+
+[cols="1,2"]
+|===
+| Nearby work | What it has / lacks
+
+| Conway's Game of Life and CA playgrounds
+| The diffusion substrate (live/dead cells, gliders, emergent structures) — but
+  no civic semantics.
+
+| CA for political theory — e.g. a 2024 paper modelling Hobbes' state of nature
+  with cellular automata
+| Bottom-up emergence of order under weak common power. Closest in spirit. But
+  scalar/agent dynamics, *no type system over transitions*.
+
+| CA in the social sciences / urban simulation
+| Local rules → global social patterns. General substrate, not constitutional.
+
+| Plague Inc. and its open-source reimplementations
+| Patient zero, evolving traits, global spread, adaptive defensive response — the
+  exact game shape we borrow. Pathogen is biological, not doctrinal.
+|===
+
+What was *not* found is the middle of the Venn diagram: a website/project that
+models *constitutional type-safety*, *sound vs. unsound human personhood*, and
+*Reconstruction-style rights patches* as a *typed cellular automaton*. That is
+the gap this artefact occupies. Novel as a synthesis, not in every component.
+
+== Why a typed model beats a scalar one
+
+A normal political sim trades scalars: `freedom + security − unrest + economy`.
+Every outcome lies on a line and the game is a tug-of-war.
+
+This model instead turns on *illegal transitions*:
+
+----
+Human     -> Property
+Person    -> NonPerson
+Citizen   -> RightlessSubject
+Emergency -> PermanentPower
+Policing  -> UnreviewableCoercion
+Fear      -> UnlimitedExecutiveAuthority
+----
+
+In the sound model several of these are *unrepresentable*; in the unsound model
+they are permitted and may even be locally advantageous. Rights stop being a
+slider and become a *type system*: they determine which moves are legal. (Full
+argument in `docs/TYPE-THEORY.adoc`; the proof in `formal/Constitution.idr`.)
+
+== The two playable modes
+
+. *Unsound polity.* The human type is broken (`PropertyPerson` is an ordinary
+  constructor). Coercion is efficient; institutions stabilise quickly; the deeper
+  legitimacy score decays and the system becomes brittle. The grim lesson:
+  unsound systems can be stable and even efficient, but their stability is
+  domination.
+. *Sound polity.* The human type is protected (`personhood`, `notProperty`,
+  `dueProcess`, `equalProtection`). Coercion is hard to use; rights constraints
+  slow the player down; trust, legitimacy, and long-run resilience improve. The
+  system absorbs shocks without converting people into expendable units.
+
+The headless comparison (`sim/compare.mjs`) shows the resulting algorithmic
+distinction directly: *unsound = faster control, higher hidden damage; sound =
+slower intervention, stronger long-term resilience.*
+
+== Why this belongs in `ideas-to-alphas`
+
+The incubator matures findings from idea to alpha before they earn a typed
+production repo. This artefact is squarely that: its load-bearing claim is a
+*type-theoretic* one (a sound constitution makes domination unrepresentable), it
+ships an Idris2 formalization alongside an executable model, and it has a clear
+graduation story.
+
+The reframing also rhymes with the wider pipeline: TypeLL treats safety as an
+*open-ended progression of type constraints*. "Personhood as a type-protected
+record whose coercive downgrades are unrepresentable" is the same move applied to
+civic state — and "standing may only ever be recognised/upgraded, never
+stripped" (`soundMonotone`) is a monotonicity discipline of exactly the kind the
+pipeline studies elsewhere.
+
+== Graduation path
+
+[cols="1,3"]
+|===
+| Step | Target
+
+| Research complete (this dir)
+| `idris2 --check formal/Constitution.idr` passes with zero `believe_me`; JS
+  engine + tests + comparison stable (✔ today).
+
+| Tighten the bridge
+| Make `src/constitution.js` the *extracted decision procedure* for `SoundStep`
+  + `SoundRestrict`, from a single shared spec, so the JS and Idris cannot drift.
+
+| Reconcile with TypeLL
+| Map "standing" onto the TypeLL personhood/QTT lattice; decide whether
+  `soundMonotone` is an instance of an existing grade-monotonicity result.
+
+| Promote
+| If the personhood-lattice connection lands, the typed core graduates toward
+  `typell`; the simulator remains here as the explanatory front-end.
+|===
+
+== Open questions
+
+. Is "standing" (`Full`/`Partial`/`NonCitizen`) a QTT grade, or a separate
+  lattice that the grade lattice acts on?
+. The proof-obligation pattern (`SoundRestrict`) is a refinement type in
+  disguise. Should admissible-but-constrained coercion be modelled with full
+  dependent refinement (`{r : Restriction | reviewable r ∧ narrow r}`)?
+. The simulator's `legitimacyDebt` is a scalar today. Is there a typed account of
+  *debt* — e.g. a linear resource that an unsound move *must* allocate and can
+  never free — that would make "hidden damage" itself unrepresentable-to-ignore?

a-sounder-constitution/README.adoc

@@ -0,0 +1,112 @@
+// SPDX-License-Identifier: MPL-2.0
+// Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
+= A Sounder Constitution — a civic contagion simulator
+Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
+:toc:
+:icons: font
+
+A Plague&nbsp;Inc.-style civic simulator where the "pathogen" is not a disease
+but a *constitutional doctrine, norm, fear, right, or type error*.
+
+[IMPORTANT]
+====
+The one idea: **rights are not resources; they are type constraints on legal
+state transitions.** An *unsound* constitution can produce fast, stable order by
+permitting domination. A *sound* constitution restricts coercive moves — it makes
+some of them literally unrepresentable — and so is slower, but far more resilient.
+====
+
+This is a research proof-of-concept in the `ideas-to-alphas` incubator: a typed
+cellular automaton that synthesises three existing-but-never-combined ideas — CA
+models of political order, Game-of-Life/Plague-Inc. diffusion, and constitutional
+type-safety. See `MOTIVATION.adoc` for the near-miss survey and novelty claim.
+
+== Try it in 60 seconds
+
+[source,sh]
+----
+cd a-sounder-constitution
+
+# 1. The headless proof of the thesis (no browser needed):
+npm run sim          # node sim/compare.mjs
+
+# 2. The test suite (unit + thesis-level):
+npm test             # node --test
+
+# 3. The playable simulator (ES modules need an HTTP server):
+npm run serve        # python3 -m http.server 8080
+#   then open http://localhost:8080/web/
+----
+
+In the playable version: pick a doctrine on the right, click the grid to release
+it, press *Play*. Then flip the constitution between *Sound* and *Unsound* and
+watch the *type-checker log*. Releasing a **Caste** or **Surveillance** doctrine
+under a sound constitution fills the log with `✗ type error: … unrepresentable`
+and domination stays at 0%; under an unsound one the same doctrine reads
+`✓ permitted … (domination)` and the polity slides toward caste.
+
+== What you should see
+
+Hold a strategy fixed and vary only the constitution (this is `npm run sim`):
+
+[cols="1,1,3"]
+|===
+| Strategy | Constitution | Outcome
+
+| reach for coercion | unsound | *fast* order — but caste stability: domination ~80–90%, legitimacy/trust → 0, enormous hidden debt
+| reach for coercion | sound   | the coercive moves are *unrepresentable* (tens of thousands blocked); domination never happens; the shortcut to order is simply gone
+| build legitimacy   | either  | durable *rights-preserving resilience* — except in Reconstruction-unsound, where a pre-existing caste cannot be undone and the polity stalls
+|===
+
+The lesson the model makes you feel: unsound order is fast and brittle because
+its stability *is* domination; sound order is slower because the type system
+refuses the cheap coercive moves — and that refusal is exactly what survives a
+shock.
+
+== Layout
+
+[cols="1,3"]
+|===
+| Path | What
+
+| `src/constitution.js` | the type checker — legal transitions, sound vs. unsound (the central mechanic)
+| `src/engine.js`       | the civic automaton — cells, gliders, turn loop, outcomes
+| `src/scenarios.js`    | the doctrine (glider) catalogue and named scenarios
+| `src/rng.js`          | seeded PRNG (determinism)
+| `web/`                | the playable canvas simulator (`index.html`, `ui.js`, `styles.css`)
+| `sim/compare.mjs`     | headless sound-vs-unsound demonstration
+| `tests/`              | `node --test` suite (mechanics + thesis-level assertions)
+| `formal/Constitution.idr` | Idris2 proof that `Person -> Property` is unrepresentable under a sound constitution
+| `docs/`               | `TYPE-THEORY.adoc`, `DESIGN.adoc`, `GLIDERS.adoc`
+|===
+
+== The two type signatures, side by side
+
+[source,haskell]
+----
+-- Unsound: personhood is a tag; anyone can be re-tagged.
+data Human = FullPerson | PartialPerson | PropertyPerson | NonCitizenPerson
+reclassify : Human -> Human          -- a total function; domination is free
+----
+
+[source,idris]
+----
+-- Sound: Property is unrepresentable; coercion needs a proof obligation.
+data Person = Full | Partial | NonCitizen            -- no Property constructor
+soundNeverProperty : (p : Person) -> Not (embed p = PropertyPerson)
+----
+
+`formal/Constitution.idr` proves the sound side; `src/constitution.js` is its
+executable mirror, exercised by `tests/`.
+
+== Status
+
+Pre-alpha research artefact (2026-06-19). The JavaScript engine, tests, headless
+comparison, and web UI run today (Node 22 / any modern browser, zero
+dependencies). The Idris2 module is written to compile clean but has *not* been
+run through `idris2` in this environment — see `formal/README.adoc` for the
+verification status and graduation criteria.
+
+== License
+
+MPL-2.0. Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath).