FELRA GCPR–RWL–FELRA WORKBENCH

GCPR–RWL–FELRA · PYTHON-FIRST VERIFICATION WORKBENCH

FELRA

形式演化邏輯—規則架構 Formal Evolving Logic-Rule Architecture

v1.0.0 51 / 51 tests · pass

FELRA turns theory and data into reproducible computational evidence first, then promotes stable results into formal specifications and proof obligations. Every run leaves behind hashes, seeds, and environment versions — results can be re-verified by anyone, on any machine, not just trusted.

Theory / Data Python verification & statistical analysis Counterexamples, residuals, sensitivity & figures Revised claims FELRA specification SMT / Lean / RWL
$ pip install -e ".[dev]" View source on GitHub →

Core Capabilities

From hypothesis to evidence bundle

A declarative project.yaml describes the parameter space, claims, and analyses; FELRA produces a complete Evidence Bundle — CSV, JSON, Markdown, figures, and hashes, all traceable.

01 · SPEC

Declarative specification

YAML describes claims and analyses; safe AST numerical expression evaluation — no extra glue code needed.

02 · SEARCH

Counterexample search

Finite declared grids, boundary checks, and random sampling — systematic counterexample search, not a single-point check.

03 · DATA

Data contracts & quality

Typed CSV/JSON/JSONL/gzip datasets; missing, invalid, and duplicate rows are all recorded as evidence, with source hashes.

04 · STATS

Statistical inference

Descriptive statistics, hypothesis tests, bootstrap confidence intervals, power analysis, and robustness analysis (bootstrap/subsample).

05 · SENS

Sensitivity & Pareto

Local finite-difference sensitivity, residual diagnostics, one- to high-dimensional parameter sweeps, two-objective non-dominated fronts.

06 · MODEL

Cross-validation & effect sizes

Leakage-aware numeric regression cross-validation, shared-fold model comparison, standardized effect sizes, multiple-comparison correction.

07 · REGISTRY

Experiment registry

Append-only JSONL experiment registry — felra registry inspects run history by project or status.

08 · LOCK

Preregistration

Immutable scientific-plan locking, with warning and strict execution modes; the plan itself carries a stable SHA-256 fingerprint.

09 · REPLAY

Provenance & replay

JSON/DOT/SVG evidence-provenance graphs, a stable result_sha256, felra replay for independent re-verification, and felra export for a paper-ready Methods/Results/Limitations bundle.

10 · SYMBOLIC

Symbolic verification

Exact algebraic equivalence and derivative checks via SymPy, with per-variable assumptions (positive, real, integer, …) — a proof over the whole declared domain, complementing the sampling-based channels above.

11 · SOUNDNESS

Numerical soundness

Overflow/NaN detection, exact-derivative condition numbers, and float64-vs-arbitrary-precision catastrophic-cancellation detection — driven from the same symbolic parser as V2, applied to real sampled points.

12 · CROSS-METHOD

Cross-method consistency

Declare two or more independent formulations or evaluators (numeric/symbolic/high_precision) for the same quantity and check pairwise agreement — arbitrary precision alone can't rescue a formula's own singularity; a different method can.

LIVE REPRODUCIBILITY CHECK · Evidence Ledger

Not a marketing number — evidence re-run on this machine today

The record below is from the examples/reproducibility example project, run end to end with FELRA v0.7.0 on 2026-07-20: executed, independently replayed, and exported as a paper bundle.

project: reproducibility-demo · FELRA v0.7 Preregistration and Replay Demo
PREREGISTRATION · MATCHED REPLAY · MATCH
Claim
For 1,001 sampled points, x² is non-negative (x ** 2 >= 0) — no counterexample was found within the declared sampling budget. This is computational evidence, not a mathematical proof.
Result SHA-256
ec641760 a43ff42f cc30d311 b5587ec0
9e4817f6 af425cb0 77a9e3c7 0f12608b
Independent replay
felra replay artifacts/reproducibility — the recomputed result hash matches byte-for-byte.
Paper export
felra export produced 18 indexed files: Methods, Results, Limitations, CITATION, figures, report, and file hashes.
square_curve.png — the figure FELRA produced from this run, plotting x against x squared
figures/square_curve.png — the actual figure produced by this run, unmodified
A matching replay proves computational reproduction on this machine — not external replication, scientific validity, or a universal mathematical proof.

Quick Start

Five commands, from install to your first evidence bundle

01 · Install

$ python -m venv .venv
$ .venv\Scripts\activate   # Windows
$ source .venv/bin/activate  # Linux / macOS
$ pip install -e ".[dev]"

02 · Create and run your first project

$ felra init my-theory
$ felra run my-theory/project.yaml \
    --output my-theory/artifacts/run

03 · Run the built-in examples

$ felra run examples/data/project.yaml \
    --output artifacts/data
$ felra batch examples/repeated_batch/batch.yaml \
    --output artifacts/repeated --workers 2

04 · Preregister, replay & export (v0.7)

$ felra verify-preregistration project.yaml \
    --record preregistration.json
$ felra replay artifacts/run --output artifacts/replay
$ felra export artifacts/run --output artifacts/paper

SCIENTIFIC BOUNDARIES

FELRA won't inflate your conclusions for you

This is an academic verification workbench, not a proof generator. The boundaries below are written into AGENTS.md, and the same rules bind anyone — human or agent — working on this project.

FELRA's Python results are computational evidence under finite data, finite precision, a finite budget, and specific statistical assumptions — not a general mathematical proof.

A p-value is not "the probability the hypothesis is true"; rejecting the null does not automatically establish causation.

Failing to reject the null does not mean the two are equivalent — "no counterexample found" is never rewritten as "theorem proved."

Demonstration datasets must stay labeled synthetic — they are not empirical evidence.

A matching replay proves computational reproduction in the same environment — not external replication, scientific validity, or universal proof.

Version Arc

From MVP to full verification-channel coverage in one week

v0.1–v0.7 had their first implementation on 2026-07-14 (v0.5–v0.7 were synced into the main branch and fully re-validated on this machine on 2026-07-20); v0.8.0 through v1.0.0 were each implemented and validated directly, also on 2026-07-20 — the three defined steps that complete the whitepaper's stage-2 verification-channel roadmap (V0-V8).

v1.0.0 Cross-Method Consistency (V8) · Stage 2 Complete

Independent-method agreement checks (numeric/symbolic/high-precision backends) complete the full V0-V8 verification-channel set. 6 new regression tests — 51/51 total.

v0.9.0 Numerical Soundness (V3)

Overflow/NaN detection, exact-derivative condition numbers, and float64-vs-arbitrary-precision catastrophic-cancellation detection. 5 new regression tests.

v0.8.0 Symbolic Verification (V2)

Exact algebraic-equivalence and derivative checks via SymPy, with per-variable assumptions — complements the sampling-based channels with a proof over the whole declared domain. 7 new regression tests.

v0.7.0 Preregistration, Provenance, Replay & Paper Export

Immutable scientific-plan preregistration, JSON/DOT/SVG evidence-provenance graphs, a stable result_sha256, felra replay and felra export. 33 regression tests.

v0.6.0 Effect Sizes, Cross-Validation & Registry

Bonferroni/Holm/Benjamini–Hochberg multiple-comparison correction, standardized effect sizes, leakage-aware cross-validation, an append-only experiment registry.

v0.5.0 Power, Robustness & Cache

JSON/JSONL/gzip datasets, noncentral-t and Fisher-z power analysis, bootstrap/subsample robustness analysis, content-addressed caching.

v0.4.0 Data, Statistics & Replication Pipeline

Typed external CSV datasets, dataset-row claims, grouped descriptive statistics, the hypothesis-test family, percentile bootstrap confidence intervals, repeated experiments, and parallel batching.

v0.3.0 Sensitivity, Residual & Pareto

Local sensitivity, residual analysis, parameter sweeps, exact two-objective Pareto fronts, felra batch.

v0.2.0 Executable Project Specs

Executable project.yaml, safe AST expression evaluation, felra run and project-level Evidence Bundles, multiple figure types.

v0.1.0 Initial MVP

The first version of the Python-first research workbench.