diff --git a/sdk/docs/manually-written/overview/explanations/ledger-model/index.rst b/sdk/docs/manually-written/overview/explanations/ledger-model/index.rst
index 42a836799609..4f628b111b21 100644
--- a/sdk/docs/manually-written/overview/explanations/ledger-model/index.rst
+++ b/sdk/docs/manually-written/overview/explanations/ledger-model/index.rst
@@ -32,9 +32,25 @@ it is an imaginary database that represents the union of all parties' databases.
 .. image:: ./images/da-ledger-model.svg
    :alt: A conceptual diagram of the Virtual Global Ledger.
 
+The ledger is fundamentally a record of interactions between actors resulting in shared facts that are stored as **contracts**.
+
+The actors on the ledger are called **parties**. Parties are the entities that authorize actions,
+sign transactions, and hold specific viewing rights. They can represent the people, organizations, or
+automated systems participating in a workflow. When parties interact and agree on a set of facts or
+obligations, that agreement is recorded on the ledger as a **contract**. A contract holds the actual data or state of the
+ledger at any given time. Every contract is assigned a unique, system-generated **contract ID** so the
+ledger can track its lifecycle.
+
+A contract is instantiated from a blueprint known as a **template**, which defines the rules of engagement with it.
+A template specifies what data the contract must contain, who is required to authorize it, and what subsequent
+actions (called **choices**) parties can take on it.
+
+A contract can also optionally be assigned a **contract key**, which is a unique, human-readable identifier tied to
+real-world data that allows parties to easily look up and interact with the contract over time.
+
 The Ledger Model defines:
 
-  #. What the changes and the ledgers looks like - the :ref:`structure <ledger-structure>` of the Canton Ledger
+  #. What the changes and the ledgers look like - the :ref:`structure <ledger-structure>` of the Canton Ledger
   #. Who sees which changes and data - the :ref:`privacy model <da-model-privacy>` for the Canton Ledger
   #. What changes to the ledger are allowed and who can request them - the integrity model for the Canton Ledger
 
@@ -77,10 +93,10 @@ The ``counterparty`` can accept the proposal with the ``Accept`` choice to creat
    :end-before: SNIPPET-PROPOSAL-END
 
 .. .. toctree::
-   :maxdepth: 3
-   ledger-structure
-   ledger-privacy
-   ledger-validity
-   ledger-integrity
-   ledger-daml
-   ledger-exceptions
+:maxdepth: 3
+ledger-structure
+ledger-privacy
+ledger-validity
+ledger-integrity
+ledger-daml
+ledger-exceptions
diff --git a/sdk/docs/manually-written/overview/explanations/ledger-model/ledger-integrity.rst b/sdk/docs/manually-written/overview/explanations/ledger-model/ledger-integrity.rst
index fe41109a71f8..40b7e676b99a 100644
--- a/sdk/docs/manually-written/overview/explanations/ledger-model/ledger-integrity.rst
+++ b/sdk/docs/manually-written/overview/explanations/ledger-model/ledger-integrity.rst
@@ -6,7 +6,7 @@
 Integrity
 #########
 
-The section on the :ref:`ledger structure <ledger-structure>` section answered the question “What does the Ledger looks like?” by introducing a hierarchical format to record the party interactions as changes to the Ledger.
+The section on the :ref:`ledger structure <ledger-structure>` answered the question “What does the Ledger look like?” by introducing a hierarchical format to record the party interactions as changes to the Ledger.
 The section on :ref:`privacy <da-model-privacy>` answered the question “Who sees which changes and data?” by introducing projections.
 This section addresses the question "Who can request which changes?" by defining which ledgers are valid.
 
@@ -148,7 +148,7 @@ Interaction with projection
 ===========================
 
 Apart from introducing the validity notion, this page also discusses how validity interacts with privacy, which is defined via :ref:`projection <da-model-projections>`.
-To that end, the sections on the different validity conditions analyse the prerequisites under what the following two properties hold:
+To that end, the sections on the different validity conditions analyse the prerequisites under which the following two properties hold:
 
 * **Preservation**: If the Ledger adheres to a condition, then so do the projections.
   This property ensures that a valid Ledger does not appear as invalid to individual parties,
@@ -180,23 +180,19 @@ This section introduces the notions that are needed to make this precise:
 Execution order
 ===============
 
-The meaning of "before" and "after" is given by establishing an execution order on the :ref:`nodes <def-action>` of a ledger.
-The ledger's graph structure already defines a :ref:`happens-before order <da-ledger-definition>` on ledger commits.
-The execution order extends this happens-before order to all the nodes within the commits' transactions
-so that "before" and "after" are also defined for the nodes of a single transaction.
-This is necessary because a contract can be created and used multiple times within a transaction.
+The meaning of "before" and "after" for actions has been formally defined by the **Global Execution Order** (also called execution order in this section)
+introduced in the :ref:`ledger structure <ledger-structure>` section.
+
+Recall that this (global) execution order is established by seamlessly combining two levels of hierarchy:
+1. The **happens-before** order of the ledger, which orders the commits themselves.
+2. The **Transaction Execution Order**, which strictly orders the discrete nodes within each commit (corresponding to a pre-order traversal of the transaction forest).
+
+This combination is necessary because a contract can be created and used multiple times within a single transaction.
+
 In the ``AcceptAndSettle`` :ref:`action of the DvP example <da-dvp-propose-accept-and-settle-action>`, for example,
 contract #3 is used twice (once in the non-consuming exercise at the root and once consumingly in the first consequence)
 and contract #4 is created and consumed in the same action.
 
-.. admonition:: Definiton: execution order
-
-   For two distinct nodes `n`:sub:`1` and `n`:sub:`2` within the same action or transaction, `n`:sub:`1` **executes before** `n`:sub:`2`
-   if `n`:sub:`1` appears before `n`:sub:`2` in the `preorder traversal <https://en.wikipedia.org/wiki/Tree_traversal#Pre-order,_NLR>`_ of the (trans)action, noting that the transaction is an ordered forest.
-   For a ledger, every node in commit `c`:sub:`1` **executes before** every node in commit `c`:sub:`2`
-   if the commit `c`:sub:`1` happens before `c`:sub:`2`.
-
-     
 Diagrammatically, the execution order is given by traversing the trees from root to leaf and left to right:
 the node of a parent action executes before the nodes in the subactions, and otherwise the nodes on the left precede the nodes on the right.
 For example, the following diagram shows the execution order with bold green arrows for the running DvP example.
@@ -231,7 +227,7 @@ which may use as inputs the contracts created outside of the piece.
 
 .. _def-internal-consistency:
 
-.. admonition:: Definition: internal consistency
+.. admonition:: Definition: internal consistency for a contract
 
    An action, transaction, or ledger is **internally consistent for a contract** `c`
    if for any two distinct nodes `n`:sub:`1` and `n`:sub:`2` on `c` in the action, transaction, or ledger,
@@ -269,7 +265,7 @@ For example, the whole ledger shown above in the :ref:`execution order example <
 
 In contrast, the next diagram shows that the ledger in the :ref:`consistency violation example <da-model-consistency-violation>` is not internally consistent for contract #1.
 This contract appears in nodes ①, ②, and ④.
-The second condition is violated but violated for `n`:sub:`1` = ④ and `n`:sub:`2` = ② as ④ does not execute before ②.
+The second condition is violated only for `n`:sub:`1` = ④ and `n`:sub:`2` = ② as ④ does not execute before ②.
 Note that the second condition is satisfied for `n`:sub:`1` = ② and `n`:sub:`2` = ④, but the definition quantifies over both pairs (②, ④) and (④, ②).
 The first condition is also satisfied because the Create node ① executes before both other nodes ② and ④.
 
@@ -352,7 +348,7 @@ then so is the (trans)action or ledger itself.
 This statement can be shown with a similar argument.
 
 Importantly, reflection requires a *signatory* of the contracts in `P`, not just a stakeholder.
-The following example shows that the propery does not hold if `P` contains a stakeholder, but no signatory.
+The following example shows that the property does not hold if `P` contains a stakeholder, but no signatory.
 To that end, we extend the ``SimpleAsset`` template with a non-consuming ``Present`` choice
 so that the issuer and owner can show the asset to a choice observer ``viewer``:
 
@@ -432,8 +428,8 @@ This essentially follows from two observations:
   That is, all inputs and outputs of a transaction are explicitly captured in contracts, choice arguments and exercise results.
 
 Not every such projection can be expressed as a set of commands on the Ledger API, though.
-The Ledger Model considers this lack of expressivity artificial, because future versions of the Ledger API may remove such restrictions.
-There are two kinds of cases where ledger API commads are less expressive than the ledger model defined here.
+The Ledger Model considers this lack of expressivity artificial, therefore future versions of the Ledger API may remove such restrictions.
+There are two kinds of cases where ledger API commands are less expressive than the ledger model defined here.
 First, a projection may contain a Fetch node at the root, like the :ref:`projection of the DvP <da-dvp-acceptandsettle-projection>` ``AcceptAndSettle`` choice for Bank 2.
 Yet, there is no Ledger API command to fetch a contract, as there are only commands for creating and exercising contracts.
 Second, the Ledger API command language does not support feeding the result of an Exercise as an argument to a subsequent command.
@@ -444,7 +440,7 @@ For example, suppose that the ``AcceptAndSettle`` choice of ``ProposeSimpleDvP``
    :start-after: SNIPPET-ACCEPTANDSETTLEDVP-BEGIN
    :end-before: SNIPPET-ACCEPTANDSETTLEDVP-END
 
-Bob can then execute accept and settle the DvP in one transaction by creating a helper contract and immediately exercising the ``Execute`` choice.
+Bob can then execute the AcceptAndSettle choice on the DvP in one transaction by creating a helper contract and immediately exercising the ``Execute`` choice.
 
 .. literalinclude:: ./daml/SimpleDvP.daml
    :language: daml
@@ -495,9 +491,9 @@ This section introduces the notions to formalize this:
 
 * The :ref:`authorization context <da-ledgers-authorization-context>` captures the parties who have actually authorized an action.
 
-* `Well-authorization :ref:<da-ledgers-authorization-rules>` demands that the authorization context includes all the required authorizers.
+*:ref:`Well-authorization <da-ledgers-authorization-rules>` demands that the authorization context includes all the required authorizers.
 
-The running example of :ref:`Bob skipping the propose-accept workflow <da-dvp-ledger-create-auth-failure>` will be used to show how node ③ requires more authorizers than its authorization context provides, and is thus not well auhtorized.
+The running example of :ref:`Bob skipping the propose-accept workflow <da-dvp-ledger-create-auth-failure>` will be used to show how node ③ requires more authorizers than its authorization context provides, and is thus not well authorized.
 For ease of reference, the ledger diagram is repeated below.
 
 .. https://lucid.app/lucidchart/cd2cef11-6f69-4f9c-8e1e-d79488547de2/edit
@@ -791,13 +787,13 @@ For example, consider a Ledger with a root action that no honest party is allowe
 So none of the projections contains this root action and therefore the projections cannot talk about its conformance or internal well-authorization.
 Fortunately, this is not necessary either, because we care only about the pieces of the Ledger that are visible to some honest party.
 
-More formally, two Ledgers are said to be **equivalent** for a set of parties `Q` if the projections of the two Ledgers to `Q` are the same.
+More formally, two Ledgers :math:`L` and :math:`L'` are said to be **equivalent** for a set of parties `Q` if the projections of the two Ledgers to `Q` are the same, i.e.
+if :math:`\text{Proj}_P(L)=\text{Proj}_P(L')`.
 Then reflection holds in the sense that there is an equivalent weakly valid Ledger.
-Let `F` be a set of sets of parties whose union contains the set of parties `Q`.
-If for every set `P` in `F`, the projection of a Ledger `L` to `P` is weakly valid for `P` insterected with `Q`,
-then the projection of `L` to `Q` is weakly valid.
-Note that this projection of `L` to `Q` is equivalent to `L` for `Q` due to the :ref:`absorbtion property of projection <da-model-transaction-projection>`.
-
+Let `F` be a set of sets of parties whose union contains the set of parties `Q`, :math:`Q \subseteq \bigcup_{P \in \mathcal{F}} P`;
+If for every set `P` in `F`, :math:`\text{Proj}_P(L)` is weakly valid for :math:`P \cap Q`, parties in both `P` and `Q`,
+then :math:`\text{Proj}_Q(L)` is weakly valid.
+Note that for parties in `Q`, :math:`\text{Proj}_Q(L)` is equivalent to `L`,  due to the :ref:`absorption property of projection <da-model-transaction-projection>`.
 
 ..
   parking lot
@@ -811,29 +807,29 @@ Note that this projection of `L` to `Q` is equivalent to `L` for `Q` due to the
 
 
 .. 
-  The next section discusses the criteria that rule out the above examples as
-  invalid ledgers.
-  
-  Ledger projections do not always satisfy the definition of
-  consistency, even if the ledger does. For example, in P's view, `Iou Bank A` is
-  exercised without ever being created, and thus without being made
-  active. Furthermore, projections can in general be
-  non-conformant. However, the projection for a party `p` is always
-  
-  - internally consistent for all contracts,
-  - consistent for all contracts on which `p` is a stakeholder, and
-  - consistent for the keys that `p` is a maintainer of.
-  
-  In other words,
-  `p` is never a stakeholder on any input contracts of its projection. Furthermore, if the
-  contract model is **subaction-closed**, which
-  means that for every action `act` in the model, all subactions of
-  `act` are also in the model, then the projection is guaranteed to be
-  conformant. As we will see shortly, Daml-based contract models are
-  conformant. Lastly, as projections carry no information about the
-  requesters, we cannot talk about authorization on the level of
-  projections.
-  
+The next section discusses the criteria that rule out the above examples as
+invalid ledgers.
+
+Ledger projections do not always satisfy the definition of
+consistency, even if the ledger does. For example, in P's view, `Iou Bank A` is
+exercised without ever being created, and thus without being made
+active. Furthermore, projections can in general be
+non-conformant. However, the projection for a party `p` is always
+
+- internally consistent for all contracts,
+- consistent for all contracts on which `p` is a stakeholder, and
+- consistent for the keys that `p` is a maintainer of.
+
+In other words,
+`p` is never a stakeholder on any input contracts of its projection. Furthermore, if the
+contract model is **subaction-closed**, which
+means that for every action `act` in the model, all subactions of
+`act` are also in the model, then the projection is guaranteed to be
+conformant. As we will see shortly, Daml-based contract models are
+conformant. Lastly, as projections carry no information about the
+requesters, we cannot talk about authorization on the level of
+projections.
+
 
 
   Contract state
@@ -858,18 +854,18 @@ Note that this projection of `L` to `Q` is equivalent to `L` for `Q` due to the
   The figures below visualize the state of different contracts at all points in the example ledger.
 
   .. https://www.lucidchart.com/documents/edit/19226d95-e8ba-423a-8546-e5bae6bd3ab7
-  .. figure:: ./images/consistency-paint-offer-activeness.svg
-     :align: center
-     :width: 100%
-     :alt: The first time sequence from above. Every action in the first and second commits is inexistent; in the third commit, Exe A (PaintOffer P A P123) is active while all the actions below it are archived.
+.. figure:: ./images/consistency-paint-offer-activeness.svg
+:align: center
+:width: 100%
+:alt: The first time sequence from above. Every action in the first and second commits is inexistent; in the third commit, Exe A (PaintOffer P A P123) is active while all the actions below it are archived.
 
      Activeness of the `PaintOffer` contract
 
   .. https://www.lucidchart.com/documents/edit/19226d95-e8ba-423a-8546-e5bae6bd3ab7
-  .. figure:: ./images/consistency-alice-iou-activeness.svg
-     :align: center
-     :width: 100%
-     :alt: The same time sequence as above, but with PaintOffer P A P123 in the second commit and Exe A (Iou Bank A) in the third commit also active.
+.. figure:: ./images/consistency-alice-iou-activeness.svg
+:align: center
+:width: 100%
+:alt: The same time sequence as above, but with PaintOffer P A P123 in the second commit and Exe A (Iou Bank A) in the third commit also active.
 
      Activeness of the `Iou Bank A` contract
 
diff --git a/sdk/docs/manually-written/overview/explanations/ledger-model/ledger-privacy.rst b/sdk/docs/manually-written/overview/explanations/ledger-model/ledger-privacy.rst
index 075ec6c56685..5bc14ba0c78a 100644
--- a/sdk/docs/manually-written/overview/explanations/ledger-model/ledger-privacy.rst
+++ b/sdk/docs/manually-written/overview/explanations/ledger-model/ledger-privacy.rst
@@ -10,6 +10,10 @@ The :ref:`ledger structure section <ledger-structure>` answered the question "Wh
 This section addresses the question "Who sees which changes and data?".
 That is, it explains the privacy model for Canton Ledgers.
 
+.. note::
+   As established in the previous section, we assume throughout this chapter that the Ledger is a **totally ordered sequence of commits**.
+   We defer the discussion of the general partial order (the DAG) to the :ref:`causality section <local-ledger>`.
+
 The privacy model of Canton Ledgers is based on a **need-to-know basis**,
 and provides privacy **on the level of subtransactions**.
 Namely, a party learns only those parts of party interactions that affect contracts in which the party has a stake,
@@ -38,7 +42,7 @@ The informees for a node are the union of the sets marked with X in the followin
 
 .. _def-informee:
 
-.. list-table:: Definiton: The **informees** of a node are the union of the sets marked with X.
+.. list-table:: Definition: The **informees** of a node are the union of the sets marked with X.
    :widths: 20 20 20 20 20
    :header-rows: 1
 
@@ -109,8 +113,11 @@ For example, the diagram below extends the :ref:`subaction diagram <da-ledger-su
 Here, the Create node ③ is part of three subactions, namely those rooted at nodes ①, ②, and ③.
 Accordingly, this Create node is shown to the informees of all these actions, even if they are not informees of the node itself.
 Those parties are called witnesses.
-Formally, for a given transaction `tx`, the **witnesses** of a node in `tx` are the union of the informees of all subactions of `tx` that contain the node.
-In particular, every informee of the node is also a witness.
+
+Because a transaction is a forest of trees, a node is contained within every action rooted at its ancestors.
+Formally, for a given transaction `tx`, the **witnesses** of a node are the union of the informees of all subactions of `tx` that contain the node.
+Equivalently, in terms of the tree structure, the witnesses of a node are the union of the informees of the node itself and the informees of all its **ancestor** nodes within `tx`.
+In particular, every informee of a node is also a witness of that node.
 
 The diagram shows the witnesses of a subaction in purple on its root action.
 For node ③, the witnesses are Alice, Bob, and Bank 1, because Bob is an informee of ① and ③; Bank 1 is an informee of ② and ③; and Alice is an informee of ① and ②.
@@ -177,29 +184,35 @@ This shows that projection can turn a single root action into a list of subactio
 
 The projection to both Bank 1 and Bank 2 at the bottom shows that a projection to several parties may contain strictly more information than the projections to each of the parties together.
 Said differently, it is impossible to reconstruct the projection to Bank 1 and Bank 2 solely from the projection for Bank 1 and the projection for Bank 2.
-Here, this is because the order of the three root actions cannot be uniquely determined from the individual projections.
+Here, this is because the order of the three root actions cannot be uniquely determined from the union of the individual projections.
 For this reason, projection is defined for a set of parties.
 
 .. _def-tx-projection:
 
-.. admonition:: Definition: projection
-                
-   The **projection** of a transaction for a set `P` of parties is the
-   subtransaction obtained by doing the following for each root action `act` of the transaciton.
+.. admonition:: Definition: Projection
+
+   The **projection** of a transaction :math:`tx` for a set of parties :math:`P` is the subtransaction obtained by applying the following recursive rules to each root action :math:`act`:
+
+   #. **Keep:** If :math:`P` contains at least one of the **informees** of :math:`act`, keep :math:`act` as-is, including its entire subtree of consequences.
+   #. **Promote:** Otherwise, if :math:`act` has consequences, replace :math:`act` with the projection for :math:`P` of its consequences (its **frontier**). This may result in a sequence of sub-actions or an empty sequence.
+   #. **Drop:** Otherwise, drop :math:`act`.
+
+The resulting :math:`\text{Proj}_P(tx)` is a **transaction forest** that preserves the original sibling ordering and ancestral relationships of the surviving actions.
+
+.. note::
+   This definition operates on **actions** (entire subtrees), not individual nodes. A node :math:`[A]` is included in the projection :math:`\text{Proj}_P(tx)` if and only if at least one member of :math:`P` is a **witness** to that node.
 
-   #. If `P` contains at least one of the informees of `act`, keep `act` as-is, including its consequences.
-   #. Else, if `act` has consequences, replace `act` by the projection (for `P`) of its consequences,
-      which might be empty.
-   #. Else, drop `act` including its consequences.
 
-This definition does not operate on nodes, but on actions, that is, subtrees of nodes.
-Accordingly, the projection of a transaction for a set of parties `P` contains a node if and only if `P` contains at least one of the witnesses of the node.
 
 As a projection is a transaction, it is possible to project a projection further.
-The projection operation has the following **absorbtion** property:
+The projection operation has the following **absorption** property:
 
 Projection to decreasing subsets of parties is absorbing.
-That is, if a set of parties `P` is a subset of `Q`, then projecting a transaction first to `Q` and then to `P` is the same as projecting it directly to `P`.
+That is, if a set of parties `P` is a subset of `Q`, then projecting a transaction first to `Q` and then to `P` is the same as projecting it directly to `P`. Symbolically,
+
+.. math::
+      \text{Proj}_P(\text{Proj}_Q(tx)) = \text{Proj}_P(tx) \quad \text{for } P \subseteq Q
+
 Intuitively, this property expresses the fact that a group of parties jointly learns at least as much about a transaction as any subgroup of these parties learns by themselves.
 The converse is false, as the above example with projection to Banks 1 and 2 has shown.
 
@@ -218,22 +231,26 @@ as it hides who is involved in the hidden parts of the transaction.
 Ledger projection
 =================
 
-Finally, the **projection of a ledger** `l` for a set `P` of parties is a DAG of updates obtained as follows:
+Finally, the **projection :math:`\text{Proj}_P(L)` of a ledger** `L` for a set `P` of parties is a DAG of updates obtained as follows:
 
-* Project the transaction of each update in `l` for `P`, but retain the update ID.
+* Project the transaction of each update in `L` for `P`, but retain the update ID.
 
 * Remove updates with empty transactions from the result.
 
-We defer defining the edges in the projection to the :ref:`causality section <local-ledger>`.
-Until then, we pretend that the ledger is totally ordered and projections retain the same ordering.
+.. note::
+   Update IDs serve as the "glue" across projections. Even if two parties see entirely different action nodes within a commit, the fact that they share the same **Update ID** allows them to correlate their views
+    and verify that their respective projections belong to the same atomic transaction.
 
-Notably, the projection of a ledger is not a ledger, but a DAG of updates.
-The requesters from the commit cannot be retained because they are typically witnesses of the actions in the projection,
-but not informees.
-Yet, the informees of the action must not know all the witnesses.
-For example, if Bank 1's projection did mention Bob as the requester of the last commit,
+Notably, the projection of a ledger is not formally a ledger itself. A true ledger consists of **commits** (which include the requesters).
+Because the projection must strip the requesters away for privacy, the true result is a **DAG of updates**, rather than a DAG of commits.
+The requesters cannot be retained because they are typically witnesses of the actions in the projection, but not informees.
+Yet, the informees of the action must not know all the witnesses. For example, if Bank 1's projection did mention Bob as the requester of the last commit,
 then Bank 1 could infer that Bob is a witness of Alice exercising the ``Transfer`` choice on contract #1.
 
+**A note on ordering:**
+Ledger projection filters action nodes while preserving the underlying graph edges. Under our working premise of a totally ordered ledger, the resulting projection naturally forms a linear sequence of updates.
+We defer defining the actual edges that form the general DAG of updates to the :ref:`Causality <local-ledger>` section.
+
 Projecting the ledger of the complete DvP example yields the following projections for each party.
 
 .. _da-dvp-ledger-projections:
@@ -247,7 +264,7 @@ Projecting the ledger of the complete DvP example yields the following projectio
 
 Examine each party's projection in turn:
 
-#. Alice sees all of the first, thrid, and forth commit
+#. Alice sees all of the first, third, and fourth commit
    as she is an informee of all root actions.
    In contrast, Alice does not see anything of the second commit,
    as she is not a stakeholder of Bob's ``SimpleAsset`` of 1 USD.
@@ -258,7 +275,7 @@ Examine each party's projection in turn:
    This effect is discussed below under :ref:`retroactive divulgence <da-model-divulgence>`.
 
 #. Bob's projection is analogous to Alice's:
-   He sees everything of the second, third, and forth commit,
+   He sees everything of the second, third, and fourth commit,
    but nothing of the first commit and instead merely contract #1 as an input.
 
 #. Banks 1 and 2 only see the commits in which they create their ``SimpleAsset`` and the ``Transfer`` Exercises on them.
@@ -273,14 +290,16 @@ They can therefore infer that their projections have happened in the same atomic
    :brokenref:`updates tree stream <com.daml.ledger.api.v2.UpdateService.GetUpdateTrees>`.
 
 
-
 .. _da-model-divulgence:
 
 Divulgence: When non-stakeholders see contracts
 ***********************************************
 
 The guiding principle for the privacy model of Canton ledgers is that contracts should only be shown to their stakeholders.
-However, ledger projections can cause contracts to become visible to other parties as well.
+However, because actions are hierarchical, informees of a parent action are, by definition, witnesses to all of its
+subsequent child nodes.
+
+This hierarchical visibility causes contracts to become visible to parties who are not stakeholders.
 Showing contracts to non-stakeholders through ledger projections is called **divulgence**.
 Divulgence is a deliberate choice in the design of Canton Ledgers and comes in two forms:
 
@@ -292,7 +311,7 @@ Divulgence is a deliberate choice in the design of Canton Ledgers and comes in t
   namely to see that the asset now belongs to Alice.
   
   In general, there is no point in hiding the consequences of an action.
-  Bob could anyway compute the consequences of the actions it is an informee of, because Daml is deterministic.
+  Bob could anyway compute the consequences of the actions he is an informee of, because Daml is deterministic.
 
 * **Retroactive divulgence** refers to an input contract being shown to the non-informee witnesses of a node using this contract.
   For example, the Fetch on Bob's ``SimpleAsset`` (contract #2) is visible to Alice
@@ -355,7 +374,7 @@ on which the Bob becomes a contract observer.
 This requires extending the contract model with a (consuming) exercise action on the ``SimpleAsset``
 that creates a new ``SimpleAsset``, with observers of Alice's choice.
 In addition to the increase in actions on the Ledger,
-the two approaches differ in in who learns about the parties that are informed about the contract:
+the two approaches differ in who learns about the parties that are informed about the contract:
 
 * If Alice discloses her ``SimpleAsset`` to Bob via an off-ledger channel,
   only Alice and Bob need to know about this disclosure.
@@ -369,13 +388,17 @@ the two approaches differ in in who learns about the parties that are informed a
   That is, all stakeholders learn about each other.
   This created a privacy problem when Alice actually does not want that Bob and Charlie know of each other.
 
-Moveover, adding parties as observers scales poorly to large numbers,
+Moreover, adding parties as observers scales poorly to large numbers,
 because every observer learns about every other observer:
 A Create event with `N` observers appears in the projection of at least those `N` parties.
 So the size of all projections together is already quadratic in `N` as an action of size at least `N` appears in `N` different projection.
 If the observers are added one by one, then `N` archives and creations are needed,
 which means the size of all projections together is cubic in `N`.
 
+Thus, while adding observers is a valid Daml feature, this scaling issue highlights why it should only be used when parties
+truly require permanent, shared visibility. For temporary or targeted access, relying on explicit off-ledger disclosure is
+the recommended design pattern to ensure observer privacy and prevent unnecessary ledger bloat.
+
 .. _da-privacy-shape-revealing:
 
 Shape-revealing projection
diff --git a/sdk/docs/manually-written/overview/explanations/ledger-model/ledger-structure.rst b/sdk/docs/manually-written/overview/explanations/ledger-model/ledger-structure.rst
index 68241f5d7a11..de711e160942 100644
--- a/sdk/docs/manually-written/overview/explanations/ledger-model/ledger-structure.rst
+++ b/sdk/docs/manually-written/overview/explanations/ledger-model/ledger-structure.rst
@@ -28,14 +28,14 @@ Bob accepts the proposal and settles the DvP.
    :start-after: SNIPPET-SCRIPT-BEGIN
    :end-before: SNIPPET-SCRIPT-END
 
-Acceptance and settlement can happen either in a single step via the ``AcceptAndSettle`` choice.
+Acceptance and settlement can happen either in a single step via the ``AcceptAndSettle`` choice:
 
 .. literalinclude:: ./daml/SimpleDvP.daml
    :language: daml
    :start-after: SNIPPET-ACCEPT_AND_SETTLE-BEGIN
    :end-before: SNIPPET-ACCEPT_AND_SETTLE-END
 
-Or in two separate steps with ``Accept`` followed by ``Settle``:
+or in two separate steps with ``Accept`` followed by ``Settle``:
 
 .. literalinclude:: ./daml/SimpleDvP.daml
    :language: daml
@@ -103,9 +103,11 @@ Overall, the settlement in the above example contains two types of actions:
 
 #. Exercising choices on contracts.
 
-These are also the two main kinds of actions in the Ledger Model.
+These are also the two main types of actions in the Ledger Model.
 
-A **node** is one of the following:
+To understand the ledger structure, we must distinguish between an action node (the discrete event data) and an action (the entire execution tree).
+
+An action node or simply a **node** is one of the following:
 
 #. A **Create** node records the creation of the contract.
    It contains the following pieces of information:
@@ -120,22 +122,22 @@ A **node** is one of the following:
 
    * The **contract observers**, or just observers for short, are the set of parties that will be informed about the contract creation and archival, in addition to the signatories.
 
-   In Daml, the signatories and contract observers are determined by the ``signatory`` and ``observer`` clauses defined by the template.
+In Daml, the signatories and contract observers are determined by the ``signatory`` and ``observer`` clauses defined by the template.
    
    Create nodes are depicted as shown below.
    Diagrams often omit fields with empty values and observers that are also signatories.
 
    .. https://lucid.app/lucidchart/31888b88-d836-457d-a4a8-05e3e161e07f/edit
-   .. image:: ./images/create-node.svg
-      :align: center
-      :width: 30%
-      :alt: The structure of a **Create** node.
+.. image:: ./images/create-node.svg
+:align: center
+:width: 30%
+:alt: The structure of a **Create** node.
 
 #. An **Exercise** node records the parameters of a choice that one or more parties have exercised on a contract.
    It contains the following pieces of information:
 
    * An exercise **kind**, which is either **consuming** or
-     **non-consuming**. Once consumed, a contract cannot be used again;
+     **non-consuming**. Once consumed, a contract cannot be used (i.e. fetched or subject to Exercise actions on) again;
      for example, Alice must not be able to transfer her asset twice, as this would be double spending.
      In contrast, contracts exercised in a non-consuming fashion can be reused, for example for expressing a delegation from one party to another.
       
@@ -144,7 +146,7 @@ A **node** is one of the following:
 
    * The **interface ID** if this choice was exercised through a Daml interface.
 
-   * The **template ID** that defines the smart contract code for the choice with the given **choice name**;
+   * The **template ID** that defines the smart contract code for the choice with the given **choice name**,
      and the **choice arguments** that are passed to the smart contract code.
      
    * An associated set of parties called **actors**.
@@ -160,12 +162,12 @@ A **node** is one of the following:
    Diagrams omit the kind if it is consuming, empty field values, and choice observers that are also actors.
 
    .. https://lucid.app/lucidchart/ce3c7eb2-081e-4ac4-af92-5efc11d21c17/edit
-   .. image:: ./images/exercise-node.svg
-      :align: center
-      :width: 30%
-      :alt: The structure of an **Exercise** node.
+.. image:: ./images/exercise-node.svg
+:align: center
+:width: 30%
+:alt: The structure of an **Exercise** node.
 
-#. A **Fetch** node on a contract, which demonstrates that the contract exists and is active at the time of fetching.
+#. A **Fetch** node acting on a contract, which demonstrates that the contract exists and is active at the time of fetching.
    A Fetch behaves like a non-consuming Exercise with no consequences, and can be repeated.
    The fetch node contains the following pieces of information, analogous to Exercise nodes:
    **contract ID**, **interface ID**, **template ID**, and the **actors**, namely the parties who fetch the contract.
@@ -173,25 +175,38 @@ A **node** is one of the following:
    Fetch nodes are depicted as shown below.
 
    .. https://lucid.app/lucidchart/27844d5e-0cdb-4f22-8f67-e97f3839e613/edit
-   .. image:: ./images/fetch-node.svg
-      :align: center
-      :width: 30%
-      :alt: The structure of a **Fetch** node.
+.. image:: ./images/fetch-node.svg
+:align: center
+:width: 30%
+:alt: The structure of a **Fetch** node.
 
+Later, in the :ref:`causality section <local-ledger>`, we will also encounter another type of node called NoSuchKey.
 
-An **action** consists of a **root node** and a list of **consequences**, which are themselves actions.
+An **action** consists of a **root node** and an ordered list of **consequences**, which are themselves actions that get triggered as a result of the execution of the action at the root node.
 This gives rise to the tree structure of an action: The root node of an action has as children the root nodes of its consequences.
 
-An action inherits its kind from its root node:
+An action's tree structure assigns a unique coordinate or address to each node, represented as a sequence of integers:
+
+* The root node has the empty coordinate :math:`\epsilon`.
+* If a node has coordinate :math:`c`, the root node of its :math:`i`-th consequence has the coordinate :math:`c \cdot i`.
+
+This hierarchical structure establishes a local **Action Execution Order**. Because the root node of an action triggers its consequences, the root node is said to execute before its consequences.
+Within the list of consequences, actions execute according to their order in the list (left-to-right). Mathematically, the execution order :math:`\prec_{act}` of the nodes within an action is simply
+the **lexicographical order** of their coordinates. For example, the root :math:`\epsilon` executes before its first child :math:`1`, which executes before its own first child
+:math:`1 \cdot 1`, which executes before the root's second child :math:`2`. This corresponds to what is called a **pre-order traversal**.
+
+A node :math:`n_1` is said to be an **ancestor** of node :math:`n_2` (and :math:`n_2` is a **descendant** of :math:`n_1`) if :math:`n_1` is the parent of :math:`n_2`, or if :math:`n_1` is an ancestor of the parent of :math:`n_2`.
+
+An action inherits its type from its root node:
 
 #. A **Create action** has a Create node as the root.
    The consequences are empty.
 
 #. An **Exercise action** has an Exercise node as the root
-   and the consequences are the subactions.
+   and the consequences are the actions triggered immediately by evaluating the choice.
    The Exercise action is the **parent action** of its consequences.
 
-#. A **Fetch action** as a Fetch node as the root.
+#. A **Fetch action** has a Fetch node as the root.
    The consequences are empty.
    
 The terminology on nodes extends to actions via the root node.
@@ -236,9 +251,16 @@ Subactions
 This example again highlights the hierarchical structure of actions:
 The ``AcceptAndSettle`` action contains the corresponding actions for ``Accept`` and ``Settle`` as its consequences.
 
-More generally, for an action `act`, its **proper subactions** are all actions in the consequences of
-`act`, together with all of their proper subactions.
-Additionally, `act` is a (non-proper) **subaction** of itself.
+More generally, since actions trigger consequences recursively, every action generates a family tree of subsequent events.
+For an action `act`, its **subactions** are the action itself together with its **proper subactions**, which are defined
+recursively as the subactions of its immediate consequences. If an action produces no consequences (a leaf node), it is its own sole subaction,
+meaning it has no proper subactions. The proper subactions of an action can therefore be seen as all the downstream events it triggers during execution.
+
+.. math::
+
+   Sub(A) = \{A\} \cup \bigcup_{A' \in C(A)} Sub(A')
+
+where :math:`C(A)` is the ordered list of immediate consequences of :math:`A`.
 
 The subaction relation is visualized below for Bob's ``Settle`` Exercise.
 Each borderless box contains an action (via its tree of nodes) and the nesting of these boxes encodes the subaction relation.
@@ -259,8 +281,9 @@ Transactions
 
 A **transaction** is a list of actions that are executed atomically.
 Those actions are called the **root actions** of the transaction.
-That is, for a transaction `tx = act`:sub:`1`\ `, …, act`:sub:`n`, every `act`:sub:`i` is a root action.
-For example, if Alice and Charlie have made one DvP proposal each for Bob, then Bob may want to both accept simulataneously.
+That is, for a transaction `tx = (act`:sub:`1`, \ `, …, act`:sub:`n`), every `act`:sub:`i` is a root action.
+
+For example, if Alice and Charlie have made one DvP proposal each for Bob, then Bob may want to both accept simultaneously.
 To that end, Bob exercises both ``Accept`` choices in a single transaction with two root actions (blue and purple), as shown next.
 Visually, transactions are delimited by the dashed lines on both sides, to distinguish them from actions.
 Like for actions, the input contracts on the left are not part of the transaction.
@@ -283,10 +306,38 @@ The transaction consists of two root actions (blue and purple), namely the two `
    :width: 50%
    :alt: The consequences of the ``Settle`` action are a transaction of two actions, namely the two ``Transfer`` legs of the DvP.
 
-         
-The hierarchical structure of actions extends to transactions and yields the notion of subtransactions.
-A **proper subtransaction** of a transaction is obtained by (repeatedly) replacing an action by its consequences;
-and a **subtransaction** of a transaction is either the transaction itself or a proper subtransaction thereof.
+This list structure extends the coordinate system and establishes a **Transaction Execution Order**.
+By using the list index :math:`i` as the starting coordinate for the :math:`i`-th root action :math:`act_i`, every node in the transaction forest receives a unique address.
+For example, the root node of :math:`act_1` has coordinate :math:`1`, and its first consequence has :math:`1 \cdot 1`. The root node of :math:`act_2` has coordinate :math:`2`.
+Just as with individual actions, the execution order of all nodes within the transaction is simply the **lexicographical order** of these extended coordinates.
+This ensures that the entire tree of :math:`act_1` executes before the tree of :math:`act_2`. Because every node has a strict position in this order, the entire hierarchical forest
+of a transaction can be logically **flattened into a single, chronological sequence** of execution.
+
+The hierarchical structure of actions extends to transactions and yields the notion of subtransactions. Conceptually, a subtransaction is a version of the
+original execution forest that has been "unrolled" to varying depths across its branches. It is formed by taking a representative sequence of actions
+(called a **frontier**) from each root action's tree and concatenating them in their original chronological order.
+
+For every action :math:`A` in a transaction :math:`T = (r_1, \dots, r_n)`, we derive its frontier through a recursive choice:
+
+* **Retain**: Keep the action itself as its own representative sequence: :math:`(A)`.
+* **Replace**: Substitute the action with the concatenation of the frontiers of its immediate consequences.
+If :math:`A` has no consequences, "replace" results in the empty sequence :math:`()`.
+
+Formally, for an action with consequences :math:`C(A) = (c_1, \dots, c_k)`, the set of all possible **frontiers** :math:`\mathcal{F}(A)` is defined recursively:
+.. math::
+   \mathcal{F}(A) = \{ (A) \} \cup \left\{ S_1 \oplus \dots \oplus S_k \;\middle|\; S_i \in \mathcal{F}(c_i) \right\}
+
+If :math:`A` is an action with no consequences (a leaf node), the recursion terminates with :math:`\mathcal{F}(A) = \{ (A), () \}`.
+
+The final **subtransaction** is the concatenation of the frontiers chosen for each root action. The set of all possible subtransactions :math:`\mathit{SubTx}(T)`
+for the forest is the collection of all such possible combinations:
+
+.. math::
+
+   \mathit{SubTx}(T) = \left\{ S_1 \oplus S_2 \oplus \dots \oplus S_n \;\middle|\; S_i \in \mathcal{F}(r_i) \right\}
+
+This ensures that every part of the original execution is represented (completeness) and no action can appear in a subtransaction alongside its own ancestor or descendant (vertical exclusion).
+The result is a flat, ordered sequence that provides a non-overlapping reconstruction of the ledger, tailored to a specific level of detail or privacy.
 
 For example, given the transaction shown above consisting only of the two consequences of the ``Settle`` action,
 the next diagram shows all seven proper non-empty subtransactions, each with their dashed delimiters.
@@ -313,7 +364,7 @@ modifications happen by consuming a contract ID and recreating a new contract wi
 
 This Ledger Model extends the UTxO model in two aspects:
 
-* A transaction may use a contract without consuming it, for example by exercising a non-consuming choice or fetching it.
+* A transaction may use a contract without consuming it, namely, by exercising a non-consuming choice or fetching it.
   In such a case, the contract ID remains in the set of UTxOs even though it appears as an input to a transaction.
 
 * Transactions are structured hierarchically and contract IDs created in the transaction may be consumed within the same transaction.
@@ -341,14 +392,29 @@ It consists of a single transaction and the so-called **update ID**, a string.
 Examples in the Ledger Model use update IDs of the form ``TX i`` for some number ``i``, similar to the transaction view in Daml Studio.
 On the Ledger API, update IDs are arbitrary strings whose lexicographic order is independent from their order on the ledger.
 
-A **commit** adds the information *who requested a party interaction*.
-It consists of an update and the one or more parties that requested it.
-Those parties are called the **requesters** of the commit.
+A **commit** records the information on *who* requested a party interaction. It bundles an
+**update** (the transaction and its unique ID) with the one or more parties that requested it.
+These parties are called the **requesters** of the commit.
 In Daml Script, the requesters correspond to the ``actAs`` parties given to the ``submit`` commands.
 
+Up to this point, we have focused on the constituents of a party interaction. To build a ledger, it must also be defined how multiple
+interactions are arranged relative to one another. When commits are recorded, they are linked together in a graph structure, with the
+commits represented as **vertices** and the links between them represented as directed edges. This structure is called a **Directed Acyclic Graph (DAG)**.
+
+.. admonition:: Definition: Directed Acyclic Graph (DAG)
+
+   A **Directed Acyclic Graph (DAG)** is a pair $G = (V, E)$ where:
+
+   * $V$ is a set of **vertices** (nodes).
+   * $E \subseteq V \times V$ is a set of **directed edges** (arrows).
+   * The graph is **acyclic**, meaning for any vertex $v \in V$,
+     there is no non-empty path that starts and ends at $v$.
+
+Using this general structure, we can formally define the Ledger.
+
 .. admonition:: Definition: Ledger
-                
-   A **Ledger** is a directed acyclic graph (DAG) of commits, where the update IDs are unique.
+
+   A **Ledger** is a directed acyclic graph (DAG) where the vertices $V$ are **commits** and every commit has a unique update ID.
 
 .. admonition:: Definition: top-level action
 
@@ -356,9 +422,15 @@ In Daml Script, the requesters correspond to the ``actAs`` parties given to the
    A top-level action of any ledger commit is also a top-level action of the ledger.
 
 A Canton Ledger thus represents the full history of all actions taken by parties.
-The graph structure of the Ledger induces a **happens-before order** on the commits in the ledger.
-We say that commit `c`:sub:`1` *happens before* `c`:sub:`2` if and only if the ledger contains a non-empty path from `c`:sub:`1` to `c`:sub:`2`,
-or equivalently, the transitive closure of the graph contains an edge from `c`:sub:`1` to `c`:sub:`2`.
+
+Because the graph structure of the ledger includes directed edges, it naturally induces a **happens-before order** on the commits in the ledger.
+
+.. admonition:: Definition: happens-before
+    We say that commit `c`:sub:`1` *happens before* `c`:sub:`2` if and only if the ledger contains a non-empty path from `c`:sub:`1` to `c`:sub:`2`,
+    or equivalently, the transitive closure of the graph contains an edge from `c`:sub:`1` to `c`:sub:`2`.
+
+At this stage, the edges $E$ are arbitrary. Any arrangement of commits that satisfies the acyclic property of a DAG constitutes a valid mathematical ledger.
+However, for a ledger to be useful in practice, these edges must follow the logic of the smart contracts they record.
 
 .. note::
    The :ref:`integrity conditions <da-model-integrity>` on a ledger require that the happens-before order respects the lifecycle of contracts.
@@ -389,9 +461,9 @@ This workflow gives rise to the ledger shown below with four commits:
   
 * In the second commit, Bank 2 requests the creation of the ``SimpleAsset`` of ``1 USD`` issued to Bob (contract #2).
 
-* In the third commit, Alice requests the creation of the ``SimpleDvpPoposal`` (contract #3).
+* In the third commit, Alice requests the creation of the ``ProposeSimpleDvP`` (contract #3).
 
-* In the forth commit, Bob requests to exercise the ``AcceptAndSettle`` choice on the DvP proposal.
+* In the fourth commit, Bob requests to exercise the ``AcceptAndSettle`` choice on the DvP proposal.
 
 .. _da-dvp-ledger:
   
@@ -405,8 +477,27 @@ This workflow gives rise to the ledger shown below with four commits:
    In this example, there need not be edges among the first three commits ``TX 0``, ``TX 1``, and ``TX 2``,
    so they could be presented in any order.
 
-   As the Ledger is a DAG, one can always extend the order into a linear sequence via a topological sort.
-   For the next sections, we pretend that the Ledger is totally ordered (unless otherwise specified).
-   We discuss the more general partial orders in the :ref:`causality section <local-ledger>`.
+Because the graph is acyclic, the happens-before relationship forms a **strict partial order** on the commits. It is transitive (if `c`:sub:`1` < `c`:sub:`2` and `c`:sub:`2` < `c`:sub:`3`,
+then `c`:sub:`1` < `c`:sub:`3`) and irreflexive (a commit cannot happen before itself). Because it is only a *partial* order, not all commits can be compared. It is possible that neither
+`c`:sub:`1` < `c`:sub:`2` nor `c`:sub:`2` < `c`:sub:`1` is true.
+
+It is a well-known property that any partial order can be extended into a **total order** (a linear
+sequence), or equivalently, the vertices of any finite Directed Acyclic Graph can be arranged into a
+linear sequence. In graph theory, this is achieved via a **topological sort**, which arranges the vertices of a
+DAG into a linear sequence whose order preserves the partial order induced by the directed edges, i.e. for every directed edge in E from `c1` to `c2`, `c1`
+appears before `c2` in the sequence.
+
+For the next sections on Integrity and Privacy, we assume that the Ledger is totally ordered (unless otherwise specified).
+We will return to the more general partial order in the :ref:`causality section <local-ledger>`.
+
+.. admonition:: Definition: Global Execution Order
+
+   By combining the totally ordered sequence of commits with the flattened sequence of each transaction, we establish a **Global Execution Order** for all action nodes on the ledger.
+   We say a node :math:`n_1` **executes before** :math:`n_2` if:
+
+   1. They are in the same commit, and :math:`n_1` precedes :math:`n_2` in the **Transaction Execution Order**.
+   2. They are in different commits :math:`c_1` and :math:`c_2`, and :math:`c_1` appears before :math:`c_2` in the totally ordered ledger.
+
+   Because every node has a rigorous execution order, the entire ledger can be viewed as a single, chronological timeline of actions (events).
 
 
diff --git a/sdk/docs/manually-written/overview/explanations/ledger-model/local-ledger.rst b/sdk/docs/manually-written/overview/explanations/ledger-model/local-ledger.rst
index fb1008779fc4..9e8b703e24f1 100644
--- a/sdk/docs/manually-written/overview/explanations/ledger-model/local-ledger.rst
+++ b/sdk/docs/manually-written/overview/explanations/ledger-model/local-ledger.rst
@@ -11,11 +11,16 @@ Causality
    Update so that the DAG structure of ledgers are reflected directly.
    This should greatly simplify the formalism here.
 
+To understand causality, we must distinguish between the theoretical model (Daml Ledger Model) and the real-world system (Daml Ledger).
+**The Daml Ledger Model** often assumes a single, global timeline where every transaction is strictly ordered. This
+simplification makes the ledger's logic easier to define. **A Daml Ledger** is a distributed system that
+does not totally order all transactions. Because forcing a global order on unrelated events is inefficient, real-world
+ledgers use a **partial order**.
 
-Daml ledgers do not totally order all transactions.
-So different parties may observe two transactions on different Participant Nodes in different orders via the :externalref:`gRPC Ledger API <ledger-api-services>`.
-Moreover, different Participant Nodes may output two transactions for the same party in different orders.
-This document explains the ordering guarantees that Daml ledgers do provide, by :ref:`example <causality-examples>` and formally via the concept of :ref:`causality graphs <causality-graph>` and :ref:`local ledgers <local-ledger-structure>`.
+In practice, this means different parties may observe two transactions on different Participant Nodes in different orders
+via the :externalref:`gRPC Ledger API <ledger-api-services>`. Moreover, different Participant Nodes may output two transactions for the same party in different orders.
+This document explains the ordering guarantees that Daml ledgers do provide, by :ref:`example <causality-examples>` and
+formally via the concept of :ref:`causality graphs <causality-graph>` and :ref:`local ledgers <local-ledger-structure>`.
 
 The presentation assumes that you are familiar with the following concepts:
 
@@ -28,7 +33,7 @@ The presentation assumes that you are familiar with the following concepts:
 Causality Examples
 ******************
 
-A Daml Ledger need not totally order all transaction, unlike ledgers in the Daml Ledger Model.
+A Daml Ledger need not totally order all transaction, unlike the assumption on ledgers in the Daml Ledger Model.
 The following examples illustrate these ordering guarantees of the Ledger API.
 They are based on the paint counteroffer workflow from the Daml Ledger Model's :ref:`privacy section <da-model-privacy>`,
 ignoring the total ordering coming from the Daml Ledger Model.
@@ -71,14 +76,14 @@ and the **Fetch** commit comes after the **Create** of the `Iou`.
 
 .. _causality-example-non-consuming:
 
-Non-Consuming Usages in Different Commits May Appear in Different Orders
+Non-Consuming Usages in Different Unordered Commits May Appear in Different Orders
 ========================================================================
 
 Suppose that the Bank exercises a non-consuming choice on the `Iou Bank A` without consequences while Alice creates the `CounterOffer`.
 In the ledger shown below, the Bank's commit comes before Alice's commit.
    
 .. https://app.lucidchart.com/documents/edit/1923969f-7bf2-45e0-a68d-6a0b2d308883/0_0
-   
+
 .. image:: ./../images/counteroffer-double-fetch.svg
    :align: center
    :width: 100%
@@ -220,7 +225,7 @@ Definition »Causal consistency for a contract«
   * If `X` is not empty, then `X` contains exactly one **Create** action.
     This action precedes all other actions in `X` in `G`\ 's action order.
 
-  * If `X` contains a consuming **Exercise** action `act`, then `act` follows all actions in `X` other than `act` in `G`\ 's action order.
+  * If `X` contains a consuming **Exercise** action `act`, then `act` follows all other actions in `X` in `G`\ 's action order.
 
 Definition »Causal consistency for a key«
   Let `G` be a causality graph and `X` be a set of actions on a key `k` that belong to transactions in `G`.
@@ -238,7 +243,7 @@ Definition »Causal consistency for a key«
 Definition »Consistency for a causality graph«
   Let `X` be a subset of the actions in a causality graph `G`.
   Then `G` is **consistent** on `X` (or `X`-**consistent**) if `G` is causally consistent for all contracts `c` on the set of actions on `c` in `X` and for all keys `k` on the set of actions on `k` in `X`.
-  `G` is **consistent** if `G` is consistent on all the actions in `G`.
+  `G` is **consistent** if `G` is consistent on the set of all the actions in `G`.
 
 When edges are added to an `X`-consistent causality graph such that it remains acyclic and transitively closed,
 the resulting graph is again `X`-consistent.
@@ -248,7 +253,7 @@ So it makes sense to consider minimal consistent causality graphs.
 
 Definition »Minimal consistent causality graph«
   An `X`-consistent causality graph `G` is `X`\ -**minimal** if no strict subgraph of `G` (same vertices, fewer edges) is an `X`-consistent causality graph.
-  If `X` is the set of all actions in `G`, then `X` is omitted.
+  If `X` is the set of all actions in `G`, then the prefix `X` is omitted and the graph is simply called **minimal**.
 
 For example, the :ref:`above causality graph for the split counteroffer workflow <causality-graph-counteroffer-split>` is consistent.
 This causality graph is minimal, as the following analysis shows:
@@ -256,9 +261,9 @@ This causality graph is minimal, as the following analysis shows:
 +----------------+--------------------------------------------------------------------------------------+
 | Edge           | Justification                                                                        |
 +================+======================================================================================+
-| `tx1` -> `tx3` | Alice's `Iou` **Create** action of  must precede the **Fetch** action.               |
+| `tx1` -> `tx3` | Alice's `Iou` **Create** action must precede the **Fetch** action.               |
 +----------------+--------------------------------------------------------------------------------------+
-| `tx2` -> `tx4` | The `CounterOffer` **Create** action of  must precede the **Exercise** action.       |
+| `tx2` -> `tx4` | The `CounterOffer` **Create** action  must precede the **Exercise** action.       |
 +----------------+--------------------------------------------------------------------------------------+
 | `tx3` -> `tx4` | The consuming **Exercise** action on Alice's `Iou` must follow the **Fetch** action. |
 +----------------+--------------------------------------------------------------------------------------+
@@ -285,7 +290,7 @@ At the bottom, `tx5` asserts that there is no key for an Account contract for th
 Then, `tx6` creates an such account with balance 0 and `tx7` deposits the painter's `Iou` from `tx4` into the account, updating the balance to 1.
 
 .. https://app.lucidchart.com/documents/edit/b9d84f0f-e459-427c-86b8-c767662af326
-   
+
 .. image:: ./../images/causality-consistency-examples.svg
    :align: center
    :width: 100%
diff --git a/sdk/docs/sharable/overview/explanations/ledger-model/ledger-privacy.rst b/sdk/docs/sharable/overview/explanations/ledger-model/ledger-privacy.rst
index 075ec6c56685..bd997088e565 100644
--- a/sdk/docs/sharable/overview/explanations/ledger-model/ledger-privacy.rst
+++ b/sdk/docs/sharable/overview/explanations/ledger-model/ledger-privacy.rst
@@ -247,7 +247,7 @@ Projecting the ledger of the complete DvP example yields the following projectio
 
 Examine each party's projection in turn:
 
-#. Alice sees all of the first, thrid, and forth commit
+#. Alice sees all of the first, third, and fourth commit
    as she is an informee of all root actions.
    In contrast, Alice does not see anything of the second commit,
    as she is not a stakeholder of Bob's ``SimpleAsset`` of 1 USD.
@@ -258,7 +258,7 @@ Examine each party's projection in turn:
    This effect is discussed below under :ref:`retroactive divulgence <da-model-divulgence>`.
 
 #. Bob's projection is analogous to Alice's:
-   He sees everything of the second, third, and forth commit,
+   He sees everything of the second, third, and fourth commit,
    but nothing of the first commit and instead merely contract #1 as an input.
 
 #. Banks 1 and 2 only see the commits in which they create their ``SimpleAsset`` and the ``Transfer`` Exercises on them.
diff --git a/sdk/docs/sharable/overview/explanations/ledger-model/local-ledger.rst b/sdk/docs/sharable/overview/explanations/ledger-model/local-ledger.rst
index fb1008779fc4..d5aef1420767 100644
--- a/sdk/docs/sharable/overview/explanations/ledger-model/local-ledger.rst
+++ b/sdk/docs/sharable/overview/explanations/ledger-model/local-ledger.rst
@@ -71,7 +71,7 @@ and the **Fetch** commit comes after the **Create** of the `Iou`.
 
 .. _causality-example-non-consuming:
 
-Non-Consuming Usages in Different Commits May Appear in Different Orders
+Non-Consuming Usages in Different Unordered Commits May Appear in Different Orders
 ========================================================================
 
 Suppose that the Bank exercises a non-consuming choice on the `Iou Bank A` without consequences while Alice creates the `CounterOffer`.