SessionUpdateProtocol
plain-language theorem explainer
A session on the Maximal Forcing program closes only when one of four progress events holds: a new forced invariant, an independence witness, a tighter admissibility bound, or an execution-plan update naming the remaining blocker. Anyone auditing Reality Closure certificates cites this as the session-progress contract. It is a pure structure: four Props plus a nonempty disjunction.
Claim. A session-update protocol is a record of four propositions $P_{\mathrm{inv}}$, $P_{\mathrm{ind}}$, $P_{\mathrm{adm}}$, $P_{\mathrm{plan}}$ (forced invariant landed; independence witness landed; admissibility tightened; execution plan updated) together with the nonempty-progress requirement $P_{\mathrm{inv}} \lor P_{\mathrm{ind}} \lor P_{\mathrm{adm}} \lor P_{\mathrm{plan}}$.
background
This module is the crown-theorem interface for Maximal Forcing Closure. It does not assert the final theorem. It states the certificate whose construction will be the theorem: for every claim $C$ in the forcing-closure of a program $P$ relative to a claim universe $U$, a classification of $C$ under $U$ is available. Once a real classifier exists for the final claim universe, the crown result is a projection from that certificate.
The session protocol sits beside that certificate language. Closing a working session is not free-form bookkeeping: it must record concrete progress of one of four kinds named in the structure. Upstream, the module imports the forced-invariant layer of Maximal Forcing, so "landed forced invariant" is meant in that sense: an invariant forced by the program rather than an ad hoc lemma.
proof idea
No proof. This is a structure definition: four fields of type Prop, plus a fifth field that is the disjunction of those four, enforcing nonempty progress. There are no tactics, no lemmas applied, and no term-mode construction beyond the inductive record type itself.
why it matters
Reality Closure is framed as a certificate program, not a single asserted theorem. This structure is the operational contract for how that program advances between sessions: every close must deposit either a forced invariant, an independence witness, a tighter admissibility constraint, or an updated plan that names the exact remaining blocker.
No downstream uses are wired yet in the graph. The declaration still earns its place as scaffolding discipline for the crown interface: it prevents "session closed" from meaning silent stall. In the broader Recognition forcing chain (T0–T8), Maximal Forcing is the meta-layer that packages what has been forced versus what remains open; this protocol is the bookkeeping face of that packaging.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.