Skip to content

docs: record the external revision and CI run for E-6 #41

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
hyperpolymath merged 3 commits into from
Oct 19, 2026
Merged

docs: record the external revision and CI run for E-6 #41

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
6fb6718
docs: record the external revision and CI run for E-6
claude Oct 19, 2026
8d43f2b
docs: date the E-6 record 2026-10-19 inside the 2026-10-12 snapshot
claude Oct 19, 2026
a26e487
Merge branch 'main' into docs/record-e6-external-revision
hyperpolymath Oct 19, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion README.adoc
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -190,7 +190,7 @@ interface is a breaking correction documented in link:docs/proof-transport.adoc[

[NOTE]
====
2026-10-12: Kripke semantics, the frame-condition correspondences, a non-factive model (`Warrant ≠ SoundWarrant` witnessed), the residual-evidence frame and the dependence test now live under `src/EpistemicTypes/Kripke/`; see link:docs/kripke-status-2026-10-12.adoc[]. Global warrant soundness for type-determined warrants is reported externally in choreographic-types but remains open pending an immutable external revision containing the theorem and its import and a successful type-check (E-6). Soundness for data-dependent warrants remains an assumption.
2026-10-12: Kripke semantics, the frame-condition correspondences, a non-factive model (`Warrant ≠ SoundWarrant` witnessed), the residual-evidence frame and the dependence test now live under `src/EpistemicTypes/Kripke/`; see link:docs/kripke-status-2026-10-12.adoc[]. Global warrant soundness for type-determined warrants is proved externally in choreographic-types, at the recorded revision `d8536184366f4ac4567aa066c5dbcb9220e3607a` with a successful CI type-check, and is not re-checked here (E-6). Soundness for data-dependent warrants remains an assumption.
====

[CAUTION]
Expand Down
4 changes: 2 additions & 2 deletions docs/kripke-status-2026-10-12.adoc
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -3,7 +3,7 @@

The modules under `src/EpistemicTypes/Kripke/` formalise Kripke semantics
and the results below. Complete epistemic logic and soundness for
data-dependent warrants remain outstanding; E-6 records the open external
data-dependent warrants remain outstanding; E-6 records the external
verification for type-determined warrants.

[cols="1,3,1",options="header"]
Expand All @@ -14,7 +14,7 @@ verification for type-determined warrants.
| E-3 | Correspondences, constructively: reflexive ⇔ factive (T, both directions); transitive ⇔ positively introspective (4, both directions); Euclidean ⇒ 5; serial ⇒ D. The converses of 5 and D need classical reasoning and are not claimed | PROVEN / OPEN as stated
| E-4 | A reflexive frame yields an `IndexedFactive` (`factive`) | PROVEN
| E-5 | *The non-factive model*: two worlds, access only w₀ → w₁; at w₀ there is a `Warrant` (evidence: a `Box` proof) for a false proposition, and no `sound` field can exist for it. `Warrant ≠ SoundWarrant`, witnessed | PROVEN (`Kripke/Belief.agda`: `believed`, `false-at-w₀`, `no-sound-warrant`); TESTED (`tests/reject/BeliefIsKnowledge`: factivity refused on this frame)
| E-6 | Global soundness of warrants in a reflexive frame — every type-determined warrant sound — is reported externally in choreographic-types (`Choreographic.Kripke`, citing this repo's `Warrant` at `495db9c`) | OPEN (an immutable external revision containing the theorem and its import, and a successful type-check, are not recorded here)
| E-6 | Global soundness of warrants in a reflexive frame — every type-determined warrant sound — is proved externally in choreographic-types (`Choreographic.Kripke`, `Frame.sound-warrant`), which imports this repo's `EpistemicTypes.Warrant` at `495db9cca003e12066a3cb9c9f2d7afa1a953aec` (`Warrant.agda`, `Base.agda` and `Access.agda` are unchanged between that commit and this one). Recorded external revision: choreographic-types `d8536184366f4ac4567aa066c5dbcb9220e3607a`. Type-check: its `Agda proofs` workflow, run 39288705455 on that commit, succeeded under Agda 2.6.4.3 with `--safe --without-K --no-libraries --ignore-interfaces --double-check` (the import is pinned by `scripts/fetch-siblings.sh` there) | RECORDED externally on 2026-10-19 (revision and CI run above; the rest of this table is the 2026-10-12 snapshot); not re-checked in this repository
|===

Separation (family bar, criterion 2): the belief model is a modality with
Expand Down
Loading