PermanssonLean

Formal verification and executable-validation companion for Permansson Regimes: A General Framework for Strategic Dynamics Beyond Equilibrium v0.1.8.

Permansson separates two questions: what persistent regime a strategic process generates, and whether a declared strategic component is constitutive of a regime property under a specified intervention. This repository collects the paper, Lean proofs, executable tests, and an application-reporting standard. It is not an automatic regime-discovery, prediction, or causal-estimation service.

Start here

Your goal	First stop	Software needed
Understand the theory	Paper and reading order	None to read the PDF
Try the application format	Setup and first example	Git and Python 3.13
Check the mathematical claims	Formalization map and Lean setup	Lean/elan and Git
Reproduce verification	Verification guide	Depends on the selected check
Make a change	Contribution guide	Depends on the change

New to the terminology? See the glossary. The documentation index links the detailed references and archives.

Using Permansson in applications

The Application Standard is draft 0.1.0, compatible with theory v0.1.8. It serializes the nine independent certificate dimensions, frozen semantic choices, typed interventions, provenance, and identified sets. You do not need Lean or LaTeX to use its Python validator.

After setting up Python and entering the repository root:

python -m pip install -r application/requirements.txt
python application/validator/validate_application.py application/examples/grounded_pr_minimal/application.json --json

Expect exit 0, contract_valid=true, and scientific_claims_verified=false. This synthetic example demonstrates a well-formed record, not empirical evidence. CONTRACT PASS checks structural consistency, not proof, causal identification, statistical coverage, or authentic preregistration. In particular, a well-formed record can truthfully describe an invalid or unresolved application.

Continue with the worked examples, CLI reference, or application/formalization boundary. Digest generation is not validation: --digest can exit 0 for matching stale IDs. Use ordinary validation, without --digest, as the contract gate.

Paper and supporting theory

Read the editorial-clean v0.1.8 PDF. The paper guide links its TeX source, the foundational EGR paper, and the specialized Appendix E papers. Those supporting copies do not change the frozen release hashes or the formalization snapshot.

Build

Install Lean through elan using the Lean setup guide, then run from the repository root:

lake exe cache get
lake build

Use the checked-in dependency manifest; a routine build does not require lake update. The Lean workflow additionally runs an axiom audit and rejects placeholders and source-level custom axioms.

Current coverage

The completion claim covers the v0.1.8 discrete formal core through Proposition 8.1, not every statement in the paper. The full theorem/definition ledger records the checked declarations and their boundaries.

Formalization strategy

The dependency map follows typed kernels, path laws, regime/persistence semantics, constitution, representation and quotient preservation, Paper-I recovery, and the periodic example. Its later milestone sections retain the historical build sequence, not a list of remaining tasks.

Status discipline

Status definitions distinguish PROVED, DEFINED, SCAFFOLDED, OPEN, NON-CORE, and EMPIRICAL material. A green Lean build checks the encoded declarations; it does not certify empirical premises or literature priority. Appendix E and the future theory roadmap remain outside the completed discrete core.

Executable verification

The verification guide separates Lean proof checking, Runs 17–30, repository/release integrity, and application-contract validation. It gives commands, expected outcomes, and the distinction between a normal clone and the historical release packages. Their PASS results are not interchangeable.

Toolchain

Component	Version authority
Theory and scholarly companion	v0.1.8 — CITATION.cff
Lean / mathlib	4.34.0 / v4.34.0 — lean-toolchain, lakefile.toml
Application format	Draft 0.1.0 — application/VERSION.json
Python verification	CPython 3.13; separate application and destructive-suite dependencies

The Lean package version remains 0.1.0 because its package metadata belongs to the immutable formalization snapshot. It is not the paper's release version or the independently versioned application standard.

Paper release provenance

The manuscript identifies mathematical snapshot c018f79ea4ce46f4f679ad5bca254509778fc53c and its recorded green CI run. For exact artifact hashes and filename mappings, use the paper verification manifest, machine-readable release metadata, and provenance guide.

Use CITATION.cff for the scholarly companion and record the exact commit when referring to a later repository or application implementation.