GCPR–RWL–FELRA · PYTHON-FIRST VERIFICATION WORKBENCH
FELRA
形式演化邏輯—規則架構 Formal Evolving Logic-Rule Architecture
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, so a result can be re-verified rather than just trusted. Since v1.9, it also keeps track of what an argument has actually established: the status of every claim is derived from re-checkable certificates, never written down by its author. Since v1.15, when a proof and a counterexample contradict each other, it names which source is wrong — and checks that answer.
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.
13 · FORMAL
External formal checkers
Lean, TLC and z3 through a closed set of adapters. Each verdict records the SHA-256 of the binary that ran and of the obligation it read, and is reported beside the Python evidence — never merged into it. Lean axiom audits check a whole development against a declared axiom set.
14 · EXACT
Exact & arbitrary precision
Decimal, Rational and mpmath backends, quoted literals read exactly ("0.1" is 1/10, not a float64), precision ladders that report stable, unstable or exhausted, and cross-backend agreement checks.
15 · CERTIFY
Re-checkable certificates
Interval enclosures with exact rational endpoints, exact identities, inequalities and external formal verdicts — each hashed into the manifest and re-checked from its own recorded data, not by re-running the analysis that issued it.
16 · OBLIGATION
Proof-obligation export
A claim rendered as SMT-LIB2 with its negation asserted, checked beside a discriminating twin — so a translation that collapses to an empty domain is reported as undecided, never as proved.
v1.9 – v1.15 · Proof-Process Verification
A status is derived, never declared
A project can declare claims, the evidence offered for them and the arguments linking them. FELRA runs a named certifier on each piece of evidence, and a small kernel derives every status from the resulting receipts: VERIFIED, REFUTED, BLOCKED, OPEN or TRUST_CONFLICT. A status written into the project file is refused at load time. Every argument is an application of a method the kernel can check, what remains is tracked as a graph of open obligations, a formalization is held to the question that was asked, and a contradiction is traced to its source.
CERTIFIERS
Ten, each with stated limits
Polynomial normal form, an independent SymPy check, exact counterexamples and witnesses, z3 with a discriminating twin, exhaustive search of a box z3 proves covers the domain, witness functions for nested quantifiers, and Lean 4. Every model z3 returns is re-checked in exact arithmetic before it is believed.
METHODS · v1.12
Five obligations per argument
Seven methods. Each application must discharge O_pre, O_dir, O_bridge, O_cover and O_trust — by rule, by z3 on a formula the library builds from the claims, or by the kernel. Any other method is recorded and never accepted; an assumed obligation caps the result at CONDITIONAL.
GAP GRAPH · v1.13
What remains, by class
Every run expands into an AND/OR graph of open obligations, each with its GAP class G0–G10. A declared research gap is discharged only through the formal claim it is bound to; expanding it into sub-gaps is a plan and discharges nothing.
REASSESS · v1.13
A shortcut that checks itself
felra ppv-reassess recomputes only what a change touches, then checks that the result equals a full recomputation and that every status that moved lies inside the affected set. Editing a claim in place under the same revision is reported as a violation.
ALIGNMENT · v1.14
A proof of the right question?
No machine certifies that a sentence means a formula. FELRA holds the formalization to its reader's declared quantifier, sorts and domain (compared by z3), to points the sentence settles (evaluated exactly), and to independent formalizations (pointwise, by z3). Cue words are hints only.
GOAL GATE
Local is not global
RUN_FINISHED, LOCAL_VERIFIED and ORIGINAL_GOAL_VERIFIED are reported separately, with how each cited claim's scope differs from the goal's. A verified formal goal that is not aligned with the sentence stays GOAL_BRIDGE_OPEN.
TRUST_CONFLICT · v1.15
Who is wrong — checked
A claim both proved and refuted is isolated: nothing may rest on it. From the exact counterexample, FELRA names the source it contradicts — a foundation axiom, a certificate of a different statement, a faulty certifier or solver — then withdraws it and re-evaluates. Only a diagnosis that resolves the conflict is CONFIRMED.
PPV-VERIFY
Re-checked from the artifacts
felra ppv-verify re-runs the exact certifiers, rebuilds every SMT obligation and Lean file and compares them byte for byte, re-checks solver models without the solver, and re-derives every status and every diagnosis. It says how many verdicts rest on a prover it did not re-run.
965353da a2b4371b b8120097 e89a5d98
felra ppv-verify — 40 of 40 checks pass: both diagnoses re-derived from the receipts, the Lean file FELRA wrote rebuilt from the claim, the cited one matched to the copy Lean read. 2 verdicts rest on a z3 unsat and 2 on Lean having checked a proof — matched to their files, not re-derived. With --rerun-smt, which hands them back to z3 and Lean, 47 of 47 pass.What the kernel derived, and why
- CONFLICTNo fifth power is a sum of four ordered fifth powers — follows from the axiom by a z3-certified implication, and is refuted by 27⁵ + 84⁵ + 110⁵ + 133⁵ = 144⁵. The diagnosis walks back through the implication, finds the axiom false at that point, and names it:
FOUNDATION_INCONSISTENT. Withdrawn, the claim is REFUTED — confirmed. - BLOCKEDThe claim resting on it is isolated — never VERIFIED through a conflicted premise.
- CONFLICTa − b ≤ a for all integers — "proved" by Lean's
Nat.sub_le, refuted by a = 0, b = −1.SPEC_MISMATCH: the theorem ranges over ℕ, not ℤ, and b = −1 is no natural number. Confirmed. - NO VERDICTA Lean proof of the same claim with the statement written by FELRA fails, as it must: a bound statement cannot drift from the claim.
- VERIFIEDa − b + b = a, by a bound Lean proof and by the polynomial normal form.
f20f017e 82621afb 56343524 d603f0c2
felra ppv-verify — 63 of 63 checks pass, including 10 SMT obligations rebuilt from their claims and one z3 counter-model re-checked without z3. Four verdicts rest on a z3 unsat, which it can match to its obligation but not re-derive.Statuses the kernel derived
- VERIFIEDThe constant gap between the four integer "walls", by normal form and by z3; the factorisation of the double-square gate, by normal form and SymPy; two Cayley-parametrisation identities, by z3.
- REFUTED"A prime p ≡ 3 (mod 4) divides at most one wall" — exact witness (u₁, v₁, u₂, v₂, p) = (3, 5, 2, 7, 3), which also refutes its pair-product variant. A second "witness" on the domain boundary is rejected.
- REFUTEDSquaring the Cayley point and calling it the same point — by t = 1/2, and by z3's own counter-model t = −1, re-checked exactly.
- BLOCKEDThe search-pruning rule that relied on the refuted lemma — blocked, not refuted, and without touching the identities.
- OPENThe perfect cuboid itself. A bounded z3 search gives no verdict; one support uses an unchecked method, another fails the implication contract.
LIVE REPRODUCIBILITY CHECK · Evidence Ledger
Not a marketing number — evidence re-run on a real machine
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.
x ** 2 >= 0) — no counterexample was found within the declared sampling budget. This is computational evidence, not a mathematical proof.9e4817f6 af425cb0 77a9e3c7 0f12608b
felra replay artifacts/reproducibility — the recomputed result hash matches byte-for-byte.felra export produced 18 indexed files: Methods, Results, Limitations, CITATION, figures, report, and file hashes.
Quick Start
From install to your first evidence bundle
The source repository is private at present, so these steps are for collaborators who have access to it.
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
05 · Proof-process verification (v1.9+, needs z3)
$ felra run examples/ppv_c3/project.yaml \ --output artifacts/ppv_c3 $ felra ppv-verify artifacts/ppv_c3
06 · Trust conflicts & Lean (v1.15+, needs z3 and Lean 4)
$ felra run examples/ppv_conflict/project.yaml \ --output artifacts/ppv_conflict $ felra ppv-verify artifacts/ppv_conflict --rerun-smt
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.
A run that meets its declared expectations has not thereby proved its original goal. Verified local claims never promote the goal; the report states the two separately.
A hash chain shows that records were not altered after they were written — not that what they say is true. A z3 unsat is the solver's verdict on the obligation as written; FELRA records which binary and which obligation, and does not re-derive it.
A verified formal claim is not thereby the question that was asked. When a sentence is bound to the goal, the goal counts as verified only if the formalization is also aligned with it — and alignment is checked against commitments its reader made explicit, not certified as meaning.
A Lean theorem FELRA did not write is not bound to the claim it is cited for: Lean checked some statement. The receipt records which, and says it is unbound.
Version Arc
From MVP to proof-process verification
v0.1–v1.0 (July 2026) built the evidence channels V0–V8 of the whitepaper's stage-2 roadmap. v1.1–v1.8 (August) added external formal checkers, exact and arbitrary-precision numerics, re-checkable certificates and proof-obligation export. v1.9–v1.11 (October) add the proof-process layer; v1.12–v1.15 make every argument an application of a checked method, track what remains as a graph of open obligations, hold a formalization to the question asked, and diagnose contradictions. Each step ships a drill that plants defects in the code and requires each to be caught by the test named for it — 22, 17, 10, 9 and 18 defects, all caught.
v1.15.0 – v1.15.2 2026-10-19 · Trust conflicts, diagnosed
When a proof and a counterexample contradict each other, the kernel isolates the claim, names the source the exact point contradicts and confirms it by withdrawing it. Lean 4 certificates: statements FELRA writes (bound) and theorems it cites (unbound). In 1.15.1, felra replay reads the run's own copy of a cited Lean file. In 1.15.2, two formalizations are compared only on the same domain — two true claims about different domains no longer count as agreeing. 345 tests.
v1.14.0 2026-10-19 · Natural language to formal claim
Alignment records hold a formalization to its reader's declared reading and to points the sentence settles. A formalization of the perfect-cuboid question that forgets "positive" is genuinely proved by the degenerate box (0, 3, 4) — and refused as an answer to the question.
v1.13.0 2026-10-19 · GAP graph & REASSESS
Open obligations as an AND/OR graph with classes G0–G10; declared research gaps discharged only through a bound claim; incremental recomputation that checks itself against a full one.
v1.12.0 2026-10-19 · Five obligations, mechanized
Seven methods, each application judged by O_pre, O_dir, O_bridge, O_cover and O_trust. Nested quantifiers, axioms and assumptions, trust policies with pinned solver binaries, exhaustive search. The method-applicability cases T1–T10 run on real mathematics.
v1.11.0 2026-10-19 · The goal gate explains itself
For every verified claim cited toward the original goal, the report names how its scope differs — quantifier, variables, sorts, domain, foundation. PPV documentation. 255 tests.
v1.10.0 2026-10-19 · PPV conformance
The perfect-cuboid reference project with 17 declared expectations; gates C01–C12 and tamper tests, including a ledger rebuilt wholesale and a forged receipt with a valid digest; a 22-defect drill, 22/22.
v1.9.0 2026-10-19 · Proof-process verification
Claim revisions, evidence receipts, a kernel that derives every status, implication bridges built by the kernel and certified by z3, a hash-chained ledger, and felra ppv-verify.
v1.8.0 2026-08-21 · Proof-obligation export
Claims rendered as SMT-LIB2 with the negation asserted, checked beside a discriminating twin so an empty domain can never pass as a proof.
v1.2.0 – v1.7.0 2026-08-18 · Numeric representation & certificates
A declared numeric policy; exact Decimal/Rational and mpmath backends; precision ladders; interval and numeric certificates re-checked from their own data; external multi-precision data ingestion.
v1.1.0 2026-08-18 · External formal backends
Lean, TLC and z3 invoked through a closed set of adapters, with each checker identified by the hash of its binary; Lean axiom audits followed in v1.3.1.
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.