diff --git a/src/Lean/CoreM.lean b/src/Lean/CoreM.lean
index c625885b98b7..16557ee3d037 100644
--- a/src/Lean/CoreM.lean
+++ b/src/Lean/CoreM.lean
@@ -214,18 +214,32 @@ structure State where
   deriving Nonempty
 
 /--
-The pointer-valued fields of `Core.Context` that are updated at most a handful of times per command.
+The pointer-valued fields of `Core.Context` that are not updated on a recursion step.
 
-`withReader` can never reuse the `Context` record, so every `withRef`, `withOptions` or
-`withIncRecDepth` pays one reference count increment per pointer field. Grouping these fields into a
-subobject makes them cost a single increment together.
+`withReader` can never reuse the `Context` record, so every `withIncRecDepth` pays one reference
+count increment per pointer field. Grouping the remaining fields into a subobject makes
+them cost a single increment together.
+
+Membership follows measured update frequency, not the number of update sites: on a representative
+module, `withIncRecDepth` runs about 1.0M times and `withRef` about 31k, while `withOptions` runs
+*once*. Fields updated only on such rare paths belong here even where they have many syntactic
+update sites, and rebuilding this record on those paths is far cheaper than copying its fields on
+every recursion step.
 -/
 structure Context.Cold where
   /-- Name of the file being compiled. -/
   fileName       : String
   /-- Auxiliary datastructure for converting `String.Pos` into Line/Column number. -/
   fileMap        : FileMap
+  options        : Options := {}
+  maxRecDepth    : Nat := 1000
+  currNamespace  : Name := Name.anonymous
+  openDecls      : List OpenDecl := []
+  initHeartbeats : Nat := 0
+  maxHeartbeats  : Nat := getMaxHeartbeats options
+  ref            : Syntax := Syntax.missing
   quotContext    : Name := .anonymous
+  currMacroScope : MacroScope := firstFrontendMacroScope
   /-- If set, used to cancel elaboration from outside when results are not needed anymore. -/
   cancelTk?      : Option IO.CancelToken := none
   /-- Cache of `Lean.inheritedTraceOptions`. -/
@@ -234,15 +248,7 @@ structure Context.Cold where
 
 /-- Context for the CoreM monad. -/
 structure Context extends Context.Cold where
-  options        : Options := {}
   currRecDepth   : Nat := 0
-  maxRecDepth    : Nat := 1000
-  ref            : Syntax := Syntax.missing
-  currNamespace  : Name := Name.anonymous
-  openDecls      : List OpenDecl := []
-  initHeartbeats : Nat := 0
-  maxHeartbeats  : Nat := getMaxHeartbeats options
-  currMacroScope : MacroScope := firstFrontendMacroScope
   /--
   If `diag := true`, different parts of the system collect diagnostics.
   Use the `set_option diag true` to set it to true.