Skip to content

docs(proposals): record the last four owner rulings #50

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 2 commits into from
Nov 10, 2026
+59 −35
Merged

docs(proposals): record the last four owner rulings #50

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
21f10cd
docs(proposals): record the last four owner rulings
claude Nov 10, 2026
5f7f5fc
docs(proposals): name all four programme rulings in the plan
claude Nov 10, 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
64 changes: 42 additions & 22 deletions docs/proposals/mathesis-re-anchoring.adoc
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -6,11 +6,11 @@
:sectnums:
:icons: font

Status: *proposed* (2026-11-10). The owner ruled on six of its eight
decisions on 2026-11-10, through the selector (<<decisions>>). This document
changes no gate, schema, deed clause or data file. Each change that a ruling
does not cover still needs one. The work orders in <<work-orders>> are
written for a later implementation session.
Status: *proposed, with rulings* (2026-11-10). The owner ruled on each of its
eight decisions on 2026-11-10, through the selector (<<decisions>>). This
document changes no gate, schema, deed clause or data file. Each change that
a ruling does not cover still needs one. The work orders in <<work-orders>>
are written for a later implementation session.

The companion document is
link:mathesis-research-programme.adoc[the research programme]. This document
Expand Down Expand Up @@ -888,14 +888,27 @@ files pass. +
the template.

[[wo-1-4]]WO 1.4 Add CI lanes for Rocq and Lean::
*Steps:* Install Rocq 8.18.0 and Lean 4.15.0 at pinned versions with digest
checks. Assert each version in the run. Write a `deviation` record for each
toolchain that does not come from the Guix manifest or the container
(PROOF-POLICY §6). Write the same record for the Agda lane. Run the three
lanes on each commit to `main`, with no path filter. A lane that runs only
when a proof file changes gives no receipt for the other commits. +
*Ruling:* D-8 (a), 2026-11-10. The toolchains come from the Guix manifest.
The plan recommended the other arm. +
*Steps:* Add Agda, Rocq and Lean to `build/manifest.scm`, at the Guix
revision that `build/channels.scm` pins. The manifest lists none of them
today. Use the provisioning engine if it knows the three provers. Record the
version that the pinned Guix gives for each prover. Compare it with the
version in the THY-1 record: Agda 2.6.3, Rocq 8.18.0 and Lean 4.15.0. A
different version means that the receipt is earned again at the new version.
Run the three proof lanes inside the pinned Guix shell. Move the Agda lane
from the distribution package to the same shell. Assert each version in the
run. Run the three lanes on each commit to `main`, with no path filter. A
lane that runs only when a proof file changes gives no receipt for the other
commits. +
*Stop condition:* the pinned Guix has no package for a prover, or has only a
version that cannot check the proofs. Then stop and report. Do not install
from an archive without a `deviation` record (PROOF-POLICY §6) and a new
ruling. +
*Check:* each lane fails on the planted controls of WO 1.3. A commit that
changes only a document still gets three receipts.
changes only a document still gets three receipts. +
*Consequence:* until the manifest works, the Rocq leg and the Lean leg have
no CI lane.

[[wo-1-5]]WO 1.5 Write the receipt of Mathesis::
*Steps:* Write `verification/receipts/theory_praxis.deed` with
Expand Down Expand Up @@ -923,7 +936,12 @@ the reader refuses as `ungraded`, with the reader's reason. Keep the pin, the
digest check and the renderer. +
*Check:* the 17 pilot claims still derive `ungraded`. The hermetic tests pass
with fixture receipts in the §8.5.1 shape. +
*Needs ruling:* yes (D-5).
*Ruling:* D-5 (a), 2026-11-10. +
*Also under this ruling:* Amend ADR 0004 so that it names the canon reader.
The owner ratifies the ADR when the owner merges that change. Add a note at
the head of `proof-receipts-as-data.adoc`: PROOF-POLICY §8.5.1 settles the
receipt format and the reader, and experiments E1 to E6 stay open. Close
issue 28 with a pointer to §8.5.1, on the owner's word.

[[wo-2-3]]WO 2.3 Move the paths::
*Steps:* Apply the table in <<structure>> with `git mv`. Update the tools,
Expand Down Expand Up @@ -1069,8 +1087,8 @@ Each decision lists its arms with the most elegant and correct long-term arm
first. The recommended arm is marked where it differs. The plan above assumes
arm (a) in each case.

The owner ruled on six decisions through the selector on 2026-11-10. D-5 and
D-8 are open.
The owner ruled on each of the eight decisions through the selector on
2026-11-10.

. *D-1 Identity.* (a) The three shelves with the evidence spine, as in
<<identity>>. (b) An index only, with the theory and the applied area moved
Expand All @@ -1091,7 +1109,7 @@ D-8 are open.
. *D-5 Overlapping proposals.* (a) Amend ADR 0004 to use the canon reader,
and ratify it. Mark `proof-receipts-as-data.adoc` as settled in part by
PROOF-POLICY §8.5.1, and keep its experiments E1 to E6. Close issue 28 with
a pointer. (b) Keep the three open. *Open.*
a pointer. (b) Keep the three open. *Ruled 2026-11-10: (a).*
. *D-6 Open pull requests.* (a) The implementation session completes the
triage table and the owner approves each row. (b) The owner triages alone.
(c) Merge all 17 in order and resolve each conflict.
Expand All @@ -1103,12 +1121,14 @@ D-8 are open.
. *D-8 Proof toolchains.* (a) Pin Agda, Rocq and Lean in the Guix manifest.
(b) Install from release archives with `deviation` records now, and move
to Guix later. Recommended: (b), because it closes the hole this week.
*Open.*

The companion programme records two more rulings of the same day: the token
theory starts with the chain of PROOF-POLICY §5 and imports the
`resource-algebra` kernel. The order is provisional until experiment X-PF1
has a result.
*Ruled 2026-11-10: (a). The owner chose the Guix manifest, which is also
the route that PROOF-POLICY §6 prefers.*

The companion programme records four more rulings of the same day. The token
theory starts with the chain of PROOF-POLICY §5, and the order is
provisional until experiment X-PF1 has a result. The theory imports the
`resource-algebra` kernel. Statement S-2 lives in Mathesis. `januskey` is the
first slice from theorem to code.

[[no-rewrite]]
=== Why the history is not rewritten
Expand Down
30 changes: 17 additions & 13 deletions docs/proposals/mathesis-research-programme.adoc
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -6,13 +6,13 @@
:sectnums:
:icons: font

Status: *proposed* (2026-11-10). The owner ruled on two of its five decisions
on 2026-11-10 (<<programme-decisions>>). The rest is not ratified. This
document claims no proved result. A statement marked *pre-registered* is a
statement to prove or to refute. A sentence marked *reading* is the view of the author of this
programme. Each fact about another repository names that repository and its
commit in <<survey>>. Each such fact is that repository's own claim. This
session checked no proof.
Status: *proposed, with rulings* (2026-11-10). The owner ruled on four of its
five decisions on 2026-11-10 (<<programme-decisions>>). The rest is not
ratified. This document claims no proved result. A statement marked
*pre-registered* is a statement to prove or to refute. A sentence marked
*reading* is the view of the author of this programme. Each fact about
another repository names that repository and its commit in <<survey>>. Each
such fact is that repository's own claim. This session checked no proof.

The companion document is
link:mathesis-re-anchoring.adoc[the re-anchoring plan]. The plan puts the
Expand Down Expand Up @@ -708,9 +708,9 @@ laws are generated from the Agda source, the row can rise to `tested-only`.

=== First experiments

. *E-3.1* Choose one vertical slice with the owner. The survey suggests
`januskey` T-1 with T-10 and G-2. Write its rungs as claims and bridges.
Compute its composite status. +
. *E-3.1* Take `januskey` as the first vertical slice (ruling R-4): theorem
T-1 with rows T-10 and G-2. Write its rungs as claims and bridges. Compute
its composite status. +
*Pass condition:* the computed status is not stronger than the weakest
rung, and each document that states a stronger status is listed.
. *E-3.2* Generate the Idris2 statement of the token laws from the source of
Expand Down Expand Up @@ -873,7 +873,8 @@ The lines depend on each other in one direction only.
the canon reader.
. Line 2 can start. The owner ruled on the bridge centre on 2026-11-10
(decision D-7 of the plan).
. Line 3 needs one home repository that agrees to be the slice.
. Line 3 starts with `januskey` (ruling R-4). Each change in `januskey` is
made in that repository, by its own rules.
. Line 4 can run at any time. It shares only S-2 with the other lines.
. The horizon waits for lines 1 and 2 to produce records.

Expand Down Expand Up @@ -952,8 +953,8 @@ a line is not worth its cost.
== Decisions for the owner

Each decision lists the most elegant and correct long-term arm first. The
programme assumes arm (a). The owner ruled on R-1 and R-2 through the
selector on 2026-11-10. R-3, R-4 and R-5 are open.
programme assumes arm (a). The owner ruled on R-1 to R-4 through the
selector on 2026-11-10. R-5 is open.

. *R-1 The order of the tokens.* (a) The chain of S-1, as PROOF-POLICY §5
lists it. (b) A partial order in which `tested-only` and `argued` are not
Expand All @@ -966,9 +967,12 @@ selector on 2026-11-10. R-3, R-4 and R-5 are open.
*Ruled 2026-11-10: (a).*
. *R-3 The home of S-2.* (a) Mathesis, because the expression language is the
ledger's. (b) `resource-algebra`, as a kernel lemma.
*Ruled 2026-11-10: (a).*
. *R-4 The first slice for line 3.* The owner names the repository.
*Ruled 2026-11-10: `januskey`.*
. *R-5 The dossier.* (a) Mathesis describes the method and reports it as a
census. (b) The method goes to the standards repository as policy first.
*Open.*

[appendix]
[[survey]]
Expand Down
Loading