systemic-tau-formal

Machine-verifiable, open formalization of Systemic Tau (τₛ) + RECD

Author: Johel Padilla-Villanueva · License: MIT · Version: 0.1.12
GitHub: https://github.com/johelpadilla/systemic-tau-formal
DOI (this version): https://doi.org/10.5281/zenodo.21684040
Concept DOI (all versions): https://doi.org/10.5281/zenodo.21516059

This monorepo elevates the existing Zenodo / PyPI corpus to a standard where:

1. Mathematics is stated for Lean 4 checking (lake build)
2. Algorithms have a minimal Python reference + tests
3. Empirical claims are listed as public falsifiable predictions
4. Philosophy is separated by mandatory epistemic labels

Layer	Path
Formal core	lean/
Reference Python	python/
Try-it scripts	notebooks/
Access map	docs/ACCESS_LAYERS.md
Falsifiable list	docs/FALSIFIABLE_PREDICTIONS.md
Protocol	docs/EXPERIMENTAL_PROTOCOL.md
Challenges	docs/CHALLENGES.md
Workshop 2026	docs/WORKSHOP_STRESS_TEST_2026.md
Issue board	docs/ISSUE_BOARD.md
τ_ch vs δ	docs/TAU_CH_DELTA.md
C3 cross-domain	docs/CROSS_DOMAIN.md
Mathlib	docs/MATHLIB.md
Formal obligations map	docs/FORMAL_OBLIGATIONS.md
Build status	STATUS.md

Related production code: PyPI systemictau · DOI 10.5281/zenodo.20576241

---

Epistemic labels (read first)

See docs/EPISTEMIC_LABELS.md:

[TEOREMA] · [CONJETURA] · [INTERPRETACIÓN FÍSICA] · [AFIRMACIÓN ONTOLÓGICA] · [OPERACIONAL] · [EMPÍRICO]

Do not collapse levels. Dengue data do not prove Lean theorems; δ is not Polo’s efficient cause.

---

Verify step by step

1. Python (works without Lean)

cd python
python -m venv .venv && source .venv/bin/activate
pip install -e ".[dev]"
pytest -q

2. Notebooks / demos

Jupyter (from repo root, after pip install -e ".[dev]" in python/):

Notebook	What it does
notebooks/01_synthetic_chaos.ipynb	Logistic maps → τₛ, g, T_RECD + plots
notebooks/02_aedes_puerto_rico.ipynb	Aedes raw-first (data/aedes/raw/ → proxy fallback)
notebooks/03_falsifiability_test.ipynb	Load your CSV under protocol defaults
notebooks/04_p3_noise_robustness.py	P3 noise scan ρ ≤ 20%
notebooks/05_first_return_poincare.py	First-return Poincaré twin (--plot)
notebooks/06_cross_domain_c3.py	C3 synthetic finance / EEG / grid kits
notebooks/07_aedes_field_report.py	Empirical τₛ/RECD on data/aedes/raw/ (no fake P1)
notebooks/08_aedes_p3_field.py	P3 noise scan on field Aedes (ρ≤20%)
notebooks/09_aedes_p4_field.py	P4 structure vs baselines (no false anti discharge)
notebooks/10_aedes_empirical_board.py	Unified P1/P3/P4 empirical board
notebooks/12_chbmit_p1_eeg.py	P1-EEG v1.0.0 CHB-MIT clinical onset (parse/lock/score/C1) — track paused
notebooks/13_chbmit_p1_eeg_v11.py	P1-EEG v1.1.0 precondition/lock/score/C1 (order + bandpower) — track paused
notebooks/14_aedes_p1_external.py	P1-Aedes v1.0.0 external (t_{\mathrm{obs}}) propose/lock/score
notebooks/15_ili_p1_external.py	P1-ILI v1.0.0 HHS %wILI → FluSurv external (t_{\mathrm{obs}})
notebooks/16_p1_synthetic_canonical.py	P1-Synthetic plant/nulls + G1–G4 + C1 companion
docs/P1_FAIL_TRIPTYCH.md	P1 synthesis: instrument PASS · field residual · C1 ambient FAIL
docs/P1_AEDES_EXTERNAL_TOBS.md	P1-Aedes multi-trap + external clinical protocol
docs/P1_EEG_CHB01_PILOT_REPORT_v1.1.md	P1-EEG v1.1.0 chb01 pilot (hit 0/7; gates PASS; paused)
papers/p1-instrument-note/	Short-note outline for the P1 instrument package

CLI twins (no Jupyter required):

python notebooks/01_synthetic_chaos.py
python notebooks/02_aedes_puerto_rico.py
python notebooks/03_falsifiability_test.py data/synthetic/regime_switch.csv
python notebooks/04_p3_noise_robustness.py
python notebooks/05_first_return_poincare.py --plot
python notebooks/06_cross_domain_c3.py
python notebooks/07_aedes_field_report.py
python notebooks/08_aedes_p3_field.py
python notebooks/09_aedes_p4_field.py
python notebooks/10_aedes_empirical_board.py

Committed lab fixtures: data/synthetic/, data/aedes/proxy/.

See notebooks/README.md.

3. Lean 4 (optional until toolchain installed)

# once: https://leanprover-community.github.io/get_started.html
# curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh
cd lean
lake build

Requires elan. After install:

export PATH="$HOME/.elan/bin:$PATH"
cd lean && lake build   # currently PASS on Lean 4.14.0

FeigenbaumReduction.lean / FeigenbaumAnalytic.lean / FeigenbaumTendsto.lean still contain honest sorrys (see STATUS.md).
Mathlib (v4.14.0) is required for ℚ order/tactics: docs/MATHLIB.md.

---

What is formalized (target checklist)

Item	Status
Definition of τₛ (mean Kendall-τ, windows)	Interface + Python ✓ · Lean ✓
Thresholds 0.50 / 0.41 from δ	Operational ✓ · band lemmas ✓ · unique f(δ) open
Gate (g(\tau_s)) and (\Delta t_k)	Python ✓ · Lean gate + δ^{-k} ✓
Feigenbaum reduction theorem	Preprint exists · 1a/2a/ε–N↔Tendsto ✓ · goals 1b–3 sorry · map
4-level ontology / Baron’s Trilemma	Spec in Lean + docs/ONTOLOGY_BRIDGE.md
lake build	PASS (Lean 4.14.0)

---

Falsifiable predictions (summary)

1. P1 Sustained (|\tau_s|<0.41) ⇒ ascent signal (t^*) 4–6 weeks before observable transition [EMPÍRICO]
2. P2 Fractal dim. of extramental clock ≈ 1.98 on low-D chaos [CONJETURA]
3. P3 Bands robust to ≤20% Gaussian noise without re-training [EMPÍRICO]
4. P4 Anti-sync ((\tau_s\le-0.41)) yields distinct RECD interval structure [CONJETURA]

Full text: docs/FALSIFIABLE_PREDICTIONS.md

---

Workshop (proposed)

Systemic Tau Stress-Test 2026 — open 48h destruction workshop (dynamics + formal + philosophy).
Full brief: docs/WORKSHOP_STRESS_TEST_2026.md · board: docs/ISSUE_BOARD.md.
Track issues with labels contradiction, improvement, new-domain, philosophy-challenge, workshop.

---

Citation

See CITATION.cff.

What	Identifier
This formal monorepo (v0.1.11)	10.5281/zenodo.21581189
Prior software v0.1.10	10.5281/zenodo.21537465
Prior software v0.1.8	10.5281/zenodo.21522882
Concept DOI (always latest)	10.5281/zenodo.21516059
v0.1.7 (archived)	10.5281/zenodo.21522346
v0.1.6 (archived)	10.5281/zenodo.21516523
v0.1.5 (archived)	10.5281/zenodo.21516329
v0.1.4 (archived)	10.5281/zenodo.21516060
GitHub	https://github.com/johelpadilla/systemic-tau-formal · release v0.1.9
Prior Systemic Tau corpus / software archive	10.5281/zenodo.20576241

@software{padilla_systemic_tau_formal_2026,
  author       = {Padilla-Villanueva, Johel},
  title        = {systemic-tau-formal: Machine-verifiable Systemic Tau
                   (τₛ) and RECD},
  month        = jul,
  year         = 2026,
  publisher    = {Zenodo},
  version      = {0.1.11},
  doi          = {10.5281/zenodo.21581189},
  url          = {https://doi.org/10.5281/zenodo.21581189}
}

---

Repo layout

systemic-tau-formal/
├── lean/                 # Lean 4 library SystemicTau
├── python/               # minimal reference core + tests
├── notebooks/            # 01–06: synthetic, proxy, P3, first-return, C3
├── papers/               # index to Zenodo / local catalog
├── data/                 # synthetic + aedes proxy (+ raw intake path)
├── docs/                 # layers, protocol, challenges, workshop, C3
├── STATUS.md
├── CITATION.cff
└── README.md

What this release is not

• Not a claim that all preprints are machine-checked
• Not a substitute for clinical/public-health decision systems without domain validation
• Not a finished derivation of 0.41 from δ (that is an explicit open formal goal)
• Not licensed field C3 results (synthetic kits only)

---

*v0.1.9 · 2026-07-24 · Unique inverse-scale f(δ) bridge + extended candidates; zero sorry/axiom.