Dependency Aggregate Recursion

Abstract

Global prerequisite meet and join aggregates satisfy exact local predecessor recursion laws.

Theorem 1.1 (Prerequisite joins satisfy local recursion).

$$\begin{gathered} \forall edge:V\to V\to Prop,label:V\to Label,node:V, \\ [\mathrm{CompleteLattice}\left(Label\right)], \\ \mathrm{prerequisiteJoin}\left(edge,label,node\right)=\sup \left(\mathrm{label}\left(node\right),{\mathrm{iSup}}_{predecessor:V}{\mathrm{iSup}}_{dependency:\mathrm{edge}\left(predecessor,node\right)}\mathrm{prerequisiteJoin}\left(edge,label,predecessor\right)\right). \end{gathered}$$

Proof. Machine-checked in Lean as D5/S3/ConceptDynamics/DagCompletion/DependencyAggregateRecursion.prerequisiteJoin_recursion (✓ std3). ∎

Source. Repository-derived.

Commentary.

In a complete lattice, the global join over a node’s prerequisite cone equals its own label joined with the joins of every direct predecessor.

The equality includes all direct predecessors through the displayed local aggregate; it does not assume finiteness or choose an enumeration.

Theorem 1.2 (Prerequisite meets satisfy local recursion).

$$\begin{gathered} \forall edge:V\to V\to Prop,label:V\to Label,node:V, \\ [\mathrm{CompleteLattice}\left(Label\right)], \\ \mathrm{prerequisiteMeet}\left(edge,label,node\right)=\inf \left(\mathrm{label}\left(node\right),{\mathrm{iInf}}_{predecessor:V}{\mathrm{iInf}}_{dependency:\mathrm{edge}\left(predecessor,node\right)}\mathrm{prerequisiteMeet}\left(edge,label,predecessor\right)\right). \end{gathered}$$

Proof. Machine-checked in Lean as D5/S3/ConceptDynamics/DagCompletion/DependencyAggregateRecursion.prerequisiteMeet_recursion (✓ std3). ∎

Source. Repository-derived.

Commentary.

Dually, the global prerequisite meet equals the node label met with every direct predecessor’s prerequisite meet.

The complete-lattice assumption is an instance binder. No distributivity or finite-lattice hypothesis is added.

References

• Truth anchor: D5/S3/ConceptDynamics/DagCompletion/DependencyAggregateRecursion.prerequisiteJoin_recursion
• Truth anchor: D5/S3/ConceptDynamics/DagCompletion/DependencyAggregateRecursion.prerequisiteMeet_recursion
• Dependency: D5/S3/ConceptDynamics/DagSemantics/DependencyAggregate