d4_page_field_is
plain-language theorem explainer
The D4 Page field of the canonical Page-curve derived witness is definitionally the conjunction of the recognition-tick capacity-transfer law and the nondegenerate Page-curve shape on Fin 2 tensor Fin 2. Auditors of the unconditional quantum-gravity master theorem cite this to confirm the slot is genuine physics content: neither True nor the master conclusion. The proof is a one-line definitional equality.
Claim. The page-curve-derived field of the canonical Page-curve derived witness equals, by definition, the conjunction of (i) the recognition-tick capacity-transfer law (bulk capacity drops by $S_{BH}/N$ per emitted tick, radiation capacity rises by the same amount, total capacity conserved, ledger-tick curve matches the continuous Page curve) and (ii) the nontrivial Page-curve proposition (a nondegenerate configuration on $\mathrm{Fin}\,2\otimes\mathrm{Fin}\,2$ with zero endpoints, interior peak $S_{BH}/2$, and strict monotone rise then fall).
background
This module answers a formal-methods referee objection to the unconditional RS quantum-gravity master theorem. Witnesses shaped like $\Sigma(P:\mathrm{Prop}), P$ are inhabited by $\langle\mathrm{True},\mathrm{trivial}\rangle$, so the master statement is only as strong as the concrete propositions in its five slots. For each atom the audit supplies an rfl-level disclosure of what the field actually is, plus a standalone proof that it holds with no master clause assumed.
The D4 slot is the Page-curve derived witness. After peer-review finding F3, the canonical witness was strengthened beyond the degenerate $\mathrm{Fin},1$ route: it packages a nontrivial Page process on $\mathrm{Fin},2\otimes\mathrm{Fin},2$ with derived capacity-curve entropy readout, interior peak equal to half the Bekenstein-Hawking entropy, and monotone rise then fall across the peak.
Upstream, the capacity-transfer package states that bulk capacity drops by exactly $S_{BH}/N$ per emitted tick while radiation capacity rises by the same amount and total capacity is conserved. The nontrivial Page proposition asserts existence of $N\ge 2$, $S_{BH}>0$, and an interior peak with the full operator-readout Page shape.
proof idea
One-line definitional equality. The page_curve_derived projection of the canonical Page-curve derived witness reduces, by the structure definition of that witness (built from the nontrivial Page-curve derived witness), exactly to the conjunction of the recognition-tick capacity-transfer proposition and the nontrivial Page-curve proposition. rfl closes the goal; no further lemmas are invoked.
why it matters
This disclosure is the non-circularity check for the D4 Page slot. The module doc states the honest findings after M1–M3: carried clauses are no longer True placeholders, and non-circularity follows because the master conclusion is assembled from independently proved, concretely named, non-self-referential propositions. The D4 field is flagged as the nontrivial content (capacity transfer conjoined with nondegenerate Page shape), explicitly not True and not the master conclusion.
It closes peer-review finding F3 on the old degenerate Fin 1 / identity / zero-entropy witness. Sibling audit theorems do the same for T0–T8, cost-uniqueness, BMV positivity, and the inhabited certificate clauses (Lorentzian, Hawking, $c_{RS}$). No downstream graph consumers are recorded; the declaration exists so a referee can inspect the master theorem's input atoms by eye.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.