OPN0001activev1TauLib v3 Full Axiom Audit
Open problem: complete the axiom-free formalization audit across the full TauLib v3 module set. Currently 1 project-local axiom (AXM0001 bridge functor exists) remains in the bridge layer; the rest must round-trip through #print axioms producing no project-local entries.
Payload
Open Problem (TauLib v3 Full Axiom Audit). Complete the axiom-free formalization audit across all TauLib v3 modules.
Current status:
- τ-Kernel modules (MOD0001-MOD0050): axiom-free ✓
- Calibration modules (MOD0051-MOD0080): axiom-free ✓
- Bridge modules: 1 project-local axiom (AXM0001) — by design
- Readout modules: pending full audit
The bridge axiom is intentional — it marks where the τ → orthodox
bridge enters as an assumption. Other modules should round-trip through
#print axioms producing no project-local entries beyond the bridge
layer.
Identifiers
Aliases & legacy IDs
taulib-v3-full-axiom-auditRelease lines
corpus_v3_workingRelations
Upstream dependencies (1)
Appears in (1)
Downstream uses (computed) (1)
Items in the corpus that reference this one via load-bearing relations. Computed from the full corpus-v3 graph at build time.
Version & History
Status disclaimer
A Corpus Item page reports the program's current internal record for this item. It does not imply external verification, scientific consensus, or final proof unless explicitly stated. Read it together with its dependencies, formalization status, and the program's overall stance.