Formal mathematics, verification, and executable research tools for strategic regime dynamics.
PermanssonLean develops and checks the mathematical foundations of Generated Regimes (GR) and Permansson Regimes (PR): descriptions of persistent processes generated by strategic behavior, together with intervention-relative tests for whether a strategic-generator component is constitutive of a declared regime property.
The research starts from a typed strategic-world process: action selection and strategic updating form the generator G = (α, U), a separate world-transition kernel is P, and their ordered composition induces a joint-state Markov kernel. The framework classifies that induced process; it is not a new equilibrium solution concept, an automatic regime-discovery service, or an empirical causal-identification system.
The repository now contains two deliberately separate Lean libraries, an accepted research companion, a draft application-reporting standard, and bounded executable proof-replay interfaces. A Lean-checked constructed model does not, by itself, certify a real-world regime.
Verified source checkpoint — 19 October 2026. At
main@3931e4dccafb, the Research Lean workflow passed its pinned compiler and axiom checks, 1,093 research test methods, and direct-import coverage for 646 research Lean modules. The separately configured Original Lean, Application contract, Executable verification, Research integrity and Integrity portability workflows also passed at that exact commit. These are date- and source-bound software-verification counts, not counts of theorems or independent scholarly reviews.
| Goal | Read this | Required tools |
|---|---|---|
| Understand the theory | Paper guide and glossary | None |
| Read the accepted research companion | v0.2.0 research companion | None for its PDF |
| Study or extend the Lean mathematics | Research build guide, implementation index | Pinned Lean 4.34.0 and Git |
| Validate an application report | Application Standard and getting started | Python 3.13 |
| Replay supported finite proofs | C10 six-state or C11 stationary-family | Python 3.13, clean Git checkout, pinned Lean |
| Reproduce validation and integrity checks | Verification guide | Depends on the check |
| Contribute | Contribution guide | Depends on the change |
The documentation index links the complete reference material.
The frozen source manuscript is Permansson Regimes: A General Framework for Strategic Dynamics Beyond Equilibrium v0.1.8. The Lean package version remains 0.1.0 because this metadata belongs to the immutable original formalization snapshot; it is not the paper or research-library release version.
| Component | Role and scope |
|---|---|
PermanssonLean/ |
Frozen v0.1.8 discrete formal core, 64 Lean source modules at the checkpoint. Default Lake target. Its completed formalization claim reaches Proposition 8.1 within the original theorem ledger; it does not cover every manuscript claim. |
PermanssonResearch/ |
Separate, evolving research Lean library, 646 source modules at the checkpoint, directly imported from PermanssonResearch.lean. Its results retain each theorem's actual finite, measurable, moment, information and intervention hypotheses. |
release/v0.2.0/ |
Accepted v0.2.0 research companion with its own theorem map and acceptance evidence. It is based on an earlier accepted research source, not the full post-PR79 October 18–19 additions. |
application/ |
Draft v0.1.0 reporting and validation standard, compatible with paper v0.1.8; structural contract checking, not mathematical or empirical certification. |
apps/permansson/ |
Separately versioned, supported C10 and C11 numerical/Lean proof-replay interfaces. Each proves only the reified finite mathematical object in its documented supported input class. |
verification/ |
Original Lean checks, research checks, numerical regression, preservation/integrity, application-contract gates, and historical release replays, each with distinct evidentiary meaning. |
Versions are not interchangeable. The paper is v0.1.8, the original Lake package metadata remains 0.1.0, the Application Standard is draft v0.1.0, the accepted research companion is v0.2.0, the C10 successor CLI is v0.1.0, and the C11 successor CLI is v0.2.0. These identifiers refer to different deliverables and are not a single synchronized release number.
From the repository root, using the checked-in lean-toolchain and lake-manifest.json:
lake exe cache get
lake build
lake build PermanssonResearchlake build checks the default frozen core. lake build PermanssonResearch checks the separate research root; one is not a substitute for the other. The original Lean workflow and Research Lean workflow independently test their respective scopes and audit permitted axioms. Routine builds must not run lake update or change the dependency pins.
For setup and current source-bound CI expectations, see the research build guide and verification guide.
These interfaces accept strictly checked external finite rational JSON inputs. Their successful outputs distinguish exact numerical calculation, genuine Lean kernel replay and scientific/empirical identification, which the CLI does not establish. Replay mode requires a clean Git checkout, the pinned Lean environment, and a fresh output directory outside the repository.
This interface admits only the exact supported six-state D0/C10 model, its predefined legal interventions and the full original two-start comparison domain. A well-formed but different stochastic model is unsupported, not an automatically certified new instance.
python apps/permansson/closure-successor/cli.py \
apps/permansson/closure-successor/examples/frozen_six_state.json \
--mode replay --output /tmp/permannsson-c10-replaySee the C10 CLI reference for the numeric-only mode, source-binding checks and negative input examples. The C10 VERSION.json still carries the marker DRAFT__COMPILER_CI_PENDING; the documentation update does not change or independently recertify that application-status metadata, despite compiler-backed PR/main CI evidence.
This interface supports 1–6-state exact rational Markov matrices with Boolean state descriptors, including periodic and multiple bottom-class examples. It proves exact stationary-family facts for the reified matrix; it does not prove a strategic generator, legal intervention, Exact GR/PR status or real-world identification.
python apps/permansson/closure-successor-c11/cli.py \
apps/permansson/closure-successor-c11/examples/multiclass_three_state.json \
--mode replay --output /tmp/permannsson-c11-replaySee the C11 CLI reference for supported schema, scope limits and failure behavior. The /tmp/ paths in these examples are Unix-style; on Windows, provide a new empty directory outside the Git checkout.
The Application Standard is draft v0.1.0, compatible with theory v0.1.8. Its offline validator checks declared structure, provenance fields, typed interventions and reporting consistency, without claiming to verify the underlying scientific statements.
python -m pip install -r application/requirements.txt
python application/validator/validate_application.py \
application/examples/grounded_pr_minimal/application.json --jsonThe synthetic example should report contract_valid=true and scientific_claims_verified=false. Contract validity is not Lean certification or empirical identification. Digest generation (--digest) is not contract validation: a successful digest bootstrap may still match stale identifiers. For worked examples and exact error meanings, see Getting started and Application boundary.
The accepted v0.2.0 companion and subsequent Research library contain scoped work on recurrent classes and occupation laws, killed-process persistence and first-exit routing, constitutive margins and intervention grammars, total-variation and metric perturbation bounds, multi-agent protocols, finite monitor/robust/hidden-state optimization and exact economic/game witnesses. The v0.2.0 implementation index is a dated pre-PR79 anchor map; the PR79 source/CI index documents the October 18 closure checkpoint. Neither automatically certifies PRs #80–102, whose exact scopes and acceptance evidence remain in their own merged PRs and CI runs.
Some boundaries are deliberately negative or conditional:
- In X1, all six scoped original finite constitutive margins have exact proofs, but the declared replete region leaks; this does not establish an Exact GR for that region.
- The separate economic model is a constructed mathematical positive witness, not a certificate for any external historical case.
- Some broader measurable two-player, projected-output and solver transfers still need additional typed adapters or hypotheses. In particular, PR #102 is a first stage of the general measurable two-player recovery, not its complete full-path-law extension.
- Finite numerical replay and a positive constitutive margin do not by themselves establish exact invariance, independent causal identification, authentic preregistration or a real-world Permansson regime.
The research build guide distinguishes current verified results from historical PR snapshots; the closure acceptance ledger is a dated evidence record, not an automatically updated universal completion certificate.
Read the editorial-clean v0.1.8 manuscript, with TeX and supporting papers. The paper's immutable mathematical snapshot is c018f79ea4ce46f4f679ad5bca254509778fc53c, separately documented by the paper verification manifest, release metadata and provenance guide. Later Research PRs do not retroactively alter this snapshot or the accepted v0.2.0 companion's source identity.
Use CITATION.cff for the scholarly companion. When citing later research or executable software behavior, include the exact Git commit and the relevant compiler/verification evidence. The repository's acceptance and CI records are not equivalent to external peer review or a validated empirical forecast.