One-Line Split
Formal Artifacts
The authoritative objects are the ACL2 source books, certification artifacts, declared hashes, prover identity, and replay procedure.
Theorem Twins
Theorem twins are descriptive semantic envelopes. They make the formal layer easier for agents and reviewers to navigate without pretending the JSON layer is the proof kernel.
Transport Note
Live theorem-twin routes may also serve application/cbor companion encodings for agent and constrained-link transport. These CBOR artifacts are descriptive transport companions only: they are not CBOR-LD, they do not replace the JSON-LD twin routes, and they do not move authority away from the prover-specific formal artifacts.
Current Claim Boundary
- The current public claim is that Sovrient has a certified ACL2 theorem family, a live Isabelle/HOL pi theorem-twin route, and a bounded public reference surface for them.
- A second prover family,
Isabelle/HOL, now exists repo-internally for session scope, participant authority, and opportunity-brief safety; those twins remain repo-internal and do not include the live pi route. - Three raw theorem twins are published today:
frame,ZF gate, andpi minimal period. The repo-internal session-scope twins remain separate unless separately declared. - The theorem reference surface does not replace ACL2 certification or make JSON the authority layer.
- No claim is made that every production lane or SSEJ record is already formally theorem-bound.
Current Certified Family
Frame
Book: scf_dtau_001_frame
Role: abstract admission, governance, replay, and durability structure.
Exported theorems: 12
Load marker: :frame-loaded
Core1
Book: scf_dtau_001_core1
Role: minimal concrete singleton witness over p-core.
Exported theorems: 7
Load marker: :core1-loaded
ZF Gate Lane
Book: scf_dtau_001_zf_gate_core
Role: first real authoritative singleton path for the release-eligibility latch.
Exported theorems: 16
Load marker: :zf1-loaded
Additional Prover Family
Isabelle/HOL
Status: repo-internal, build-verified
Current theories: session_scope, participant_authority, opportunity_brief_safety
Current role: session-envelope, participant-boundary, and briefing-safety invariants.
Public route status: repo-internal only; the live pi theorem-twin route is tracked below.
Live Isabelle/HOL Pi Route
Pi Minimal Period
Framework: SOVRIENT_ISABELLE_PI_001
Role: canonical surfaced result
Status: build-verified, live public route
Theorem: minimal_shared_period_2pi_trig_complexexp
Alternate encoding: cbor · sha256 · manifest
Encoding note: application/cbor companion only; not CBOR-LD and not a replacement for the JSON-LD twin route.
Authority Chain
.lispsource books plus.certand.portartifacts define the current public ACL2 authority path..thysource theories, the Isabelle session root, and the replay wrapper define the repo-internal authority path for the second prover family.- Detailed theorem twins exist for both families, and raw live theorem twins are published for the ACL2
frameandZF gatebooks plus the Isabelle/HOLpi minimal periodroute today. - This public theorem reference surface summarizes the current family and claim boundary in bounded web-safe terms.
Why This Matters
ANATOP Fit
The theorem layer now follows the same authority-versus-twin pattern used elsewhere on the site: authoritative artifact, semantic twin, declared scope, and fail-closed regeneration when hashes drift.
SSEJ Fit
The formal layer now has a path to support the Justified component of SSEJ with machine-checkable theorem ids rather than only prose citations, while still keeping authority with ACL2.
What This Public Surface Proves
- Sovrient has a current certified ACL2 family consisting of frame, core witness, and first real lane books.
- Sovrient also has a build-verified repo-internal Isabelle/HOL family for session and briefing invariants.
- The formal layer now has a bounded public discovery surface with three resolving raw theorem-twin routes.
- The authority boundary is explicit: ACL2 artifacts remain primary, semantic twins remain descriptive.
What It Does Not Prove
- That every Sovrient operational lane is already covered by a certified concrete book.
- That the repo-internal Isabelle/HOL session-scope twins are already live public routes.
- That production SSEJ records already cite theorem ids on the public surface.
- That the current theorem family is a finished ontology or a complete public theorem registry.
Current Public Handles
- Theorem Reference JSON
- Live frame theorem twin JSON-LD
- Live frame theorem twin SHA-256
- Live frame theorem twin CBOR companion
- Live frame theorem twin CBOR SHA-256
- Live frame theorem twin CBOR manifest
- Live ZF gate theorem twin JSON-LD
- Live ZF gate theorem twin SHA-256
- Live ZF gate theorem twin CBOR companion
- Live ZF gate theorem twin CBOR SHA-256
- Live ZF gate theorem twin CBOR manifest
- Live Isabelle pi theorem twin JSON-LD
- Live Isabelle pi theorem twin SHA-256
- Live Isabelle pi theorem twin CBOR companion
- Live Isabelle pi theorem twin CBOR SHA-256
- Live Isabelle pi theorem twin CBOR manifest
- Supporting Methodology
- Supporting Methodology State JSON
- Machine State JSON
Related Public Surfaces
For procurement and teaming context, see Capabilities.